标签: z3py

我在 Z3 python 中有这个代码：

x = Bool('x')
y = Bool('y')
z = Bool('z')
z == (x xor y)
s = Solver()
s.add(z == True)
print s.check()

但是此代码在运行时报告以下错误：

c.py(4): error: invalid syntax

如果我替换xor为and，则没有问题。所以这意味着不支持异或？

多年来,我一直在追踪解决技术的问题 - 我还有一篇关于将它们应用于特定难题的博客文章 - "穿越梯子".

为了达到目的,我偶然发现了z3,并尝试将其用于特定问题.我使用了Python绑定,并写了这个:

$ cat  laddersZ3.py
#!/usr/bin/env python
from z3 import *
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
solve(
    a>0, a<200,
    b>0, b<200,
    c>0, c<200,
    d>0, d<200,
    e>0, e<200,
    f>0, f<200,
    (e+f)**2 + d**2 == 119**2,
    (e+f)**2 + c**2 == 70**2,
    e**2 + 30**2 == a**2,
    f**2 + 30**2 == b**2,
    a*d == 119*30,
    b*c == 70*30,
    a*f - 119*e + a*e == …

理想情况下,可以将'或'两个数字表示为位向量,但我无法做到.请告诉我们代码中是否有错误或其他错误

line1 = BitVec('line1', 1)
line2 = BitVec('line2', 1)
s = Solver()
s.add(Or(line1, line2) == 0)
print s.check()

给出的错误是

error: 'type error'
WARNING: invalid function application for or, sort mismatch on argument at position 1,         expected Bool but given (_ BitVec 1)
WARNING: (declare-fun or (Bool Bool) Bool) applied to: 
line1 of sort (_ BitVec 1)
line2 of sort (_ BitVec 1)

从这个错误我明白,或者只能为bool变量做.我的问题是如何或为BitVectors

p = Int('p')
q = Int('q')

s = Solver()
s.add(1<=p<=9, 1<=q<=19, 5<(3*p-4*q)<10)
s.check() 
print s.model()

返回sat,并给出解决方案

[p = 0, q = 0]

这不符合约束.如果我删除最后的约束,它将返回一个满足前两个(平凡)约束的合理对.这是怎么回事？

永久链接在线试用:http://rise4fun.com/Z3Py/fk4

编辑:我是z3的新手,所以有可能我做了一些可怕的错误,让我知道.

我正在学习 Z3 求解器。我有一个关于数组和相关条件的问题。特别是，我必须创建 Z3py 代码来解决以下 if 条件：

totalAccounts = [ 1, 2, 3, 4, 5 ]    

def (myAccounts):
   cnt = len(myAccounts)
   if (cnt > 10) doSomething()

myAccounts是一个整数列表，是列表的子集totalAccounts。通过的条件cnt > 10取决于列表的长度myAccounts。

我想我需要表示为 Z3 的数组并使用函数myAccounts复制其中的值。totalAccountsStore

MYACCOUNTS = Array ('MYACCOUNTS', IntSort(), IntSort())
I = Int('I')
i = 0
for elem in totalAccounts:
  MYACCOUNTS = Store(MYACCOUNTS, i, elem)
  i = i + 1

但我不知道如何在创建添加到求解器的条件时表示此类数组的长度：

solver = Solver()
solver.add( ??? > 10 )

我做对了吗？

考虑证明以下 while 循环的正确性，即我想表明，给定循环条件开始时，它最终将终止并导致最终断言为真。

int x = 0;
while(x>=0 && x<10){
   x = x + 1;
}
assert x==10;

在不使用循环展开的情况下，用于检查正确性的 SMT-LIB 的正确翻译是什么？

我的问题是“Distinct”在 z3 python 中有效吗？。我比较了以下代码，但似乎没有给出相同的结果：

(declare-const x Int)
(declare-const y Int)
(assert (distinct x y))
(check-sat)
(get-model)

结果是：

sat

  (model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    1)
  )

我添加了否定断言只是为了测试，结果未满足，这是正确的：

(assert (= x y))

unsat
Z3(6, 10): ERROR: model is not available

但是当我在 python 中使用 z3 时，它总是给我如下所示：

x = Int('x')
y = Int('y')
Distinct(x, y)
s = Solver
s = Solver() 
s.check()

当我添加以下断言时，它应该给我 unsat 但它返回 sat：

s.add(x == y)
[y = 0, x = 0]

这是否意味着我使用了错误的语法？

我需要 z3 中的一些临时变量，我不需要计算值，只需要检查它是否存在就足够了。

这是我正在做的（简单形式）：

import z3

def maj(a, b, c):
    return (a & b) ^ (a & c) ^ (b & c)

def func(a, b, c):
    a = z3.RotateRight(a, 5) ^ z3.BitVecVal(0xafaf, 16)
    b = z3.RotateRight(b, 2) ^ z3.RotateRight(b, 7)
    c = z3.RotateRight(c, 11) ^ z3.LShR(c, 3)
    return a + c, b + c, maj(a + b, a + c, b + c)

solver = z3.SolverFor('QF_BV')
some_var = 0x0000
_x = z3.BitVec('x', 16)
x = _x
y = z3.BitVecVal(some_var, 16) …