Z3 Python exclude tracker variables from solution

user_8909169 0
Viewed 45

I'm using the Z3 Python API and I have the following code to get unsatisfiable cores:

for idx, constr in enumerate(z3constrs):
    solver.assert_and_track(constr, f'tracker{idx}')

However, the model's solution contains the tracker variables:

>>> print(solver.model())
[tracker71 = True,
 tracker229 = True,
 rect11_x1 = 35,
 ...]

Is there any way to remove these variables from the solution (while keeping it a ModelRef object) without running the solver twice?

z3py z3
1 Answers

Short answer: No. These variables are part of the model, and thus their presence is important when you use solver.model() result in other calls, such as m.evaluate(expr). So, you cannot "ignore" them, while still keeping the result as a ModelRef.

But you can ask the question, why do you need the result to be a ModelRef in that case? By eliminating tracker-variables, you're violating internal invariants about how the models are constructed. If your concern is simply to not display them in a model or pass around a data-structure that contains everything but trackers, then the typical thing to do is to simply create a list of pairs and use that instead. Here's an example:

from z3 import *

a = Int('a')
s = Solver()
s.assert_and_track(a > 3, 'tracker1')
s.check()
m = s.model()
clean_m = []
for d in m.decls():
    if not(d.name().startswith("tracker")):
       clean_m += [(d, m[d])]
print(m)
print(clean_m)

This prints:

[tracker1 = True, a = 4]
[(a, 4)]

Obviously, you can post-process the results further to shape them in any-way you want.

user_9363100
Related