Z3结果的随机性

Question

我正在使用z3python接口作为我正在编写的一个研究工具的一部分，当我在同一个查询上重复运行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解算器，并检查同一查询的可满足性。查询是located here。在

虽然上面的代码部分并不完全是我将如何使用z3python接口，但问题源于这样一个认识：Z3解算器在同一个查询的不同代码点调用两次时，返回了不同的结果。我想知道这是否是故意的，是否有任何方法可以使其失效或确保确定性。在

Answer 1

我想你说的不同是指不同的型号。 如果结果从sat更改为unsat，那么它就是一个bug。在

也就是说，如果我们在同一个执行路径中解决同一个问题两次，那么Z3可以生成不同的模型。Z3为表达式分配内部唯一的id。在Z3使用的一些启发式算法中，内部id用于断开连接。请注意，程序中的循环正在创建/删除表达式。因此，在每次迭代中，表示约束的表达式可能具有不同的内部ID，因此解算器可能会生成不同的解。在

参见以下相关问题：

• Z3 timing variation