标签: z3

SMTLib2指令(get-info all-statistics)显示多个数字，例如

num. conflicts:     4
num. propagations:  0 (binary: 0)
num. qa. inst:      23

为了测试不同的公理化和编码，我想知道这些数字中的哪一个适合宣布一个Z3运行比另一个运行更好/更有效。

从名字中猜测，我想说的是num. qa. inst-数量化实例化的数量-是一个很好的指标（低=更好），但是其他指标呢？

我在一个名为"knapsack.smt2"的文件中有背包问题的以下示例代码,我相信它是smt2格式,我有最新版本的Z3:

(declare-const s1 Int)
(declare-const o1 Int)
(declare-const b1 Bool)

(declare-const s2 Int)
(declare-const o2 Int)
(declare-const b2 Bool)

(declare-const s3 Int)
(declare-const o3 Int)
(declare-const b3 Bool)


(declare-const sack-size Int)
(declare-const filled Int)

(assert (< o1 sack-size))
(assert (< o2 sack-size))
(assert (< o3 sack-size))

(assert (>= o1 0))
(assert (>= o2 0))
(assert (>= o3 0))

(assert (=> (not b1)(= o1 o2)))
(assert (=> (not b2)(= o2 o3)))

(assert (=> b1 (= (+ o1 s1) o2)))
(assert (=> …

我有一些混淆使用通用量词和declare-const而不使用forall

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (>= (f x x) (+ x a))))

我可以这样写:

(declare-const x Int)
(assert  (>= (f x x) (+ x a))))

在这两种情况下,使用Z3将探索Int类型的所有可能值.那有什么区别？我真的可以使用declare-const来消除forall量词吗？

我在IR中有一些代码,这段代码已经是SSA形式.现在我试图将此代码转换为SMT公式,然后将其提供给Z3进行一些验证.我有一些问题:

1. 有没有技术论文详细解释如何将SSA IR转换为SMT公式？我四处搜索,无济于事.

2. 对于那些计算指令,转换为Z3公式没有太多问题.但是,我仍在努力处理无条件和条件分支指令.有关如何将这些指令转换为Z3公式的任何建议？

非常感谢!!!

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(simplify (or (= s ON) (= s OFF) (= s BROKEN)))
(simplify (and (> a 0) (> a 1)))

结果是:

(or (= s ON) (= s OFF) (= s BROKEN))
(and (not (<= a 0)) (not (<= a 1)))

但预期的结果是:

1
> a 1

是否有可能在Z3中简化这些表达式(这些表达式的组合)？谢谢!

我正在使用Z3的Python API,试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用Python接口提取不可满足核心的问题.

我有以下简单查询:

(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)

通过z3可执行文件(对于Z3 4.1)运行此查询,我收到了预期的结果:

unsat
(__constraint0)

对于Z3 4.3,我获得了一个分段错误:

unsat
Segmentation fault

这不是主要问题,尽管这是一个有趣的观察.然后我将查询(在文件中)修改为

(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)

使用文件处理程序,我将此文件的内容(在变量`queryStr'中)传递给以下Python代码:

import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
    ...
elif querySatResult == z3.unsat:
    print solver.unsat_core()

我从`unsat_core'函数接收空列表:[].我是否正确使用此功能？该函数的文档字符串表明我应该做类似的事情

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

但是,我想知道是否仍然可以按原样使用查询,因为它符合SMT-LIB v2.0标准(我相信),以及我是否遗漏了一些明显的东西.

我成功地在我的Mac OSX(Mountain Lion,JDK 7,Scala 2.10,Z3 4.3)上安装了Scala ^ Z3(在此之后:http://lara.epfl.ch/w/ScalaZ3).一切都很顺利,除了我不能从这个网站(http://lara.epfl.ch/w/jniz3-scala-examples)运行任何例子,没有得到这个讨厌的错误:

java.lang.NoClassDefFoundError: scala/reflect/ClassManifest
    at .<init>(<console>:8)
    at .<clinit>(<console>)
    at .<init>(<console>:7)
        ...
Caused by: java.lang.ClassNotFoundException: scala.reflect.ClassManifest
    at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
    at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
    at java.security.AccessController.doPrivileged(Native Method)
    at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
    ... 29 more

Run Code Online (Sandbox Code Playgroud)

我认为这是因为Scala 2.9.x和2.10.x在处理反射时不兼容.因为我能够在Scala 2.9.x下运行相同的示例集.我的问题是,无论如何要解决这个并在Scala 2.10下运行Scala ^ Z3？

我对以下两个声明感到困惑。对我来说，它们描述的是同一件事：整数变量x。

• (declare-const x Int)
• (declare-fun x () Int)

是否有任何上下文可以使它们在性能上有所不同或提供不同的模型？谢谢。

我一直在努力解决一个包含某些术语绝对值的小问题.在z3中,不支持abs()函数.在python中有,但我最终必须将它传递给z3py.有什么方法可以通过它将绝对运算符的术语从python传递给z3,还是有其他方法吗？以下是一个小例子的代码.

`
x = Int('x')
y = Int('y')

x= abs(2-y)
s=Solver()
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m`

答案应该是y = 1,这是删除abs()时的情况.有没有办法用绝对值函数来解决这个问题？ABS().或者有什么方法可以在python中解决它,然后我可以将它传递给z3.我也尝试过同情,但它不起作用.

我有两个文件,其内容相同,除了我放置断言的顺序:在一个文件中,断言按照另一个的相反顺序放置.第一个文件(po-9.z3)在不到一秒的时间内被Z3声明为不可用,而另一个(po.z3)在一分钟内无法验证.

造成这种差异的原因是什么？我假设将先前在验证中涉及的断言放在文件中会改善性能.但是,通过验证的那个(po-9.z3)在文件的底部有大多数相关/特定于问题的断言.另外,在po.z3中,虽然要证明的定理和假设位于文件的顶部,但是一个重要的断言(lambda表达式的一阶公式)放在文件的底部.当我把它带到顶部时,po.z3会在不到一秒的时间内完成验证.

在z3 smt2文件中生成断言的最佳顺序是什么？