标签: z3

我正在使用Z3 SMT求解器来解决我在逻辑QF_BV中使用SMTLIB 2语言表达的问题.

该模型是不可满足的,我试图让求解器产生一个不满足的核心.

我的模型由几个"强制"约束组成,我使用assert语句指定.

我想要使​​用(assert (! (EXPR) :named NAME))构造来指定我想要用于不良核心生成的断言.

unsat正如预期的那样,Z3给了我一个.然而,Z3似乎总是抛弃一个由所有命名的断言组成的"琐碎的"不饱和核心.

我知道我的命名断言中存在一个子集,这是一个不可靠的核心.我使用Yices SMT求解器找到了这个核心,它经常给我相对较小的不饱和核心.Yices模型与Z3模型相同(几乎是从SMT2到Yices输入语言的逐行转换).

产生"好"的不良核心是解决者特有的功能,还是我可以做出任何通用的建议/改变来帮助Z3给我一个更好的核心？

我最近观察到Z3中有关触发的几种行为,我不明白.不幸的是,这些例子来自大型Boogie文件,所以我想我现在抽象地描述它们,只是为了看看是否有明显的答案.但是,如果具体文件会更好,我可以附加它们.

基本上有三个问题,尽管第三个可能是第二个问题的特例.据我所知,没有任何行为是预期的,但也许我错过了一些东西.任何帮助将不胜感激!

首先:就触发而言,我的程序中的琐碎平等似乎被忽略了.例如,if t1是一个应该与量化公理的模式匹配的术语,如果我在表单的Boogie程序中添加一行

assert t1 == t1;

然后t1似乎没有被用作量化公理的触发器.我明确地添加了这一行,以便为t1证明者提供触发器,我经常在Boogie程序中做/做.

相反,如果我引入了额外的功能,比方说

function f(x : same_type_as_t1) : bool
{ true }

现在改为添加一行

assert f(t1);

我的节目,然后t1 就似乎被用来作为Z3的触发器.我检查了前程序的Z3翻译,并且(平凡的)平等t1确实在Boogie翻译中存活下来(即,不是Boogie尝试做一些聪明的事情).

其次:次要模式似乎对我不起作用.例如,我有一个程序,其中一个公理有形式

axiom (forall ... :: {t1,t2} {t3,t4,t5} ..... );

和一种情况,t3, t4并t5都发生了.程序无法验证,显然是因为公理没有实例化.但是,如果我重写公理为

axiom (forall ... :: {t3,t4,t5} {t1,t2} ..... );

然后程序验证.在这两种情况下,运行Boogie的时间大约为3秒,并且模式可以存活到Z3输出.

第三:这很可能是第二个问题的症状,但我对以下行为感到惊讶:

我写了这个形式的公理

axiom (forall .. :: {t1,t2} .... );

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving …

在使用z3处理我的硕士论文时,我发现了一些我无法理解的奇怪的东西.我希望你能帮助我.:)

我写的smt文件看起来像这样:

(set-logic QF_UF)
(set-info :smt-lib-version 2.0)

;Declare sort Node and its objects.
(declare-sort Node 0)
(declare-fun n0 () Node)
(declare-fun n1 () Node)

;Predicate
(declare-fun dead_0 (Node) Bool)
;Abbreviation
(declare-fun I () Bool)

;initial configuration
(assert(= I (and 
(not(= n0 n1))
(not(dead_0 n0))
(dead_0 n1))))

;Predicate
(declare-fun dead_1 (Node) Bool)
;variable
(declare-fun m0_1 () Node)

;Abbreviation for Transformation
(declare-fun TL1_1 () Bool)

;Transformation1neuerKnoten1
(assert(or (= m0_1 n0)(= m0_1 n1)))

;Is the whole formula satisfiable?
(assert(= (and I TL1_1) true)) …

Z3目前支持DIMACS格式输入.在解决方案之前有没有办法输出问题的DIMACS格式？我的意思是将问题转换为系统CNF并以DIMACS格式输出.如果没有,任何朝这个方向发展的想法都会有所帮助.

我正在尝试在mac os x上构建Z3.

在README文件之后,我刚刚执行了

autoconf
./configure
make

得到错误"omp.h"文件未找到.

我将omp.h文件从目录复制/usr/llvm-gcc-4.2/lib/gcc/i686-apple-darwin11/4.2.1/include到lib目录来解决这个问题.

