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

Question

Is there a way to prevent the Z3 solver from binding (=interpreting) certain variables (=constants) when satisfiability is checked?

For example, in the following C# program two different interpretations are possible:

1. switch1=true and CONST1=16, or
2. switch2=true and 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)));

`

Question: Is there a natural way to make the second interpretation (switch2=true) invalid such that it will not show up when iterating over all interpretations.

I've tried to make rax0 inconsistent by asserting ctx.MkEq(rax0, ctx.MkBVAND(ctx.MkBV(0, 64), ctx.MkBV(0xFFFFFFFFFFFFFFFF, 64)) but that didn't help.

I could check whether interpretations use rax0 somehow, but i don't know how to test that. I guess it would have been better that such interpretations were made invalid.

Answer 1

A model/interpretation is typically defined as a total map from symbols to values; it therefore seems a bit surprising if one could tell the solver to not include certain symbols in the assignment.

Here is an idea, though: I interpret your goal of finding models that "ignore" certain symbols as finding models which remain models regardless of which (other) values one would assign to the symbols of interest. That is, models that work for all values of these symbols. Hence, you universally quantify over these symbols and then ask the solver for satisfiability.

Consider this example:

(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)

It admits several models, e.g. i1 = 0, i2 = 0, !b1, !b2. If you want to enforce models that "ignore" i1, i.e. which are models regardless of the value of i1, then simply quantify over i1:

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

The only way of satisfying these constraints is satisfying the first disjunct, for which the value of i1 is irrelevant. Indeed, adding (assert b1) to above program makes it unsatisfiable: there are no models left in which i1 can be ignored.

Quantifying over i2, on the other hand, leaves the solver with a greater choice of potential models: those in which i1 is irrelevant (because !b1) and those in which i1 is positive.