z3 相关问题

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

我怎么知道Z3py中是否有一个数组为空？

我开始使用Z3py，并且我很难理解它的功能。我必须知道数组是否为isEmpty，但是我不知道如何在“ x”和“ array” def之间创建引用...

python z3 z3py

回答 1 投票 0

Z3的“ ctx-solver-simplify”和“ ctx-simplify”之间的可满足性不一致

我正在尝试使z3（我正在使用z3py）来检查公式是否可满足，如果可满足，则对其进行简化。我最初使用Z3的ctx-solver-simplify。但是，由于我是...

z3 z3py simplification sat satisfiability

回答 1 投票 0

Z3给序列指定的错误模型

我将以下代码放在https://rise4fun.com/Z3/中（declare-const s（Seq Int））（declare-const t1（Seq Int））（declare-const t2（Seq Int））（declare -const n Int）（断言（=（seq.len s）n））（断言（＆...

回答 1 投票 0

z3中`str.indexof`与`seq.indexof`之间的差异

在z3教程中，分别提到了str.indexof和seq.indexof。但是，在Z3 C API中，只有一个相关函数Z3_mk_seq_index。该函数是否进行特殊情况处理...

回答 1 投票 0

为什么Z3保持变量不变，即使它被指定不这样做

我在Z3中遇到了一个问题，似乎无法找到它的起源以及如何解决。我的目标是对于给定的特定迭代（for循环），它由if-then-else ...

z3 solver smt

回答 1 投票 1

如何使z3生成不满足的证据？

我正在尝试从命令行使用z3作为SAT解算器，但是我不知道如何使它生成不满足的证明。不管我做什么，它只会打印“ unsat”，没有任何解释，...

z3 sat

回答 1 投票 0

在smt / z3优化中哪个非线性断言是完整的？

我列出了一些关于二次函数的断言：（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

z3 相关问题

最新问题