z3 相关问题

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

异常：型号不可用

我在使用符号执行模型的 z3 中收到模型不可用的错误消息。初始代码添加了 v1 和 v2 并且它可以工作，但是一旦我替换 v1 和 v2 值，我得到的模型是......

python random model z3 ctf

回答 1 投票 0

如何在Z3的SMT-LIB中定义枚举类型

我之前使用Z3的API来定义一个枚举类型，如下所示让 T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|]) 它将类型 T 的元素枚举为“a”、“b”和“c”（没有其他内容......

z3 smt

回答 2 投票 0

根据寄存器值重新制定寄存器位之间的按位布尔表达式

假设我们有两个例如32 位输入寄存器和一个同样宽的输出寄存器，并通过布尔函数链接这些寄存器的各个位。有没有一种方法可以按位表示这些

z3 boolean-expression

回答 1 投票 0

是否可以将C++代码转换为SMT2？

我是 SMT 求解器和这些主题的新手。我需要将 C++ 代码转换为 SMT2 的等效代码（我有一个需要 .smt2 作为输入的工具）。我已经找到了这个解决方案，但它没有解释

z3 smt

回答 2 投票 0

添加多个约束后 Z3 位向量无法满足

对于 CTF 挑战，我需要根据每个字节的几个约束重建一个字节数组。然而，在 Z3 中尝试了一下位向量后，我注意到solver.check()返回...

python z3 z3py

回答 1 投票 0

Z3：超时参数无效

为Z3求解器设置了超时参数，执行数千次求解后，发现超时参数无效，求解过程不会在预定时间停止...

回答 1 投票 0

与 Z3 Python API 进行异或 - 仅返回单个解决方案

我正在使用 Z3 的 Python API 测试单个 XOR 语句。这是我得到的输出： [B_L = 真，A_L = 假，C_L = 假] 然而，我应该有 3 个解决方案，其中两个变量是......

python z3 z3py

回答 1 投票 0

为 Z3 开发新理论求解器的指南和/或最小工作示例

从之前在 StackExchange 上提出的许多问题中，我了解到理论插件现已在 Z3 4.x 中弃用，现在预计可以编写自己的理论求解器并从

回答 1 投票 0

Z3 求解器类型错误：“ArithRef”对象无法解释为整数

我正在尝试使用 Z3py 运行下面的代码，主要问题是我想使用求解器找到我的函数的参数。我想在我的

z3 smt z3py

回答 1 投票 0

Z3-Solver 的“TransitiveClosure”功能是否有 bug？

这是使用 TransitiveClosure 的简单示例的代码。从 z3 导入 * defcompute_transitive_closure（图）： num_nodes = len(图) # 创建 Z3 上下文 ctx = 上下文() #

z3 z3py constraint-programming operations-research transitive-closure

回答 1 投票 0

Z3优化模块出现意外行为？

我也有一个带有软约束的优化问题。所有软约束都具有相同的权重 1. 问题：如果软约束改变了优化，那么它们实际上是否应该被忽略......

z3 z3py

回答 1 投票 0

z3 中原子的自定义理论

我希望 z3 中有一些变量，它们取某个无限集合中的值，其元素除了相等比较之外没有任何操作（lisp 意义上的原子理论）。目前...

z3 smt sat propagation

回答 1 投票 0

z3 中最大满足子集查找器的文档示例中的错误

我正在尝试使用 z3 文档示例中的代码来查找 z3 中最令人满意的子集。这是我复制的代码：从 z3 导入 * def main(): x, y = 实数('x y')

z3 smt z3py

回答 1 投票 0

提高 z3 优化问题的求解器速度

我正在尝试使用 Z3 (Python) 解决包含线性整数模理论的 SMT 问题。该问题类似于 Knuth

python performance z3 smt

回答 1 投票 0

rust z3 并行求解所有可行值

详情我有一个需求，就是解决所有可行的结果，并且表达式只有未知。我使用rust z3来做到这一点，但是效率太慢了！我的想法例如，我有一个表达 li...

rust parallel-processing z3 solver

回答 1 投票 0

Z3 .NET API 中的优化给出了不正确的结果 - bug？

我正在使用 Z3 的 .NET API，并且使用下面的代码发现了奇怪的行为（可能是优化器中的错误）。当使用 Optimize 类运行时，它会错误地找到解决方案，而

.net optimization z3

回答 1 投票 0

我想构建一个 z3 解算器来打印范围而不是打印所有可能的值

假设我有一个整数表达式 x。因此，如果我不应用任何约束，该整数的最小值和最大值将是 INT_MIN 和 INT_MAX。但假设我应用一个约束 a 使得 a

c++ z3 constraint-programming

回答 1 投票 0

如何在 Z3 Java API 中定义带约束的递归函数？

我正在使用 Z3 Java API 并尝试通过使用递归 API 定义函数 f(x) = x + 1。然而，我不想直接将函数定义为 y = x + 1，而是想使用约束来

java z3 smt

回答 1 投票 0

向 z3 添加二元运算符

我正在尝试解析字符串并将其翻译为其等效的 z3 形式。导入z3 表达式 = 'x + y = 10' p = my_parse_expr_to_z3(expr) # 结果：([x, '+', y], '==', [10]) p = my_flatten(p) ...

python parsing z3

回答 1 投票 0

为什么 Z3 对于类似的约束返回 sat 和 unsat？

我是Z3的新手，并试图用它解决“发送+更多=金钱”的难题。我通过复制其他人的代码解决了一些错误，但我不太明白它为什么有效。 Q1: 为什么...

python z3 z3py

回答 1 投票 0

z3 相关问题

最新问题