smt 相关问题

可满足性模数理论（SMT）是逻辑公式的决策问题，与经典的一阶逻辑中表达的背景理论的组合相等。

z3中的DPLL（T）样式SMT解决方案是否已为线性实数算法记录？

我正在尝试设计方法来改善我的问题的z3性能。我知道CAV'06论文和技术报告。 z3 v4.3.1的相关部分是否与这些...中描述的内容有所不同？

z3 smt formal-verification dpll

回答 1 投票 1

Z3统计数据的解释

我从Z3的运行中获得了一些统计数据。我需要了解这些含义。对于sat和SMT解决方案的最新发展，我颇为生疏，不了解最新信息，因此，我试图...

z3 smt usage-statistics sat-solvers dpll

回答 1 投票 6

Z3中的多元素减法

我正在使用Z3解决需要减法的问题，并且我遇到了这样一个事实，即Z3中的减法允许多个参数。对我来说，这很奇怪，因为减法不是联合运算。 ...

z3 smt associativity

回答 1 投票 0

在z3中使用战术时有空未饱和核数

使用战术时，Solver返回空的unsat核心。情况1：s = Solver（）x =实数（'x'）B =布尔（'b'）C =布尔（'c'）s.add（B ==（x> 1））s.add（C ==（x == -1））s.check（B，C）情况2：s = Then（'...

z3 smt z3py

回答 1 投票 0

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

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

z3 solver smt

回答 1 投票 1

在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中具有MaxSMT的量词

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

z3 smt

回答 1 投票 0

使用MAXSMT进行增量学习

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

z3 smt

回答 1 投票 0

smt2中的类型不匹配

下面的smt2代码给出与类型有关的错误。（声明数据类型（（列表1））（（par（T）（（cons（hd T）（tl（列表T））（nil））））））））（声明排序Ty 0）（定义乐趣- rec ...

smt cvc4

回答 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

z3中有实值计算的问题

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

z3 smt

回答 1 投票 0

SMT-LIB基准

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

z3 smt bitvector

回答 2 投票 2

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

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

optimization z3 smt

回答 1 投票 1

z3模型的NoneType输出

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

z3 smt

回答 1 投票 0

在SMT的定义中包含断言

我想捕获事实事实断言。 int f（x）{if（x == 1）返回1; else {assert（x> 0）;返回2; }} int g（x）{assert（x> 5）; ...

z3 smt

回答 1 投票 1

如何将IntVector转换为z3py中的Int

我正在使用z3py，并且我有一个大小为3的IntVector。我需要将IntVector中的每个数字解析为一个整数。意思是，如果我有一个IntVector，它具有这样的约束：myIntVector = ...

python z3 smt z3py

回答 1 投票 1

如果我在（get-model）之后标记它？

如果仅执行（检查星期六），则标记为不坐。但是，如果您尝试（get-model），它不会标记，并且错误会立即出现。有什么办法可以标记我而不会出错？

z3 smt

回答 1 投票 0

如果有多个解决方案，我最多可以打印2个？ [处于保留状态]

如果一个公式具有多个模型，是否有某种方法可以打印它们？我有一个问题，我知道有很多解决方案。但是，如果我使用以下命令（check-sat）（get-model）（...

z3 smt

回答 1 投票 1

计算一个整数集的总和

使用CVC4的集合理论（版本1.8-预发行版[git master a90b9e2b]），我定义了一组具有固定基数的整数（set-logic ALL_SUPPORTED）（set-option：produce-models true）（...

smt cvc4

回答 1 投票 1

什么是落后Z3优化最大值和最小值功能的原理是什么？

我写这封信询问Z3优化功能背后的理论/算法，特别是对于它的最大值和最小值功能。这似乎很神奇的给我。它是莫名其妙的二进制搜索或这样的吗？怎么样 ...

z3 smt

回答 1 投票 3

smt 相关问题

最新问题