Do not assign concrete values to symbols

Question

I use Z3 to solve some constraint.

I invented an expression "x^m@mx where x noteq T". Someone provides "S^a".

We know "x^m@mx where x noteq T" can start with "S^a", on the condition that "x=S,a=m, x noteq T ".

Since this condition is satisfiable, "x^m@mx where x noteq T" will evaluate to "S^a@aS" by applying the condition.

So, I want to use Z3 to check if the conditions are satisfiable.

var ctx = new Context();

EnumSort domain = ctx.MkEnumSort("domain", new string[] { "S", "T"});

var x = ctx.MkConst("x", domain);
var m = ctx.MkConst("m", domain);
var a = ctx.MkConst("a", domain);

var solver = ctx.MkSolver();
solver.Add(ctx.MkEq(x, domain.Const(0))); // x=S
solver.Add(ctx.MkEq(a, m)); // a=m
solver.Add(ctx.MkNot(ctx.MkEq(x, domain.Const(1)))); // x noteq T

if (solver.Check() == Status.SATISFIABLE)
{
    Console.WriteLine(solver.Model);
}
else
    Console.WriteLine("Not satisfiable");

The model is m=S, a=S, x=S. This is wrong because my expression will step to "S^S@SS"

I want to leave a unassigned because later users can provide concrete values for a.

So how do I stop Z3 from assigning values to a?

It's OK to show me Python code.

Answer 1

Your question is rather confusing: What constraints are you trying to satisfy exactly? But, in general, SMT solvers do not calculate symbolic models. That is, when they determine sat, then there's an assignment to all the variables. (Note that if a particular choice isn't forced on a variable, then they'll take one of the possible values.)

So, if you don't want a to receive value, do not make it a parameter of your system:

from z3 import *

domain, (S, T) = EnumSort('domain', ('S', 'T'))

x = Const('x', domain)
m = Const('m', domain)

s = Solver()
s.add(x == S)
s.add(x != T)

if s.check() == sat:
    print(s.model())
else:
    print("Unsat")

Of course, the above is rather pointless: If you have s.add(x == S), then s.add(x != T) is irrelevant since x == S automatically implies x != T for an enumerated type.