问题标签 [z3py]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
z3 - 如何使用 BitVector 对有符号整数进行建模？
假设它a是一个 8 位的整数 value 254。如果a是有符号整数，则实际上被认为是-2。相反，如果a是无符号的，它仍然是254。
我试图用 Z3 用 BitVector 理论来模拟这个有符号/无符号整数问题，但似乎 BitVector 不允许这样做。这是真的？那么关于如何在 Z3py 中建模的任何想法？
非常感谢。
z3 - Z3在变量决策过程中可以调用python函数吗？
我正在尝试解决一个问题，例如我有4 点，每两点之间都有成本。现在我想找到总成本小于界限的节点序列。我写了一个代码，但它似乎不起作用。主要问题是我已经定义了一个 python 函数并试图在约束中调用它。
这是我的代码：我有一个函数def getVal(n1,n2): where n1, n2are Int Sort。该行将Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ]4 个点定义为 Int 排序，当我添加约束时s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) < 100)，它会立即调用getVal函数。但我想要的是，当 Z3 将决定 Nodes[0]、Nodes[1]、Nodes[2]、Nodes[3] 的值时，应该调用该函数来获取点之间的成本。
如果这不是解决问题的正确方法，那么您能否告诉我其他解决问题的方法。我可以使用 Z3 求解器对此类问题进行编码以找到最佳的航点序列吗？
z3 - 可以从 Z3 得到最终的 CNF 公式吗？
这是我的简单编码。我想获得呈现所有这些约束的最终布尔 CNF。Z3求解器中是否有任何选项可以获得最终的布尔CNF？
感谢和问候
z3 - 可以使用 Z3py 计算 Kauffman 括号吗？
我正在尝试使用 Z3py 计算三叶结的考夫曼括号。到目前为止，我有以下代码：
使用此代码，我获得以下输出：
现在我需要应用规则：
并使用此类规则简化输出。拜托，你能告诉我怎么做吗？非常感谢。
z3 - 如何使用 Z3 的 Python API 执行量词消除
如何使用 Z3 的 Python API 执行量词消除？尽管我检查了教程和 API，但无法做到。
我有一个具有存在量词的公式，我希望 Z3 给我一个新公式，这样这个量词就被消除了。我基本上想做与此相同的事情：
但使用 Python 接口。我的公式也是线性算术。
谢谢！
加法：在完成量词消除后，我将“添加”另一个无量词公式。因此，如果我使用策略，有没有办法将子目标（即策略的输出）转换为线性算术表达式？
z3 - 在电气网络的情况下，如何使用 Z3Py 和 Taylor 的想法执行量词消除
请考虑以下电网
这个电网的 SAT 问题是
使用Z3Py在线解决此问题，使用以下代码：
输出是：
最后使用 Z3Py 我们解决了量词消除的线性问题：
相应的输出是：
在此处在线运行此示例
请让我知道为什么 Z3Py 在线性示例中没有完全执行量词消除；并且如果可以在线使用 Z3Py 解决量词消除的原始非线性问题。非常感谢。
z3 - 是否可以强制 Z3 模型评估涉及数组的布尔表达式？
有时，评估模型中的布尔表达式不会返回具体的布尔值，即使表达式显然具有具体值。我已经能够将其简化为涉及数组表达式的情况，例如这个测试用例：
我希望这可以打印False，但它会打印K(Int, 0) == Store(K(Int, 0), 0, 1)。其他示例产生类似的结果。将第一行替换x = Array('x', IntSort(), IntSort())为相同的结果（尽管这取决于默认解释）。有趣的是，将第一行替换为x = Store(K(IntSort(), 0), 0, 1)导致示例打印True。
有没有办法强制 Z3 将这些表达式评估为具体值？
z3 - 为什么带数字参数的 * 没有被简化展平？
我希望simplifywith:flat评估3 * x * y * zto (* 3 x y z)。相反，结果是(* 3 (* x y z))。为什么？
例子
z3 - 在 Z3 中使用 push 命令进行增量求解
我正在使用 Z3 的 python api 进行某种增量求解。solver.push()我迭代地将约束推送到求解器，同时使用命令检查每个步骤的不可满足性。我想了解 Z3 是否会使用从先前约束中学习到的引理，或者在使用新添加的约束进行求解时先前获得的令人满意的解决方案。我从不使用solver.pop()命令。我在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？