我正在尝试使用 Z3 来确定表达式是否可满足。我可以通过定义上下文然后定义 int_const 变量和公式来轻松地做到这一点。要以编程方式计算表达式，您必须用代码编写所有内容。假设逻辑表达式以字符串的形式给出，那么呢？例如，
“x == y &&！x == z”
在 C API 中将表示为：
context c;
expr x = c.int_const("x")
//Same for other variables
...
formula = (x == y) && (!x == z);
solver s(c);
s.add(formula);
//s.check() ...etc etc
好的，我可以为这个特定的公式编写代码，但是如何在给定字符串的情况下以编程方式执行此操作。我对你能想到的任何事情都持开放态度。
谢谢 ：）
在Z3教程的第13.2.3节中,有一个很好的例子,说明如何减少在处理注入的公理化时必须实例化的模式数量.在该示例中,必须以单数形式表示的函数f将类型A的对象作为输入并返回类型B的对象.据我所知,排序A和B是分离的.
我有一个SMT问题(FOL + EUF)Z3似乎没有终止,我试图找出原因.我有一个函数f:A-> A我认为是单射的.问题可能是f的域和codomain重合吗？
提前感谢任何建议.
这个问题非常类似于:Z3:将Z3py表达式转换为SMT-LIB2？
是否可以从Solver对象生成SMT-LIB2输出？
给定一个简单的移位和异或运算，其中“输入”是符号：
input = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = 0xffffffff & ((shiftreg << 8) | (shiftreg >> 24))
shiftreg = shiftreg ^ 0xcafebabe
s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
# unsat
我们被告知这个方程是不可解的。如果打印，s包含：
[4294967295 &
((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
3405691582 ==
134520840]
但是，我可以轻松地创建一个示例来解决“输入”的这个方程。
want = 0x804a008
want ^= 0xcafebabe
want = 0xffffffff & ((want >> 8) | (want << 24))
want ^= 0x8049d30
print hex(want) …我有一个非常简单的示例Z3程序，如下所示：
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
此示例程序可以在Z3在线编译器中执行，没有问题。但是当我想使用以下命令使用命令行提示符执行同一程序时：
Z3 <script path>
我收到错误消息：
ERROR: line 1 column 21: could not match expression to benchmark .
并对程序中的每一行重复此错误。谁能帮我看看我在做什么错？
据我所知，z3 一般无法验证归纳证明。但我很好奇是否有一种方法可以让它检查一些简单的事情，例如：
; returns the same input list after iterating through each element
(declare-fun iterate ((List Int)) (List Int))
(declare-const l (List Int))
(assert (forall ((l (List Int)))
(ite (= l nil)
(= (iterate l) nil)
(= (iterate l) (insert (head l) (iterate (tail l))))
)
))
(assert (not (= l (iterate l))))
(check-sat)
现在它只是在我的机器上永远循环。
一阶逻辑的有效命题 (EPR) 片段通常被定义为以下形式的 prenex 量化公式集\xe2\x88\x83X.\xe2\x88\x80Y.\xce\xa6(X,Y)，其中X和Y是（可能为空）变量序列。量化的顺序（即 ）\xe2\x88\x83*\xe2\x88\x80*对于 EPR 的可判定性重要吗？如果改变量化顺序，我们会失去可判定性吗？
特别是，我对捕获可判定逻辑中的 set-monadic 绑定操作的语义感兴趣。给定S1类型的元素集T1（即S1具有类型）和类型的T1 Set函数，set-monad 的绑定操作通过应用于每个元素来构造一个新的类型集fT1 -> T2 SetS2T2 SetfS1并联合结果集可以在以下 SMT-LIB 代码/公式中捕获此行为：
(declare-sort T1)\n(declare-sort T2)\n;; We encode T1 Set as a boolean function on T1\n(declare-fun S1 (T1) Bool)\n(declare-fun S2 (T2) Bool)\n;; Thus, f becomes a binary predicate on (T1,T2)\n(declare-fun f (T1 T2) Bool)\n(assert (forall ((x T1)(y T2)) (=> …In following Python code:
from itertools import product
from z3 import *
def get_sp(v0, v1):
res = sum([v0[i] * v1[i] for i in range(len(v0))])
return res
def get_is_mod_partition(numbers):
n = len(numbers)
mod_power = 2**n
for signs in product((1, -1), repeat = len(numbers)):
if get_sp(numbers, signs) % mod_power == 0:
return 1
return 0
def check_sat(numbers):
n = len(numbers)
s = Solver()
signs = [Int("s" + str(i)) for i in range(n)]
for i in range(n):
s.add(Or(signs[i] == -1, signs[i] == 1)) …我想使用 Int 向量作为数组索引。
Python。
array = [12,45,66,34]
s= Solver()
x = Int('x')
s.add(array[x] == 66)
所以 x 应该是 2..
我该怎么做？
我想提高 SMT 求解的可扩展性。我实际上已经实现了增量求解。但我想提高更多。在不了解问题本身的情况下，还有其他一般方法可以改进它吗？