创建所有令人满意的模型，Z3 .Net API答案

【问题标题】：Creating all satisfying models, Z3 .Net API创建所有令人满意的模型，Z3 .Net API
【发布时间】：2017-07-12 12:30:38
【问题描述】：

我正在使用 Z3 .Net API。我有一段简单的代码，我想在其中创建所有令人满意的模型。代码是这样的：

    Solver solver = ctx.MkSolver();

    Expr x = ctx.MkConst("x", ctx.MkBoolSort());
    Expr y = ctx.MkConst("y", ctx.MkBoolSort());

    BoolExpr constraint1 = ctx.MkBoolConst("Constraint1");
    solver.AssertAndTrack(ctx.MkOr((BoolExpr)x, (BoolExpr)y), constraint1);

问题是，稍后在代码中，当我想枚举我使用此代码的所有模型时：

        Model resultModel = pSolver.Model;
        Console.WriteLine("x = {0}, y = {1}",
            resultModel.Evaluate(pX),
            resultModel.Evaluate(pY));

但也有一些模型，例如 if (X = true) then (Y = Y)。对于这些情况，我想表明实际上有两种模型，例如：

X = true, Y = true
X = true, Y = false

API 中是否有可以给我这些答案的功能，或者我应该使用内部编码来获得这些答案。

【问题讨论】：

标签： z3

【解决方案1】：

一般来说，不。至少不是以 SMT-Lib 认可的方式。当求解器呈现模型时，它们总是与基本值相关联，并且 SMTLib 不提供任何“最小”模型的规定。请注意，这里的最小含义也不清楚：在您的示例中，x 和y 就足够了，并且在另一个之前修复一个会影响其他变量的选择。您希望求解器更喜欢哪一个？

如果您对此类最小模型感兴趣，基于 BDD 的求解器是您的朋友。由于您在 BDD 中修复了变量顺序，因此您可以根据该变量顺序轻松读取“最小”模型。但是 SMT 求解器通常不会公开这些细节，如果他们有这样的引擎，它们也不会让您轻松访问。在 Z3 的特殊情况下，您可能想在https://github.com/Z3Prover/z3/issues 询问是否有低级 API 来获得更有用的东西；但是获得这样的“符号”模型并不是 SMT 求解器通常提供的。

【讨论】：