z3 相关问题

Z3是Microsoft Research开发的高性能定理证明器。

我列出了一些关于二次函数的断言：（declare-fun H（）Int）（assert（> = H 8000））（assert（<= H 12000））（minimize（-（^ H 2）H））（ check-sat），但答案是“未知”，原因是...

z3 smt nonlinear-optimization

回答 1 投票 0

获取量化变量的z3实例

我正在尝试对z3做些奇怪的事情。我正在尝试看看我是否可以使用z3从交互式定理证明者那里获得类似“应用”策略的信息。我有一个像ForAll（[x]，Implies（a（...

z3 z3py

回答 1 投票 0

z3中具有MaxSMT的量词

我们可以在z3中使用带有软约束的量词吗？一起使用它们时，我会收到以下消息。警告：不支持使用量化约束进行优化

z3 smt

回答 1 投票 0

z3.parse_smt2_string在int2bv上失败

当我在文档中的示例字符串上使用parse_smt2_string时，它可以正常工作。但是，在int2bv上解析失败。我该如何诊断？ >>>导入z3 >>> z3 ....

python python-3.x z3 z3py

回答 1 投票 1

Z3优化中的间隙公差控制

我想使用z3优化类来获得次优的结果，同时仍然能够控制我离最优结果有多远。我正在使用C ++ API。例如，CPLEX具有...

optimization z3

回答 1 投票 1

我们可以提取z3使用的当前策略，然后类似地配置另一个实例吗？

我想在设置特定逻辑时重复使用/激活的策略，但是我需要避免使用set-logic。因此，有什么方法可以让Z3在...

回答 1 投票 0

使用MAXSMT进行增量学习

我们可以在z3中以增量方式使用MaxSMT求解器的先前解决方案（优化）吗？另外，是否有任何方法可以在优化程序上打印出软断言？

z3 smt

回答 1 投票 0

这些条款的等效horn条款是什么？

我正在使用Z3和扩展的SMT-LIB2语法来解决我的horn子句。我知道horn子句的头应该是未解释的谓词；但是，我不知道应该如何重写以下内容...

z3 z3-fixedpoint horn

回答 1 投票 0

为什么Z3对这些号角子句返回“未知”

我正在使用Z3解决我的horn子句。在Horn子句的主体中，未解释的谓词应为肯定。但是，我需要否定一些未解释的谓词。我看过一些...

z3 z3-fixedpoint

回答 1 投票 0

cpp中z3的编译和执行命令？

＃include #include #include“ mainProj.cpp”使用命名空间std;使用名称空间z3; int main（）{上下文c; tactic t = tactic（c，“ bit-blast”）; expr x = c .... ] >>

c++ z3 smt

回答 1 投票 0

检查一阶逻辑是否满足要求的工具/语言？

通常，一阶逻辑是不确定的。但是，可以确定一些一阶逻辑片段，例如Monadic逻辑，BSR片段，分隔片段。有解决SAT / SMT问题的工具...

z3 first-order-logic satisfiability sat-solvers

回答 1 投票 1

z3中有实值计算的问题

我正在研究一个我想根据某些约束来学习真实参数的问题。以下是代码片段：s = Solver（）def logistic_function（x，y）：out = y [0] for i in ...

z3 smt

回答 1 投票 0

为什么Python是64位时，为什么不能在Windows上使用pip安装angr-z3？

它说模块机器类型不匹配；为什么？（注意：这是一个自我解答的问题；请参阅下文。）

python pip 64-bit z3 angr

回答 1 投票 1

SMT-LIB基准

我想对一些SMT求解器进行基准测试，而SMT-LIB Benchmark存储库[1,2]似乎是一个不错的起点。但是，链接已关闭至少几天。有人知道吗...

z3 smt bitvector

回答 2 投票 2

z3py处函数“ from_file（）”的问题

假定我们具有以下文件：func.smt（声明数据类型（T）（（（AVL leafA（nodeA（val T）（alt Int）（izq AVL）（der AVL）））））espec.smt （declare-const t（AVL Int））和...

z3 solver z3py

回答 1 投票 0

有什么方法可以使Z3使用多核（多线程）解决大问题？

我正尝试从商用求解器转到Z3，以解决大整数可满足性问题。 “大”是指我要求解的模型具有约300,000个整数和300,000个（...

optimization z3 smt

回答 1 投票 1

Z3中定义变量和常量的宏

我想在Z3中拥有可以定义变量和常量的宏。我无法弄清楚如何使用该语言，因此我正在使用cpp（c预处理器）来执行此操作。例如，我有：＃...

macros c-preprocessor z3

回答 1 投票 2

unzip z3解算器失败

我正在尝试在非root用户的远程Linux服务器上安装z3，我已将ubuntu匹配发行版下载到服务器上的主目录中，当我解压缩它时，我没有得到所有文件夹...] >

ubuntu server z3

回答 1 投票 0

z3模型的NoneType输出

我正在使用MaxSMT来找到一组软约束和硬约束的解决方案。超时为600秒，我从求解器得到的模型输出对于所有参数都是Nonetype。我...

z3 smt

回答 1 投票 0

z3解算器：使用“ parseSMTLIB2String”与“ rise4fun在线工具”获得不同的结果

我正在使用z3开发Java程序，但是当我使用“ parseSMTLIB2String”方法与在线工具rise4fun测试非常简单的编码时，得到了不同的结果。以下是我用于测试的编码：...

java z3

回答 1 投票 1

z3 相关问题

最新问题