(Z3Py) 检查方程的所有解 [英] (Z3Py) checking all solutions for equation

问题描述

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

In Z3Py, how can I check if equation for given constraints have only one solution?

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

If more than one solution, how can I enumerate them?

推荐答案

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

You can do that by adding a new constraint that blocks the model returned by Z3. For example, suppose that in the model returned by Z3 we have that x = 0 and y = 1. Then, we can block this model by adding the constraint Or(x != 0, y != 1). The following script does the trick. You can try it online at: http://rise4fun.com/Z3Py/4blB

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

Note that the following script has a couple of limitations. The input formula cannot include uninterpreted functions, arrays or uninterpreted sorts.

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

这篇关于(Z3Py) 检查方程的所有解的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！