标签: z3

我想使用 Z3 来解决最自然地用原子（符号）、集合、谓词和一阶逻辑表达的问题。例如（伪代码）：

A = {a1, a2, a3, ...} # A is a set
B = {b1, b2, b3...}
C  = {c1, c2, c3...}

def p = (a:A, b:B, c:C) -> Bool # p is unspecified predicate
def q = (a:A, b:B, c:C) -> Bool

# Predicates can be defined in terms of other predicates:
def teaches = (a:A, b:B) -> there_exists c:C 
                            such_that [ p(a, b, c) OR q(a, b, c)  ]

constraint1 = forall b:B there_exists a:A
                         such_that …

我在UFBV查询上运行Z3.目前查询包含2个调用check-sat.如果放在Z3 push 1之后check-sat在30秒内解决查询.如果不放任何东西push 1- Z3在200秒内解决它.有趣.任何具体原因还是巧合？

z3py片段:

x = Int('x')

s = Solver()
s.add(x <= x)
print s.check()
print s.model()
print s.model().sexpr()

http://rise4fun.com/Z3Py/mfPU

输出:

sat
[]

任何值都x可以,但z3返回空模型.x模型中缺少的自由变量是否表示任何整数值都是有效模型？

我有两个使用实数的SMT2-Lib脚本,这在道德上是等价的.唯一的区别是,一个也使用位向量而另一个不使用位向量.

这是使用实数和位向量的版本:

; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite (= #b1 s1) s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite (= #b1 s0) s7 s8)))
   (let …

我仍然是Z3的新手,并且有一个问题:是否可以使用Z3进行等效性检查？

如果可能的话,你能给我一个检查2个等价公式的例子吗？

谢谢.

我是z3py的新手,正在使用Python中的Z3 API,但无法弄清楚如何定义一个bitvectors数组.

我想要的东西:

DOT__mem[16] = BitVec('DOT__mem[16]', 8)

但是这种语法不起作用,即使在本教程的练习面板上也是如此.

有人可以帮助正确的语法吗？

我正在使用Z3的python api来做一些增量求解.我迭代地将约束推送到求解器,同时使用solver.push()命令检查每个步骤的不可满足性.我想了解Z3是否会使用先前约束的学习引理或者在使用新添加的约束求解时先前获得的满意解.我从不使用solver.pop()命令.在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？

下面的Python代码段说明了Z3的存储性能行为。在不push()调用的情况下，z3会在0.1秒内检查公式。有了push()（并且没有额外的断言），z3需要0.8s。即使在交换s.append(f)和之后也会发生类似的结果s.push()。

import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)

知道为什么会出现这种减速吗？而且，如何解决？

我正在使用z3-4.3.2.bb56885147e4-x64-osx-10.9.2。

我按照说明在运行时使用Visual Studio Community 2015在64位Windows 8.1系统上构建Z3

python scripts/mk_make.py -x

但是当我运行nmake时,我收到以下错误:

C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8848): error C3861:
 '_InterlockedIncrement64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8879): error C3861:
 '_InterlockedDecrement64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8915): error C3861:
 '_InterlockedExchange64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8969): error C3861:
 '_InterlockedExchangeAdd64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8979): error C3861:
 '_InterlockedExchangeAdd64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(9026): error C3861:
 '_InterlockedAnd64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(9036): error C3861:
 '_InterlockedOr64': identifier not found
C:\Program …

我正在做一些验证工作,我将常规树语法作为基础理论.

Z3允许您使用未解释的函数定义自己的东西,但是在您的决策过程递归时,这并不能很好地工作.他们曾经允许使用插件,但我认为这已经被删除了.

我想知道,有没有人推荐过一个体面的SMT求解器,它允许你为自定义理论编写决策程序？