Z3 的使用

未解释的常量

Z3的常量类型4种 ：Int、Real、Bitvec、bool

创建变量：

a = Int('a')  #创建单个整形
a, b, c = Ints('a b c') #创建多个整形
a = Real('a')  #实数
a = Bool('a')
a = BitVec('a', 32)  #32位向量

创建常量列表：

IntVector(name, sz, ctx=none) #Return a list of integer constants of size `sz`.
RealVector(name, sz, ctx=none) #Return a list of real constants of size `sz`.
BoolVector(name, sz, ctx=none) #Return a list of bool constants of size `sz`.

他们的函数原型：

def IntVector(prefix, sz, ctx=None):
     ctx = _get_ctx(ctx)
     return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]

def RealVector(prefix, sz, ctx=None):
     ctx = _get_ctx(ctx)
     return [Real("%s__%s" % (prefix, i), ctx) for i in range(sz)]

def BoolVector(prefix, sz, ctx=None):
     ctx = _get_ctx(ctx)
     return [Bool("%s__%s" % (prefix, i), ctx) for i in range(sz)]

从函数原型稍微改变一下，就可以写出一个创建矩阵的语句：

def IntMatrix(prefix, sz):
     return [[Int("%s__%s__%s" % (prefix, j, i)) for i in range(sz)] for j in range(sz)]

整形常量

给整形常量赋值

>>> x, y = Ints('x y')
>>> x = IntVal(5)
>>> y = 5
>>> x.sort()
Int
>>> y.sort()
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: 'int' object has no attribute 'sort'
>>> type(y)
<class 'int'>
>>> type(x)
<class 'z3.z3.IntNumRef'>

实数常量

给实数常量赋值：

用RealVal()函数：

#Return a Z3 real value.
#`val` may be a Python int, long, float or string representing a number in decimal or rational notation.
#If `ctx=None`, then the global context is used.
#`val` 可以是 Python int、long、float 或 string，以十进制或有理数表示数字。
#如果 `ctx=None`，则使用全局上下文。

>>> RealVal(1)
1
>>> RealVal(1).sort()
Real
>>> RealVal("3/5")
3/5
>>> RealVal("1.5")
3/2

>>> x = Real('x')
>>> x = 1/3
>>> x
0.3333333333333333
>>> type(x)
<class 'float'>

位向量（Bit-Vector）

在z3中只有BitVec类型的常量才可以进行机器运算（位运算），在移位的时候不会像python中的变量一样多出一位或 少一位。

给位向量的常数赋值：

>>> y = BitVec('y', 4)
>>> y = BitVecVal(15, 4)
>>> y
15
>>> y.sort()
BitVec(4)

布尔（bool）

对于布尔类型常量的运算有and or xor not

from z3 import *
p, q = Bools('p q')
s = Solver()
s.add(Or(p, q), 
      Or(Not(p), q), 
      Or(Not(p), Not(q)))
print(s.check())
print(s.model())

与之对应的公式：$(p \lor q) \land (\lnot p \lor q) \land (\lnot p \lor \lnot q)$

也就是离散数学里的哪些基础运算

变量（variable）

z3对于变量(variable)的定义以及创建变量：

#Create a Z3 free variable. Free variables are used to create quantified formulas.
#创建一个 Z3 自由变量。 自由变量用于创建量化公式。

>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))
False

而之前的Int、Real、Bit-Vecotr、bool在官方的文档中用的词都是constant(常量)。

至于这个quantified formulas是什么还在学习中。。。。。

求解器（Solver）

创建一个求解器

s = Solver()

给求解器添加约束条件（assertion）

insert

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]

add

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]

append

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]

其实这三个方法的定义完全一样的。。。。

def append/add/insert(self, *args):
        self.assert_exprs(*args)

看到>>> s [x > 0, x < 2]，solver中是使用列表来存放约束条件的，所以可以把一部分或者全部的约束条件先保存在一个列表中，最后一下子全添加到solver中：

>>> a, b = Ints('a b')
>>> s = Solver()
>>> m = []
>>> m += [a > b]
>>> m += [a + b == 5]
>>> s.add(m)
>>> s
[a > b, a + b == 5]

求解器去除约束条件(reset 去除所有)

Remove all asserted constraints and backtracking points created using `push()`.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]

回溯点

在网上查了很多资料，大部分说push()是搞了一个栈的结构，pop()是弹出栈，我就没搞明白，果然还是看官方文档好

Create a backtracking point.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Create a backtracking point.意为创建一个回溯点，而pop()是回溯到回溯点，个人感觉这比栈好理解多了，不然容易被汇编的pop() 出栈误导，下面是另一种实例：

>>> s.push()
>>> s.add(a > b)
>>> s.add(b > 3, a + b == 5)
>>> s
[a > b, b > 3, a + b == 5]
>>> s.pop()
>>> s
[]

满足（satisfied）与不满足（unsatisfied）

用check()看是否有解，若有解用model()输出解：

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x + 5 == 3, x > 0)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(x + 5 == 3)
>>> s.check()
sat
>>> s.model()
[x = -2]

函数

不像编程语言，有副作用（side-effects）会抛出异常或者从不返回，z3中的函数没有副作用。它们定义了所有的输入值。这包括函数，比如除法。z3基于第一顺序的逻辑。

对于约束x+y>3我们说x、y是变量。在很多教材上，x、y被称作未解释的常数。也就是这个约束允许对于任意解释x+y>3恒成立。

更准确的说，函数和在第一顺序逻辑的常量符号是未解释的或自由的，也就是说没有一个被附加的先验解释。这与属于理论签名的函数相反，比如算术，函数+有一个固定的标准解释（它是两个数字的相加）。未解释函数和常数具有最大的灵活性，它们允许任何与函数或常数上的约束一致的解释。

为了说明未解释的函数和常量，让我们使用未解释的整型常量（也就是变量）x，y，最后让f是一个未解释的函数，它接收一个类型为整型（也就是sort）的参数并得到 一个整型值。

这里定义的Function可以理解为一个自定义的运算

>>> x = Int('x')
>>> y = Int('y')
>>> f = Function('f', IntSort(), IntSort())
>>> solve(f(f(x)) == x, f(x) == y, x != y)
[x = 0, y = 1, f = [1 -> 0, else -> 1]]