Mirrors/hacktricks
2
0
Fork 0
mirror of https://github.com/carlospolop/hacktricks synced 2024-12-04 18:40:54 +00:00
Code Issues Projects Releases Packages Wiki Activity
hacktricks/reversing/reversing-tools-basic-methods/satisfiability-modulo-theories-smt-z3.md
Translator workflow a21a0e7217 Translated to Chinese
2023-08-03 19:12:22 +00:00

12 KiB
Raw Blame History

☁️ HackTricks 云 ☁️ -🐦 推特 🐦 - 🎙️ Twitch 🎙️ - 🎥 Youtube 🎥

非常基本地说，这个工具将帮助我们找到需要满足一些条件的变量的值，手动计算这些值将会非常麻烦。因此，你可以告诉 Z3 变量需要满足的条件，它将找到一些值（如果可能的话）。

基本操作

布尔值/与/或/非

#pip3 install z3-solver
from z3 import *
s = Solver() #The solver will be given the conditions

x = Bool("x") #Declare the symbos x, y and z
y = Bool("y")
z = Bool("z")

# (x or y or !z) and y
s.add(And(Or(x,y,Not(z)),y))
s.check() #If response is "sat" then the model is satifable, if "unsat" something is wrong
print(s.model()) #Print valid values to satisfy the model

整数/简化/实数

SMT（Satisfiability Modulo Theories）求解器Z3支持整数、简化和实数。这些功能使得Z3成为一个强大的工具，用于解决与整数和实数相关的问题。

整数

Z3可以处理整数变量和整数表达式。它支持整数的基本运算，如加法、减法、乘法和除法。此外，Z3还支持比较运算符，如等于、不等于、大于、小于、大于等于和小于等于。

简化

Z3的简化功能可以对表达式进行简化，以得到等价但更简洁的表达式。这对于优化和简化复杂的数学表达式非常有用。

实数

除了整数，Z3还支持实数。它可以处理实数变量和实数表达式，并支持实数的基本运算和比较运算符。

总之，Z3的整数、简化和实数功能使其成为一个强大的工具，用于解决与整数和实数相关的问题。

from z3 import *

x = Int('x')
y = Int('y')
#Simplify a "complex" ecuation
print(simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
#And(x >= 2, 2*x**2 + y**2 >= 3)

#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
#so you can get the decimals you need from the solution
r1 = Real('r1')
r2 = Real('r2')
#Solve the ecuation
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
#Solve the ecuation with 30 decimals
set_option(precision=30)
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))

打印模型

To print the model generated by Z3, you can use the model method. This method returns a string representation of the model.

要打印Z3生成的模型，可以使用model方法。该方法返回模型的字符串表示形式。

print(s.model())

The output will display the values assigned to each variable in the model.

输出将显示模型中每个变量被赋予的值。

[x = 1, y = 2, z = 3]

You can also access the individual values of the variables using the eval method.

您还可以使用eval方法访问变量的各个值。

x_value = s.model().eval(x)
y_value = s.model().eval(y)
z_value = s.model().eval(z)

This allows you to retrieve and use the values of the variables in your program.

这样可以在程序中检索和使用变量的值。

from z3 import *

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
s.check()

m = s.model()
print ("x = %s" % m[x])
for d in m.decls():
print("%s = %s" % (d.name(), m[d]))

机器算术

现代CPU和主流编程语言使用固定大小的位向量进行算术运算。在Z3Py中，机器算术可用作位向量。

from z3 import *

x = BitVec('x', 16) #Bit vector variable "x" of length 16 bit
y = BitVec('y', 16)

e = BitVecVal(10, 16) #Bit vector with value 10 of length 16bits
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print(simplify(a == b)) #This is True!
a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
print(simplify(a == b)) #This is False

有符号/无符号数

Z3提供了特殊的有符号版本的算术操作，其中位向量被视为有符号或无符号是有区别的。在Z3Py中，运算符**<, <=, >, >=, /, % 和 >>对应于有符号版本。相应的无符号运算符是ULT, ULE, UGT, UGE, UDiv, URem 和 LShR**。

from z3 import *

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)
solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)
solve(x < 0)

# using unsigned version of <
solve(ULT(x, 0))

函数

解释函数，例如算术函数，其中函数 +具有固定的标准解释（它将两个数字相加）。未解释函数和常量是最大灵活性的；它们允许与函数或常量的约束一致的任何解释。

例如：将 f 应用两次于 x 的结果再次为 x，但将 f 应用一次于 x 的结果与 x 不同。

from z3 import *

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
s.check()
m = s.model()
print("f(f(x)) =", m.evaluate(f(f(x))))
print("f(x)    =", m.evaluate(f(x)))

print(m.evaluate(f(2)))
s.add(f(x) == 4) #Find the value that generates 4 as response
s.check()
print(m.model())

示例

数独求解器

from z3 import *

def solve_sudoku(grid):
    # 创建一个9x9的整数变量矩阵
    X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
          for i in range(9) ]

    # 每个单元格的值在1到9之间
    cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
                 for i in range(9) for j in range(9) ]

    # 每行的值唯一
    rows_c   = [ Distinct(X[i]) for i in range(9) ]

    # 每列的值唯一
    cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
                 for j in range(9) ]

    # 每个3x3的子网格中的值唯一
    cells_c += [ Distinct([ X[3*i0 + i][3*j0 + j]
                           for i in range(3) for j in range(3) ])
                 for i0 in range(3) for j0 in range(3) ]

    # 已知的单元格的约束
    sudoku_c = [ If(grid[i][j] == 0, True, X[i][j] == grid[i][j])
                 for i in range(9) for j in range(9) ]

    # 创建求解器对象
    s = Solver()

    # 添加所有约束
    s.add(cells_c + rows_c + cols_c + cells_c)

    # 求解数独
    if s.check() == sat:
        m = s.model()
        r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
              for i in range(9) ]
        return r
    else:
        return None

# 数独问题
grid = [ [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ],
         [ 0, 0, 0, 0, 0, 0, 0, 0, 0 ] ]

# 解决数独问题
solution = solve_sudoku(grid)

# 打印解决方案
if solution is not None:
    for row in solution:
        print(row)
else:
    print("No solution found")

这是一个使用Z3求解数独问题的示例。它通过创建一个9x9的整数变量矩阵来表示数独的单元格，并添加约束条件来确保每个单元格的值在1到9之间，并且每行、每列以及每个3x3的子网格中的值都是唯一的。然后，它根据已知的单元格的约束条件，使用Z3求解器来求解数独问题。如果存在解决方案，则打印解决方案；否则，打印"无解"。

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
(0,0,0,5,1,0,0,0,7),
(0,8,9,0,0,0,0,4,0),
(0,0,0,0,0,0,2,0,8),
(0,6,0,2,0,1,0,5,0),
(1,0,2,0,0,0,0,0,0),
(0,7,0,0,0,0,5,2,0),
(9,0,0,0,6,5,0,0,0),
(0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print "failed to solve"

参考资料

☁️ HackTricks 云 ☁️ -🐦 Twitter 🐦 - 🎙️ Twitch 🎙️ - 🎥 Youtube 🎥