1回答
我正在为一个项目使用z3 Java API。对于一些例子，它需要花费太多的时间来解决。我已经等了好几个小时了，还是不能解决这个问题。我不知道它会不会解决。但是当我将Solver::toString的输出打印到一个文件中时，z3二进制在一秒钟内就解决了这个问题。我尝试了一些策略和参数，但没有帮助。这里有一个例子(列表理论)：这里的问题可能是什么？谢谢。
浏览 1提问于2018-08-16得票数 0
在前面的问题中，我问到当使用nlsat解算器处理非线性实算法上的多项式约束时，z3是否能给出一个完整的结果。正如泰勒所回答的，nksat的解算器是完整和健全的。当解决上帝军的约束时，Z3支持非卫星核心提取。我想知道是否有可能在使用nlsat解算器时提取出unsat核心？如果z3不支持，我能在z3之上实现它吗？另一个问题是它能处理多大的问题。
浏览 4提问于2014-04-13得票数 2
回答已采纳
我试图用“nlsat”解算器实现快速解释算法。由于该算法需要多次求解原约束集的子集，所以我决定在z3 c++接口中使用push/pop函数(在nlsat解算器中检查(假设)不工作)。z3能够告诉我，整个约束集在不到1分钟的时间内是unsat。但是，当检查原始约束集的子集时，它不会给出超过1小时的结果。原始约束集的子集如有任何建议，将不胜感
浏览 3提问于2014-04-30得票数 1
回答已采纳
1回答
我想定义一个二维数组，如下所示，使用z3求解器，使用C如何使用Z3解算器C API来定义这一点，其中我需要添加一些约束，比如每行的总和等于
浏览 0提问于2013-04-17得票数 2
1回答
如何用Z3生成模型？
、、、
我目前正在与SMT求解器Z3一起开发一种模型计数方法。有人知道Z3是如何为例如线性算术类生成模型的吗？使用了哪种算法，在哪里可以找到该算法的源代码？
谢谢，扬尼奇
浏览 2提问于2016-02-05得票数 0
回答已采纳
我一直在阅读尼古拉的文章《使用Z3的工程理论》，这篇文章讲述了如何将自定义决策过程与Z3连接起来。Z3 API在。有人能告诉我他们或他们的替代品在哪里吗? 2.在相关的注释中，我在界面中看到了几个新概念，如探针和战术。这些都有描述或解释吗？
浏览 0提问于2012-12-27得票数 1
1回答
我是Z3的新手，作为练习，我尝试了一个魔方解算器，通过改编现有的数独解算器()。或者有经验的z3程序员会建议我的实现存在问题，因为这种规模的问题应该是可以解决的？
谢谢。
浏览 5提问于2015-10-27得票数 2
我在Python-API中使用Z3。我正在设置一组相当大的线性算术约束。如果我不使用任何push/pop，一切都可以正常工作。我在MacOS 10.7.5上使用Z3版本4.3.1 - 64位。
非常感谢&致敬，克劳斯
浏览 3提问于2013-06-18得票数 2
1回答
上下文:我使用z3对有界java程序验证进行了研究。我想得到一个线性化问题的优化模型。一种标准的方法是递增地搜索模型，直到找到未满足条件的情况。但是性能似乎是个问题，而且引入JNI破坏了代码的可移植性，JNI将z3 c/c++ api集成到我的工具中。
现在我想在java方法的所有输入上添加约束。我使用数量数组(我使用数组理论对堆进行建模)。然而，对于可满足的问题，z3总是立即返回“未知”。似乎生成模型是不可能的。我注意到有一个选项z3，INST_GEN，然后我试图理解它。我将以下公式提供给<e
浏览 5提问于2012-07-13得票数 2
回答已采纳
这些扩展可以同时与Z3的所有其余部分(即在Z3中实现的所有其他理论解算器)一起使用吗？或者这些字符串扩展只适用于准独立？
浏览 0提问于2016-06-09得票数 1
0回答
Z3中Real变量的通常精度是多少？是否使用精确算术？如果Real意味着必须使用精确的算术，那么对于精度有限的浮点值，是否还有其他的数据类型？最后:从这个角度来看，z3与其他流行的SMT解算器是不同的，还是在SMT-LIB定义中是标准化的？
浏览 6提问于2017-06-14得票数 1
回答已采纳
1回答
使用options -smt2 -in启动后，是否可以获得Z3的版本？就像这样; Z3 4.3.2 x64 // Desired reply
浏览 0提问于2013-04-08得票数 2
回答已采纳
1回答
ocaml上的Z3结合
、、、、
我目前使用的是ocaml 4.06.0，我正在尝试使用Z3卫星解算器。我正在使用opam的绿洲来编译文件(它成功地构建了所有的东西)。我尝试重新安装z3包，但错误仍然存在。有人能帮我解决这个问题吗?因为我不知道还能尝试什么？
浏览 1提问于2018-11-10得票数 1
回答已采纳
1回答
我正在使用Z3的python来进行某种增量解决。我迭代地将约束推到求解器，同时使用solver.push()命令检查每个步骤的不可满足性。我想知道Z3是使用以前约束的学习引理，还是用新添加的约束来解决以前得到的满意解。我从不使用solver.pop()命令。在哪里可以获得更多关于如何使用以前迭代中完成的工作的详细信息？
浏览 8提问于2013-08-16得票数 5
回答已采纳
我将数字存储为z3::expr，并希望对它们进行比较。我尝试了以下几点：z3::expr a = c.real_val("0");z3::expr comp =如果我使用的是一个求解器，那么所有的事情都会像预期的那样工作：s.add(comp);
std::cout << s.check() <<
浏览 6提问于2021-11-26得票数 2
回答已采纳
在进行理论一致性检查之前，Z3的SAT解算器是否获得了对SMT问题的命题(化)部分的完整赋值？另外，在实际代码(codeplex稳定的z3 v4.3.1)中，由SAT求解器决定的命题字面(启发式)在哪里？
浏览 3提问于2014-01-21得票数 1
回答已采纳
在之后，我在本教程中尝试了第一个示例。(set-logic QF_UF)(assert (and p (not p)))(exit)java -jar jsmtlib.jar test1.smt这可能有什么问题呢？
浏览 0提问于2012-09-22得票数 0
回答已采纳
云服务器
对象存储
ICP备案
云点播
实时音视频
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号