在检查可满足性时，如何防止 Z3 求解器绑定（=解释）某些变量（=常量）？

Question

有没有办法在检查可满足性时阻止 Z3 求解器绑定（=解释）某些变量（=常量）？

例如，在下面的 C# 程序中可能有两种不同的解释：

switch1=true 且 CONST1=16，或
switch2=true 和 RAX!0=16

`

Dictionary<string, string> settings = new Dictionary<string, string> {
    { "unsat-core", "true" },    // enable generation of unsat cores
    { "model", "true" },         // enable model generation
    { "proof", "false" }         // enable proof generation
};
Context ctx = new Context(settings);
Solver solver = ctx.MkSolver();

BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); // register values
BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64);
BoolExpr switch1 = ctx.MkBoolConst("switch_1_on"); // switch on/off instruction 1
BoolExpr switch2 = ctx.MkBoolConst("switch_2_on"); // switch on/off instruction 2
BitVecExpr immConst = ctx.MkBVConst("CONST1", 64); // imm const

//making rax0 inconsistent does not work
//solver.Assert(ctx.MkEq(rax0, ctx.MkBVAND(ctx.MkBV(0, 64), ctx.MkBV(0xFFFFFFFFFFFFFFFF, 64))));

// instruction 1: MOV RAX, immConst
solver.Assert(ctx.MkIff(switch1, ctx.MkEq(rax1, immConst)));

// instruction 2: NOP
solver.Assert(ctx.MkIff(switch2, ctx.MkEq(rax1, rax0)));

// atleast and atmost one instruction must be executed
solver.Assert(ctx.MkAtMost(new BoolExpr[] { switch1, switch2 }, 1));
solver.Assert(ctx.MkOr(new BoolExpr[] { switch1, switch2 }));

// after executing the ASM we want rax to be 0
solver.Assert(ctx.MkEq(rax1, ctx.MkBV(0, 64)));

`

问题：有没有一种自然的方法可以使第二个解释（switch2=true）无效，从而在遍历所有解释时不会出现。

我试图通过断言 ctx.MkEq(rax0, ctx.MkBVAND(ctx.MkBV(0, 64), ctx.MkBV(0xFFFFFFFFFFFFFFFF, 64)) 使 rax0 不一致，但这没有帮助。

我可以检查解释是否以某种方式使用 rax0，但我不知道如何测试它。我想这样的解释是无效的会更好。

Answer 1

一个model/interpretation通常被定义为从符号到值的总映射；因此，如果可以告诉求解器不要在赋值中包含某些符号，这似乎有点令人惊讶。

不过，这里有一个想法：我将您寻找 "ignore" 某些符号的模型的目标解释为寻找仍然是模型的模型，而不管人们将哪个（其他）值分配给感兴趣的符号。也就是说，适用于这些符号的所有值的模型。因此，您对这些符号进行普遍量化，然后向求解器询问可满足性。

考虑这个例子：

(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const i1 Int)
(declare-const i2 Int)

(assert
  (or ; Admits several models
    (not b1)
    (< 0 i1)
    (and b2 (= i1 i2))))

(check-sat)
(get-model)

它承认几个模型，例如。 i1 = 0, i2 = 0, !b1, !b2。如果你想强制执行 "ignore" i1 的模型，即不管 i1 的值是什么模型，那么只需量化 i1:

(assert
    (forall ((i1 Int)) 
      (or
        (not b1)
        (< 0 i1)
        (and b2 (= i1 i2)))))

满足这些约束的唯一方法是满足第一个析取，i1 的值与其无关。事实上，在上面的程序中添加 (assert b1) 会使其无法满足：没有剩余的模型可以忽略 i1。

另一方面，对 i2 进行量化，使求解器可以选择更多的潜在模型：i1 不相关的模型（因为 !b1）和i1 是正数。

在检查可满足性时，如何防止 Z3 求解器绑定（=解释）某些变量（=常量）？

How to prevent Z3 solver from binding (=interpreting) certain variables (=constants) when satisfiability is checked?

c#

z3