ForAll in Z3.py

Question

I have a question about the using of ForAll in Z3.py. I want to create a local variable in ForAll declaration as follows:

A = DeclareSort('A')
a0,a1,a2,a3 = Consts('a0 a1 a2 a3', A)

s = Solver()
f = Function('f', A, A, BoolSort())
s.add(ForAll ([a0],(f(a0, a0))))

print (s.check())
print (s.model())

The result should be applied to all Consts except a0 as it is a local variable in the ForAll but the model shows the solution apply to all Consts including a0.

Creating local variable is possible in SMT but not in python.

Can anyone help?

Answer 1

Here is what the model provides:

sat
[elem!0 = A!val!0, f = [else -> True]]

It introduces a single element called "elem!0" having a unique value "A!val!0" (this is Z3's way to generate fresh values"). The interpretation of f is given such that f is always true.

If you want to quantify on variables not listed in a list, then you should walk the formula being quantified over and collect variables that are not included in a set. There are three cases to consider when walking an expression: It can satisfy one of the following properties:

 is_quantifier(e), is_app(e), is_var(e)

An expression 'e' is an uninterpreted constant if is_app(e) is True, the number of children is 0 (len(e.children()) == 0), and furthermore when accessing e.decl().kind() you obtain an uninterpreted kind.

You can use "e.get_id()" to retrieve a unique identifier corresponding to an expression. This can be used in python maps (you can't use expressions themselves as keys in python maps because equality is overloaded to construct new expressions for checking semantic equality of expressions, rather than checking syntactic equality of expressions).