然后,我lib/buffer.h:243:13: error: use of undeclared identifier 'push_back'在构建代码时遇到错误.

可能是什么解决方案？我gcc version 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2336.11.00)在Mac OS X 10.7.5上.

我们知道,我们可以通过以下方式证明一个定理的有效性:

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
assert ( forall (x,y) . Demorgan(x,y) )

或者,我们可以通过以下方式消除forall量词:

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
( assert (not  Demorgan(x,y) ) )

因此,如果它返回不饱和,那么我们可以说上面的公式是有效的.

现在我想用这个想法从以下断言中消除forall量词:

assert ( exists x1,x2,x3 st .( forall y . formula1(x1,y) iff
                                          formula2(x2,y) iff
                                          formula3(x3,y) ) )

那么在Z3(使用C++ API或SMT-LIB2.0)中有什么办法可以断言如下:

assert (exists x1,x2,x3 st. ( and ((not ( formula1(x1,y) iff formula2(x2,y) )) == unsat)
                                  ((not ( formula2(x2,y) iff formula3(x3,y) )) == unsat))) 

我是Z3的新手,我正在查看在线python教程.

然后我想我可以检查BitVecs中的溢出行为.

我写了这段代码:

x = BitVec('x', 3)
y = Int('y')

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

我期待[y = 7,x = 7](即当值相等但后继不是因为x + 1将为0而y + 1将为8)

但Z3回答[y = 0,x = 0].

我究竟做错了什么？

任何或多或少的实用编程语言和编译器都必须处理约束.最常见的约束是类型.通常,类型推导和统一是通过简单的算法(例如Hindley-Milner)完成的,其中最终程序中的所有项都被赋予唯一类型.如果没有发生,则会出现错误指示.

在编译器中可能存在更复杂的约束,其中完全统一是不可能的,并且解决方案仅在某些限制下存在.可能的例子是

• 数据流分析.仿射相等约束的解可以用于循环矢量化.

• 内存管理.如果我们对引用和数据访问模式有一些约束,编译器可以从优化引用计数和垃圾收集中受益.

从另一点来看,约束求解器(如Z3或Yices)在为不同类型的约束寻找可满足的模型方面非常强大.

我正在寻找有关编译器如何从SMT求解器的强大功能以及他们正在解决的任务类型中受益的成功案例.我列出了一些区域,但我没有找到任何具体的例子.你能建议吗？

在之前的文章中,使用Z3Py在线解决了涉及运算放大器的一些问题.但是现在Z3Py在线无法使用我试图在线使用Z3 SMT-LIB来解决这些问题.

例1:

在以下电路中找到R的值

使用以下代码解决此问题:

(declare-const R Real)
(declare-const V1 Real)
(declare-const V2 Real)
(declare-const Vo Real)
(declare-const I1 Real)
(declare-const I2 Real)
(declare-const g Real)
(assert (= (/ V1 (+ R -50)) I1))
(assert (= (/ V2 (+ R  10)) I2))
(assert (= (* (* R (+ I1 I2)) -1) g))
(assert (= Vo g))
(assert (= Vo -2))
(assert (= V1 1))
(assert (= V2 0.5))
(assert (> R 0))
(assert (> R 50))
(check-sat)
(get-model) …

我在Windows 7以及64位Java 7上使用的是Z3版本4.3.2的Java-API,但我不认为Java是回答这个问题的必要条件.

现在我使用以下Java代码来简化Z3中断言的一个子集:

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Goal goal = ctx.mkGoal(true, false, false);
goal.add(bel.toArray(new BoolExpr[0])); // bel is List<BoolExpr>
ApplyResult applyResult = simplifyTactic.apply(goal);

到目前为止,我已经过滤了要简化的断言,然后使用上面的代码进行简化,它按预期工作.

经过一些测试后,我得出结论,我还需要插入模型的过滤断言(其中包含一些元信息,如基数).

是否有可能简化一些断言集A,而另一个断言集B仍被视为但未被改变？

以下示例可能会稍微澄清这个问题:

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)

(assert (=> a c)); member of set A
(assert (=> b d)); member of set A
(assert a); member of set A

; member of set B
(assert 
    (<= 
        (+ (ite (= c true) 1 0) (ite (= d true) …