标签: z3

我正在尝试一些涉及递归函数的Z3教程的例子.我试过以下例子.

1. 斐波纳契(第8.3节)
2. IsNat(第8.3节)
3. 归纳法(第10.5节)

Z3超过了上述所有示例.但是,该教程似乎意味着只有Inductive是非终结的.

Z3可以检查包含递归函数的公式的可满足性,还是无法处理任何归纳事实？

特别是,它是否使用DPLL(T)？它是否使用低于/高于近似值？它是否在单词级别处理线性算术？那么非线性算术呢？

我在文章中只发表了一篇关于"类似于MathSAT/Boolector中的简化"的表面提及,以便有效地解决量化比特公式.

非常有趣的是什么方法帮助Z3在smtcomp的QF_BV部分获得第一名.

我想使用Z3 C API解决包含量词的约束.我正在努力使用像"Z3_mk_exists()"这样的函数,因为我没有找到任何在线或tar文件中的测试示例中的示例.我并不完全理解这些函数所需的所有参数以及它们的确切含义.有人可以帮忙吗？

谢谢.Kaustubh.

当我试图获得一个模型字符串,以及我定义的变量时,我在模型中得到额外的输出 -

 z3name!0=3, z3name!1=-2, z3name!10=0, z3name!11=0, z3name!12=0, z3name!13=0, z3name!14=0, z3name!15=0, z3name!2=0, z3name!3=0, z3name!4=2, z3name!5=2, z3name!6=0, z3name!7=-3, z3name!8=2, z3name!9=0

我想知道这是错误的输出吗？或者是Z3正在使用的一些中间变量？

因为我定义的变量的值对我来说似乎没问题.我之前没有见过任何这样的输出,因此我怀疑了.

我编写以下Z3 python代码

x, y = Ints('x y')
F = (x == y & 16)      # x has the value of (y & 16)
print F

但我得到了以下错误:

TypeError: unsupported operand type(s) for &: 'instance' and 'int'

如何在Z3方程中进行按位运算(在这种情况下)？

谢谢.

如何使用z3计算解决方案的数量？例如,我想证明,对于任何一个n,方程组有2个解{x^2 == 1, y_1 == 1, ..., y_n == 1}.以下代码显示给定的可满足性n,这不是我想要的(我想要任意数量的解决方案n).

#!/usr/bin/env python

from z3 import *

# Add the equations { x_1^2 == 1, x_2 == 1, ... x_n == 1 } to s and return it.
def add_constraints(s, n):
    assert n > 1
    X = IntVector('x', n)
    s.add(X[0]*X[0] == 1)
    for i in xrange(1, n):
        s.add(X[i] == 1)
    return s

s = Solver()
add_constraints(s, 3)
s.check()
s.model()

任何人都可以告诉我如何通过Z3py实现最小化整数问题,如下所示？我如何定义所有声明？这里所有变量都是int sort.

Z3中是否有专门的求解器可以解决这类问题？如果有,那么我该如何设置该求解器的配置？

谢谢

我已经使用profiler gprof(这里包括调用图的统计数据)描述了我的问题,这些问题在(伪非线性)整数实际片段中,并且试图将分成两个类的时间分开:

I)SAT求解部分(包括[纯粹]布尔传播和[纯粹]布尔冲突子句检测,回跳,任何其他命题操作)

II)理论解决部分(包括理论一致性检查,理论冲突条款的产生和理论传播).

做线3280-3346在smt_context.cpp内bounded_search()组成的顶级DPLL(X)循环？

我相信在SAT求解器函数中总结时间更容易(因为它们更少),然后其余的可以被认为是理论解算器的时间.我想弄清楚我应该考虑哪些功能属于上面的I类？他们是smt::context::decide(),smt::context::bcp()内smt::context::propagate()？还有其他人？ smt::context: resolve_conflict()似乎与理论解决者的呼吁混在一起？

它的功能smt::context::propagate()似乎主要是理论传播(第二类)bcp()吗？而且,smt::context::final_check()似乎纯粹是在II级.

任何提示都非常感谢.谢谢.

对于任意k和布尔变量的数量,在Z3中编码"至少k /最多k个这些布尔变量必须为真"的约束是什么？

我想通过引入新的PB变量(使用这种编码)将"至少k "作为伪布尔问题,通过双条件(例如)将它们与我的布尔变量相关联,并声明它们的总和大于或者等于k.这是一种合理的方法,还是我应该使用更简单/更有效的编码？x == true iff y == 1

我正在尝试使用Python中的Z3 Thoerem Prover解决一个方程式。但是我得到的解决方案是错误的。

from z3 import *    
solv = Solver()
x = Int("x")
y = Int("y")
z = Int("z")
s = Solver()
s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>0, z>0)
s.add()
print(s.check())
print(s.model())

我得到这个解决方案：

[z = 60, y = 5, x = 1]

但是，当您将这些值填写到给定的方程式中时，结果为：10.09735182849937。但是我想找到的是一个精确的解决方案。我究竟做错了什么？

谢谢你的帮助 ：）