(Z3Py) 检查方程的所有解

Posted 2023-02-25

【中文标题】(Z3Py) 检查方程的所有解

【英文标题】：(Z3Py) checking all solutions for equation

【发布时间】：2012-08-05 17:53:44

【问题描述】：

在 Z3Py 中，如何检查给定约束的方程是否只有一个解？

如果有多个解决方案，我该如何列举它们？

【参考方案1】：

您可以通过添加一个阻止 Z3 返回的模型的新约束来做到这一点。 例如，假设在 Z3 返回的模型中，我们有 x = 0 和 y = 1。然后，我们可以通过添加约束Or(x != 0, y != 1) 来阻止这个模型。 以下脚本可以解决问题。 您可以在线试用：http://rise4fun.com/Z3Py/4blB

请注意，以下脚本有一些限制。输入公式不能包含未解释的函数、数组或未解释的排序。

from z3 import *

# Return the first "M" models of formula list of formulas F 
def get_models(F, M):
    result = []
    s = Solver()
    s.add(F)
    while len(result) < M and s.check() == sat:
        m = s.model()
        result.append(m)
        # Create a new constraint the blocks the current model
        block = []
        for d in m:
            # d is a declaration
            if d.arity() > 0:
                raise Z3Exception("uninterpreted functions are not supported")
            # create a constant from declaration
            c = d()
            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                raise Z3Exception("arrays and uninterpreted sorts are not supported")
            block.append(c != m[d])
        s.add(Or(block))
    return result

# Return True if F has exactly one model.
def exactly_one_model(F):
    return len(get_models(F, 2)) == 1

x, y = Ints('x y')
s = Solver()
F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x]
print get_models(F, 10)
print exactly_one_model(F)
print exactly_one_model([x >= 0, x <= 1, y >= 0, y <= 2, 2*y == x])

# Demonstrate unsupported features
try:
    a = Array('a', IntSort(), IntSort())
    b = Array('b', IntSort(), IntSort())
    print get_models(a==b, 10)
except Z3Exception as ex:
    print "Error: ", ex

try:
    f = Function('f', IntSort(), IntSort())
    print get_models(f(x) == x, 10)
except Z3Exception as ex:
    print "Error: ", ex

【讨论】：

我也想问一下，Z3的SMT语言扩展也可以吗？

不，不是。不过，我认为在 SMT 2.0 前端添加这个命令是个好主意。

您能否添加注释来解释为什么使用此方法不支持未解释的函数和数组？这是一个偶然的限制（数据结构不是 ExprRefs 之类的）还是一个更基本的限制？

【参考方案2】：

下面的 python 函数是包含常量和函数的公式模型的生成器。

import itertools
from z3 import *

def models(formula, max=10):
    " a generator of up to max models "
    solver = Solver()
    solver.add(formula)

    count = 0
    while count<max or max==0:
        count += 1

        if solver.check() == sat:
            model = solver.model()
            yield model
            
            # exclude this model
            block = []
            for z3_decl in model: # FuncDeclRef
                arg_domains = []
                for i in range(z3_decl.arity()):
                    domain, arg_domain = z3_decl.domain(i), []
                    for j in range(domain.num_constructors()):
                        arg_domain.append( domain.constructor(j) () )
                    arg_domains.append(arg_domain)
                for args in itertools.product(*arg_domains):
                    block.append(z3_decl(*args) != model.eval(z3_decl(*args)))
            solver.add(Or(block))

x, y = Ints('x y')
F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x]
for m in models(F):
    print(m)

【讨论】：

对于一般用途，我会将公式增强求解器传递给 models() 而不是公式，并使用 push/pop 包装 while 循环。

【参考方案3】：

引用http://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t))
    def fix_term(s, m, t):
        s.add(t == m.eval(t))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()   
    yield from all_smt_rec(list(initial_terms))  

这确实比莱昂纳多自己的答案表现得更好（考虑到他的答案已经很老了）

start_time = time.time()
v = [BitVec(f'vi',3) for i in range(6)]
models = get_models([Sum(v)==0],8**5)
print(time.time()-start_time)
#211.6482105255127s

start_time = time.time()
s = Solver()
v = [BitVec(f'vi',3) for i in range(6)]
s.add(Sum(v)==0)
models = list(all_smt(s,v))
print(time.time()-start_time)
#13.375828742980957s

据我观察，将搜索空间分成不相交的模型会产生巨大的差异

【讨论】：

很棒的发现！这在我的实验中也确实快了很多。

次要问题：使用yield from … 而不是for x in …: yield x。

请注意，该论文中all_smt 的实现存在一个错误。有关修复，请参阅 github.com/Z3Prover/z3/issues/5765#issuecomment-1009135689。

【参考方案4】：

Himanshu Sheoran给出的答案引用了论文https://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations

不幸的是，当时论文中给出的实现中存在一个错误，该错误在该答案中被引用。该功能已被更正。

为了后代，这是代码的正确版本：

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()   
    yield from all_smt_rec(list(initial_terms))

【讨论】：

yield from all_smt_rec(terms[i+1:]) 不正确，应该是 yield from all_smt_rec(terms[i:]) 我在 Nikolaj 之前的实现中也指出了这个错误。保持直到 i 的所有项都相同，[i:] 因为我们仍然需要改变并找到 term[i] term[i+1:] 的所有解决方案，本质上意味着我们只对 term[i 进行一次分配] 保持所有术语[:i] 固定

好收获！已更正。