2

我正在使用 Z3 Python 接口作为我正在编写的研究工具的一部分，当我在同一个查询上重复运行 Z3 求解器时，我注意到一些非常奇怪的行为：特别是，我似乎每次都没有得到相同的结果，即使我在运行前明确重置了求解器。作为参考，这是我的代码：

import z3

with open("query.smt", "r") as smt_reader:
    query_lines = "".join(smt_reader.readlines())
    for i in xrange(3):
        solver = z3.Solver()
        solver.reset()

        queryExpr = z3.parse_smt2_string(query_lines)
        equivalences = queryExpr.children()[:-1]
        for equivalence in equivalences:
            solver.add(equivalence)

        # Obtain the Boolean variables associated with the constraints.
        constraintVars = [equivalence.children()[0] for equivalence
                          in equivalences]
        # Check the satisfiability of the query.
        querySatResult = solver.check(*constraintVars)

        print solver.model().sexpr()
        print solver.statistics()
        print ""

上面的代码三次重新创建 Z3 求解器并检查同一查询的可满足性。查询位于此处。

虽然上面的代码部分并不是我将如何使用 Z3 Python 接口，但问题源于一个认识，即 Z3 求解器在同一查询的代码的不同点被调用两次时，会返回不同的结果。我想知道这是否是故意的，是否有任何方法可以禁用它或确保确定性。

4

1 回答 1

3

我假设不同的意思是不同的模型。如果结果从 sat 变为 unsat，则这是一个错误。

话虽如此，如果我们在同一个执行路径中两次解决同一个问题，那么 Z3 可以产生不同的模型。Z3 将内部唯一 ID 分配给表达式。内部 ID 用于打破 Z3 使用的一些启发式方法中的联系。请注意，程序中的循环正在创建/删除表达式。因此，在每次迭代中，表示约束的表达式可能具有不同的内部 ID，因此求解器可能会产生不同的解决方案。

请参阅以下相关问题：

于 2013-03-31T16:38:44.993 回答