[SMT-LIB] Some problem with ForAll quantifier in my SMT formula

[Adrien Champion]

Hi Jun, Morgan and Nikolaj,

In this latest version, you are checking the satisfiability of the 
formula
g = ( exists a, ( (c=b) and (d=a*c) ) => (d=b) ).
So you are asking the question "does there exist values for the free 
variables
of g such that g evaluates to true?".
Variable a is quantified so it is not part of the model in theory, 
hence the
"None".

Unless I'm mistaken, in which case I hope someone will correct me,
z3 does give you a value for it via a!0. I guess this is
because g is equisatisfiable with h = ( (c=b) and (d=a!0*c) ) => (d=b). 
So z3
works on h instead of g and gives you the model it found for h (any 
model of h
is also a model of g on the set of variables {b,c,d,a!0}, while the 
opposite is
not true).
What happens is that the model z3 finds makes f (with a!0 instead of a) 
evaluate
to false since (d = a!0 * c) is (1 = 0 * 0) i.e. false.
Since false implies anything (f => d=b) is true -- b does not even need 
to be
valuated, which is why it does not appear in the model.

Anyway, it seems the question you want to ask is
"does there exist a value for variable a such that for all b, c and d,
(f => d=b) holds?".
So what you need to do is change
> s.add(Exists(a, Implies(f, d == b)))
to
> s.add(ForAll([b,c,d], Implies(f, d == b)))

In SMT lib, it looks like this
> (set-logic BV)
> (declare-fun a () (_ BitVec 32))
>
> (assert (forall (
>   (b (_ BitVec 32)) (c (_ BitVec 32)) (d (_ BitVec 32))
> ) (=>
>     (and (= c b) (= d (bvmul a c)))
>     (= d b)
>   )
> ))
>
> (check-sat)
> (get-model)

which, when fed to z3, yields
> sat
> (model
>   (define-fun elem!3 () (_ BitVec 32)
>     #x00000002)
>   (define-fun a () (_ BitVec 32)
>     #x00000001)
> )

Although I'm not sure what elem!3 is here, it looks closer to what you
are looking for.

I hope this helps.

Best,

-- 
Adrien Champion
PhD candidate
Onera / Rockwell Collins France
http://www.onera.fr/staff-en/adrien-champion/
adrien.champion at onera.fr
Onera: +33 (0)5 62 25 26 54
RCF: +33 (0)5 61 71 77 00