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

只要不在SAT和UNSAT之间就同一问题进行切换，这不是一个错误。

您链接的答案之一解释了正在发生的事情：

Randomness in Z3 Results

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

也许当它解析它分配相同的id时，而API可能会有所不同，尽管我发现有点难以置信......

如果您需要这种行为并且您确定它是通过SMT编码执行此操作，则始终可以从API打印表达式然后解析它们。

Answer 2

我想我发现了代码的特定部分产生了这些奇怪的相反行为。也许周围的Z3专家可以告诉我，如果我完全错了。

首先，如果我在程序的单次运行中尝试相同的代码（无论是手动生成的代码还是使用API​​生成的代码）两次，我有时会得到不同的模型。这是我以前没有注意到的，这对我来说实际上并不是一个真正的问题。

然而，我主要担心的是如果我运行我的程序两次，在两次运行期间检查完全相同的代码会发生什么。

当我手动生成代码时，我最终会得到如下函数定义：

(declare-fun var!0 () Int)
(declare-fun var!2 () Int)
(declare-fun var!42 () Int)

(assert (and
    (or (= var!0 0) (= var!0 1))
    (or (= var!2 0) (= var!2 1))
    (or (= var!42 0) (= var!42 1))
))

(define-fun fun ((i! Int)) Int
    (ite (= i! 0) var!0
        (ite (= i! 1) var!2
            (ite (= i! 2) var!42 -1)
        )
    )            
)

据我所知（以及我所读到的内容（请参阅here）），API无法处理我定义“有趣”功能的方式。所以我用API来定义它是这样的：

(declare-fun var!0 () Int)
(declare-fun var!2 () Int)
(declare-fun var!42 () Int)

(assert (and
    (or (= var!0 0) (= var!0 1))
    (or (= var!2 0) (= var!2 1))
    (or (= var!42 0) (= var!42 1))
))

(declare-fun fun (Int) Int)
(assert (forall
    ((i! Int))
    (ite (= i! 0) (= (fun i!) var!0)
        (ite (= i! 1) (= (fun i!) var!2)
            (ite (= i! 2) (= (fun i!) var!42) (= (fun i!) -1))
        )
    )
))

似乎使用第一种方法，检查不同运行的相同代码总是（或至少经常对我来说不是真正的问题）给出相同的模型。

使用第二种方法，检查不同运行的相同代码通常会给出不同的模型。

任何人都可以告诉我，如果Z3实际上是如何工作的，我确实有一些逻辑吗？

因为我需要我的结果尽可能重现，所以我回到手动代码生成，它似乎工作得非常好。我很乐意在API中看到一个函数，允许我们直接定义函数，而不必使用“forall”方法，看看我刚才描述的是不是真的。