标签: z3

我在QFBV公式上使用Z3.我想知道Z3是否可以像SAT求解器这样的公式逐步增加布尔子句.基本上我需要一种方法来实现以下循环:

F = initial QFBV formula
while(F is unsat) {
    F := F Union {some additional QFBV formula based on unsat core}
}

Z3是否保留学到的信息？我可以逐步使用z3吗？

谢谢.

说我有

t1<x and x<t2

是否可以隐藏变量x以便 t1<t2 在Z3中？

对于某些给定的结果/ x对,我想在简单的"result = x*t + c"公式中找到c和t系数:

from z3 import *

x=Int('x')
c=Int('c')
t=Int('t')

s=Solver()

f = Function('f', IntSort(), IntSort())

# x*t+c = result
# x, result = [(1,55), (12,34), (13,300)]

s.add (f(x)==(x*t+c))
s.add (f(1)==55, f(12)==34, f(13)==300)

t=s.check()
if t==sat:
    print s.model()
else:
   print t

......但结果显然是错误的.我可能需要找出如何映射函数参数.

我该如何正确定义功能？

我想从z3获得的解决方案没有简化使用let语句.

例如,如果我给出以下内容:

(declare-const x Int)
  (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
             (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
                                      (and (<= (- 4 x.1) 0) 
                                           (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))

我得到的解决方案是:

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= …

也许我错过了什么,但是使用z3 C++ API构建if-then-else表达式的方法是什么？

我可以使用C API,但我想知道为什么C++ API中没有这样的函数.

问候,朱利安

如何检索枚举变量的值v ？例如，

vTyp, (val1,val2,val3) = EnumSort('vTyp',['val1','val2','val3'])
v = Const('my variable',vTyp)

现在，由于只是上面的变量v，我将如何检索值的列表 [val1,val2,val3]中v（这里val1,val3,val3是表达如上）？

我试过了，[v.sort().constructor(0), ...(1), ...(2)] 但是构造方法没有返回表达式。

自升级到Z3(最新的git master)的开源版本以来,我注意到使用C API(从2-122s开始)重复运行几乎相同的SMT查询之间存在显着的时序差异.查询之间的唯一区别是数组的命名(在QF_AUFBV逻辑中).

我们按如下方式分配数组:

Z3_symbol s = Z3_mk_string_symbol(z3_context, arrayName);
Z3_mk_const(z3_context, s,
            Z3_mk_array_sort(z3_context, getSort(32), getSort(8)));

下面是一个示例查询(转换为SMT-LIB).将"arr51"替换为其他名称(例如,"a"或"arr51_0x2628008")会显着改变查询的持续时间,最多可达两个数量级.在不改变阵列名称的情况下重复运行不会出现明显的时序变化.

有趣的是,Z3 3.2的旧二进制版本似乎不受阵列命名的影响(并且对于我们的大多数查询运行速度更快).

(benchmark klee
:status unsat
:logic QF_AUFBV
:extrafuns ((arr51 Array[32:8]))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(let (?x23 (concat bv0[32] ?x16))
(let (?x34 (bvsub (bvadd (concat (extract[33:0] ?x23) bv0[30]) (concat (extract[35:0] ?x23) bv0[28])) (concat (extract[40:0] ?x23) bv0[23])))
(let (?x42 (bvadd (bvadd ?x34 (concat (extract[44:0] ?x23) bv0[19])) (concat (extract[45:0] ?x23) …

链接：具有Pyhton绑定的
Z3定理证明者
picosat

我已经使用Z3作为SAT求解器。对于较大的公式，似乎存在性能问题，这就是为什么我想查看picosat来查看它是否是更快的替代方案。我现有的python代码使用z3语法生成一个命题公式：

from z3 import *

import pycosat
from pycosat import solve, itersolve

#
#1 2  3  4  5  6  7   8  (variable names in picosat are numbers!)
#
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))

# formula in Z3:
f = simplify(C)

print f 

输出/结果

And(S,
    Or(Not(S), P),
    Or(Not(P), S),
    Or(Not(P), B),

    Or(Not(C), P),
    Or(Not(G), P),
    Or(Not(M), P),
    Or(Not(R), P),
    Or(Not(SN), P),
    Or(Not(B), …

我正在尝试使用Z3的HORN逻辑(set-logic HORN)对一些命令式程序进行编码,但是在定义子句时遇到了一些困难(使用SMT2).谁能告诉我在哪里可以找到Z3这个功能的良好文档来源？

Z3的算术求解器是基于DPLL(T)和Simplex(本文所述)开发的.我不明白Z3在生成冲突解释时如何执行回溯.我举个例子:

线性算术公式为:

(2x1+x2?200 OR 3x1+x2?250) AND (2x1+x2+x3?200 OR 4x1+2x2+x3?400) AND x1?50 AND x2?50 AND x3?60

断言后2x1+x2?200,2x1+x2+x3?200,x1?50,x2?50和x3?60先后,它产生冲突的解释集{2x1+x2+x3?200, x1?50, x2?50, x3?60}.

我的问题是,当生成此冲突集时,如何执行回溯？