1回答
我刚刚发现Z3 JAVA API中名为"mkDiv()“的除法是指整数除法，而不是普通除法。例如： ArithExpr a = ctx.mkDiv(ctx.mkInt(3),ctx.mkInt(5)).simplify(); A的结果是"0“但"3/5”。在tutor中，除法和整数除法似乎是分开的两部分：(assert (= r1 (Diva4)；整数除法(assert (>= b (/ c3.0
浏览 14提问于2020-10-18得票数 0
回答已采纳
2回答
Z3使用JNA引发无效的内存访问
、、、、
我在java中使用jna的Z3 C应用程序接口。我经常得到无效的内存访问，但仅限于windows (.dll)和mac os (.dylib)库。当然，这种解决方案是不可持续的。在线程中，用户遇到了类似的问题，事实证明这是由于一些编译配置造成的。at 0x000000000000000c
Crashed Thread: 0 Dispatch queue: com.a
浏览 1提问于2012-09-03得票数 3
回答已采纳
1回答
我们有一个使用.NET API v4.0的Z3项目。我们希望能够在Mono上编译和运行该项目。这听起来很奇怪，但我们的情况如下。我们有一个使用Z3的课程，所有的实验室计算机都安装了Windows和.NET框架。"z3.dll" target="libz3.dylib" os="osx"
浏览 3提问于2013-01-13得票数 10
回答已采纳
在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
1回答
我使用的是Z3的Java API，我需要定义自然的整数变量，即它们的值不能为负数。如何使用java API在z3中定义自然数据类型？
浏览 1提问于2015-06-17得票数 1
我正在使用Z3 java API。我需要定义一组配对元素e.x。{(e1，e2)...}我不知道如何使用Java API在z3中声明配对数据类型？
浏览 1提问于2015-02-10得票数 0
2回答
我已经安装了Z3 API for Java，我正在尝试使用它，但是我找不到任何文档来解释如何使用这个API。到目前为止，我发现的唯一资源是和，因此我想知道是否有人知道Z3 Java API的其他文档。
浏览 4提问于2014-04-21得票数 4
回答已采纳
1回答
在Z3接口中，FuncDecl有一个DeclKind()来表示它是否是重写规则。但是如何在Z3 java API中创建重写规则呢？
浏览 4提问于2013-03-05得票数 1
回答已采纳
我有一个已有的smt2文件，并用z3 java api解析了这个，解决了这个问题。但我有一个关于如何将FuncDecl转换为Expr的问题，因为我想使用z3 java apis构建一些简单的公式。因为我的原始公式完全是用smt2文本文件编写的，所有内容都被解析到一个BoolExpr中。现在，我成功地提取了const，并且需要用新的公式来处理它们。我该怎么做呢？基本上，我正在寻找的是
浏览 0提问于2013-12-13得票数 1
当我尝试运行bin文件夹中的z3.exe文件时。提示符出现后立即消失。我需要知道如何通过z3.exe文件运行用z3编写的文件。
我该怎么做呢？或者，通过Java运行z3的最佳选择是什么？
浏览 6提问于2013-03-17得票数 3
回答已采纳
1回答
回到过去的日子(即。去年)，我们曾经能够使用理论插件作为一种实现自定义简化器的方法。Z3文档甚至包含了。
我的问题很简单:有没有办法用Z3 4.x实现同样的目标？特别是，我感兴趣的是一种为Z3提供基本术语的外部计算评估的方法。
浏览 2提问于2012-12-10得票数 2
回答已采纳
我正在尝试对Java 32位整数算法进行建模。我正在尝试使用z3位向量来实现这一点。我使用的是来自不稳定分支的Z3 Java API。 .simplify()).getLong());
我得到了我想要的结果
浏览 1提问于2013-12-05得票数 0
我已经生成了一个smt2文件，它已经被Z3 (4.3)通过Z3 Java成功读取(解析)。现在我想知道如何让Z3开始解决多个作用域(推送和弹出)的公式。smt2文件包含推送和弹出命令的列表。我知道您可以使用solver.push()和solver.pop()来实现这一点，但是这里的问题是作用域已经在文件中生成了，而我没有使用Z3内部API来创建这些公式和作用域。我只需要将整个smt2文件提供给Z3并执行多次求解(只有
浏览 2提问于2015-07-18得票数 1
1回答
我需要使用java API在z3中定义一个函数，该函数接受一个目录的输入，然后递归删除其中的所有内容。既然z3不支持递归函数，有没有办法表达这种功能呢？
浏览 3提问于2015-08-12得票数 0
我在z3 shell和java api中都尝试了相同的假设。declare-const x (_ BitVec 32))
(check-sat)在z3外壳中，解决方案是:x=9，但在z3应用程序接口中，解决方案是:x= 0x80000000在我的应用程序中，我更喜欢外壳结果。所以我想知道我是否错过了
浏览 0提问于2016-11-08得票数 1
1回答
我的程序使用Z3_open_log()创建所有z3交互的日志。然后在另一个程序中，我用Z3_parse_z3_file()将其读回。它给了我在输入上做出的所有断言的连接。然后通过解析z3文件，我得到(和a1 a2)。如果这不是
浏览 1提问于2012-03-29得票数 1
回答已采纳
1回答
虽然我可以看到在C++中存在对Java的遍历(在这个question中概述)，但我在Java api中找不到它的等效方法，有没有一种方法可以在Z3中遍历Java？ 谢谢!
浏览 12提问于2019-02-25得票数 1
回答已采纳
云服务器
ICP备案
云点播
对象存储
即时通信 IM
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号