Z3在多次运行时生成不同的型号

Question

我已经使用Z3和JAVA绑定2年了。出于某种原因，我总是将自己的SMTLib2代码生成为String，然后使用parseSMTLib2String构建相应的Z3 Expr。据我所知，每次用这种方法输入两次完全相同的输入时，我总是得到相同的模型。

但我最近决定直接更改并使用JAVA API并使用ctx.mk...()构建表达式。基本上，我没有生成String然后解析它，但我让Z3完成了构建Z3 Expr的工作。

现在发生的事情是，当我检查解算器确实存储完全相同的代码时，我得到了不同的模型。我的JAVA代码看起来像这样：

static final Context context = new Context();
static final Solver solver = context.mkSolver();

public static void someFunction(){
    solver.add(context.mk...()); // Add some bool expr to the solver
    Status status = solver.check();
    if(status == SATISFIABLE){
        System.out.println(solver.getModel()); // Prints different model with same expr
    }
}

我在运行期间对“someFunction（）”进行了多次调用，并且检查的表达式context.mk...()发生了变化。但是如果我运行我的程序两次，则会检查相同的表达式序列，有时会从一次运行到另一次运行给出不同的模型。

我已经尝试禁用auto-config参数并设置我自己的随机种子，但Z3有时会产生不同的模型。我只使用有界整数变量和未解释函数。我是以错误的方式使用API吗？

如果需要，我可以将整个SMTLib2代码添加到这个问题中，但它并不是很短并且包含多个求解器调用（我甚至不知道哪一个会从一个执行到另一个执行产生不同的模型，我只知道一些做）。

我必须确切地说，我已经阅读了以下主题，但发现答案要么过时，要么（如果我理解正确的话）支持“Z3是确定性的并且应该为相同的输入生成相同的模型”：

Z3 timing variation

Randomness in Z3 Results

different run time for the same code in Z3

编辑：令人惊讶的是，使用下面的代码我似乎总是得到相同的模型，Z3现在似乎是确定性的。但是，与我以前的代码相比，内存消耗量很大，因为我需要将内存保留在内存中一段时间。知道我可以用更少的内存来实现相同的行为吗？

public static void someFunction(){
    Context context = new Context();
    Solver solver = context.mkSolver();
    solver.add(context.mk...()); // Add some bool expr to the solver
    Status status = solver.check();
    if(status == SATISFIABLE){
        System.out.println(solver.getModel()); // Seem to always print the same model :-)
    }
}

这是我多次调用方法“someFunction”得到的内存消耗：

Answer 1

另一答案