2回答
Z3使用JNA引发无效的内存访问
、、、、
我在java中使用jna的Z3 C应用程序接口。我经常得到无效的内存访问，但仅限于windows (.dll)和mac os (.dylib)库。在线程中，用户遇到了类似的问题，事实证明这是由于一些编译配置造成的。jna4404318687023840668.tmp 0x000000010a00c884 ffi_call + 644
21 jna4404318687023840668.tmp 0x000000010a003ca5 Java_com_sun_jna_Native_ffi_1prep_1c
浏览 1提问于2012-09-03得票数 3
回答已采纳
在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
1回答
去年)，我们曾经能够使用理论插件作为一种实现自定义简化器的方法。Z3文档甚至包含了。
我的问题很简单:有没有办法用Z3 4.x实现同样的目标？特别是，我感兴趣的是一种为Z3提供基本术语的外部计算评估的方法。
浏览 2提问于2012-12-10得票数 2
回答已采纳
1回答
我需要使用java API在z3中定义一个函数，该函数接受一个目录的输入，然后递归删除其中的所有内容。既然z3不支持递归函数，有没有办法表达这种功能呢？
浏览 3提问于2015-08-12得票数 0
1回答
如何在Z3 Java API中定义排序？我需要做一件类似以下的事情： (define-sort Set (T) (Array T Bool))
浏览 9提问于2019-06-13得票数 0
我是Z3的新手，所以请原谅这个问题听起来太简单了。我有两个问题，在Z3 Java中重新分级常量。
如何在内部创建常量？String, int)到public StringSymbol mkSymbol(String)，这最终调用了Native.mkStringSymbol(var1.nCtx(), var2)，后者在var3中生成了这一行中的变量另一件我感到困惑的事情是使用API定义常量的范围。在交互式Z3<em
浏览 2提问于2017-12-31得票数 1
1回答
我使用的是Z3的Java API，我需要定义自然的整数变量，即它们的值不能为负数。如何使用java API在z3中定义自然数据类型？
浏览 1提问于2015-06-17得票数 1
我正在尝试对Java 32位整数算法进行建模。我正在尝试使用z3位向量来实现这一点。我使用的是来自不稳定分支的Z3 Java API。
但是，我不知道如何从z3获得正确的溢出行为。
浏览 1提问于2013-12-05得票数 0
2回答
作为，Z3不能提供递归函数的模型。然而，有没有可能告诉Z3 (最好是通过Java API)，没有定义递归函数的模型就足够了(或者实际上选择我感兴趣的函数，实际上我不需要非常数函数的模型)？显然，这可能会导致查询返回sat，尽管有些函数没有模型。基本上，用户必须确保这些函数确实具有某种模型。然而，我假设这并不是Z3或SMT求解器的工作方式，也就是说，我假设Z3需要一
浏览 1提问于2014-09-24得票数 1
1回答
在Z3接口中，FuncDecl有一个DeclKind()来表示它是否是重写规则。但是如何在Z3 java API中创建重写规则呢？
浏览 4提问于2013-03-05得票数 1
回答已采纳
我正在使用Z3 java API。我需要定义一组配对元素e.x。{(e1，e2)...}我不知道如何使用Java API在z3中声明配对数据类型？
浏览 1提问于2015-02-10得票数 0
1回答
我正在学习在匹配案例中运行类似的代码，该案例用于匹配JAVA API中的卡车运输(https://www.microsoft.com/en-us/research/wp-content/uploads有一个用于定义max函数的代码： (define-fun imax ((a Int) (b Int)) Int (if (> a b) a b)) 我把它翻译成Java： public static
浏览 9提问于2020-08-29得票数 0
我对SMT Z3使用(如DbC)的代码和开源替代工具的实际示例很感兴趣，并寻找实例。因此，事实上，我对类似的Z3正式解决工具感兴趣，但是：
最后，关于将
浏览 3提问于2011-01-06得票数 5
回答已采纳
1回答
有时(或多次)发生的情况是，问题太大，以至于Z3求解器有很多超时。在这种情况下，我认为将问题分成更小的子问题将是有益的。我在examples目录中看到了一个理论示例，但是它对我来说并不是很清楚。
浏览 0提问于2013-02-20得票数 0
回答已采纳
我一直在阅读尼古拉的文章《使用Z3的工程理论》，这篇文章讲述了如何将自定义决策过程与Z3连接起来。Z3 API在。有人能告诉我他们或他们的替代品在哪里吗? 2.在相关的注释中，我在界面中看到了几个新概念，如探针和战术。这些都有描述或解释吗？
浏览 0提问于2012-12-27得票数 1
当我在-st中使用Z3标志时，我得到了Z3的内存消耗。但是，我想使用C/C++ API获得同样的信息。有人能告诉我怎么做吗？我尝试使用API Z3_solver_get_statistics()，然后使用Z3_stats_to_string()。但是，生成的字符串不包含任何有关内存的信息。
谢谢！
浏览 0提问于2013-10-08得票数 1
回答已采纳
1回答
有两个expr_vector A，B，我尝试使用以下命令比较它们中的元素错误‘class z3：：expr或者您能告诉我如何比较这两个expr_vector中的变量吗？例如变量q1分别在向量<expr>A和B中。
浏览 0提问于2013-02-06得票数 1
我想问一下，如何下载使用Java的稳定版本的Z3？在codeplex的主分支中，源不包含目录src/api/java。
这是存在于一些分支，如cade24或rc和其他。我不知道该选哪一个。
浏览 1提问于2014-10-23得票数 1
回答已采纳
我已经生成了一个smt2文件，它已经被Z3 (4.3)通过Z3 Java成功读取(解析)。现在我想知道如何让Z3开始解决多个作用域(推送和弹出)的公式。smt2文件包含推送和弹出命令的列表。我知道您可以使用solver.push()和solver.pop()来实现这一点，但是这里的问题是作用域已经在文件中生成了，而我没有使用Z3内部API来创建这些公式和作用域。我只需要将整个smt2文件提供给Z3并执行多次求解(只有这一部分，我需要Z3 API
浏览 2提问于2015-07-18得票数 1
我是z3求解器的初学者。我想实现通用量词，我在https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html中发现context.mkForAll例如，我应该如何实现以下语句的检查:对于{2，4，6，8}中的任意y，存在整数x，其中x> y？ 这是我第一次在这里提问，所以请让我知道如何改进我的问题。
浏览 30提问于2020-07-08得票数 0
回答已采纳
云服务器
对象存储
ICP备案
云点播
实时音视频
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号