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

Thu Jun 20 19:20:21 EDT 2013

Hi Jun,

Morgan provided a good answer when not considering the auxiliary variables.
Some similar answers are recently provided on StackOverflow for a similar question.
With the auxiliary variables, you should be careful. The meaning of the formula you wrote
does not follow your intent when you mixed the conjunctions and universal quantifier.
In general, in logic you have the following equivalences:

	(forall ((x T)) (=> (= x t) phi[x]))
Is equivalent to
	phi[t]
where t does not contain x.

Similarly, 
	(exists ((x T)) (and (= x t) phi[x])))
Is equivalent to
	phi[t]

In your example you use universal quantifier for the auxiliary variables, but use conjunction.
This does not seem to reflect your intent. In a nutshell, you write the following:

	(forall ((x T)) (and (= x t) phi[x]))

Formulated in SMT-LIB you wrote:
	(forall ((b T) (tmp T) (a1 T)) (and (= tmp b) (= a1 (* a tmp)) (= a1 b)))

when you must have intended:
	(forall ((b T) (tmp T) (a1 T)) (=> (and (= tmp b) (= a1 (* a tmp))) (= a1 b)))

where the quantified 'b' comes from the problem you are solving, and the quantified tmp and a1
come from the auxiliary definitions.

BTW, SMT-LIB provides also let-expressions, so you can write:
	(let ((x t)) phi[x])
Similarly, when you interact with an SMT solver using a programmatic API, you can just build a
term structure corresponding to the auxiliary variables. So tools that perform symbolic execution
do not really need to introduce auxiliary variables. 

Thanks,
Nikolaj

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Adrien Champion
Sent: Thursday, June 20, 2013 12:18 PM
To: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] Some problem with ForAll quantifier in my SMT formula

Hi Jun,

To answer your second question, about the following python code

> from z3 import *
>
> a, b, a1, tmp = BitVecs('a b a1 tmp', 32)
>
> f = True
> f = And(f, tmp == b)
> f = And(f, a1 == a * tmp)
> f = And(f, a1 == b)
>
> s = Solver()
> s.add(ForAll([b, a1], f))
>
> if s.check() == sat:
>     print 'a =', s.model()[a]
> else:
>     print 'Unsat'

This is unsat since forall b, (tmp = b) is unsat: there is no concrete value for tmp for which this is true, since it must be equal to any bitvector b.
I guess you meant
> s.add(ForAll([b, a1, tmp], f))

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

On Thu, 20 Jun 2013 14:37:28 -0400, Morgan Deters wrote:
> Hi Jun,
>
> Since this involves Z3-specific functionality (the Python bindings), 
> you might try asking on stackoverflow.com and tagging with "z3":
>
>   http://stackoverflow.com/questions/tagged/z3
>
> That said, I think your encoding is not quite giving you what you 
> want.
>  You want to know if there exists an "a" such that for all "b", b = a
> * b.
>  This can be written directly, without "a1" and "tmp".  In SMT-LIB 
> syntax [*], it might look like:
>
> (declare-fun a () (_ BitVec 32))
> (assert
>   (forall ( (b (_ BitVec 32)) )
>     (= b (bvmul a b))
>   )
> )
> (check-sat)
> (get-value (a))
>
> and indeed, with this input, Z3 gives exactly what you want:
>
> sat
> ((a #x00000001))
>
> [*] Note that SMT-LIB doesn't have an "officially-specified" logic 
> that combines quantifiers and bitvectors, but some solvers, like Z3 
> and CVC4, can handle such a logic.
>
>  Morgan
>
> On Thu, Jun 20, 2013 at 11:32 AM, Jun Koi <junkoi2004 at gmail.com>
> wrote:
>
>> Hi,
>>
>> I am sorry if this is not a right place to ask questions on SMT 
>> solver, but I am really struggling, and have nobody to ask. Please 
>> ignore if this bothers you, but any help will be highly appreciated!
>>
>> My problem: I am trying to use SMT to find value of "a" value so that 
>> "a * b == b" with all value of "b". The expected result is "a == 1". 
>> One minor issue is that in the input formula, besides "a", "b", I 
>> have some auxiliary variables (like tmp, tmp1, etc ..., which I must 
>> deal with). I use
>> Z3
>> solver, with python binding. I have two solutions below.
>>
>> *(A) I implemented this with ForAll quantifier in below code (correct 
>> me if there is a solution without using any quantifier). The idea is 
>> to prove "f"and "
>> g" are equivalent.*
>>
>> from z3 import *
>>
>> a, b, a1, tmp1 = BitVecs('a b a1 tmp1', 32)
>>
>> f = True
>> f = And(f, tmp1 == b)
>> f = And(f, a1 == a * tmp1)
>>
>> g= True
>> g = And(g, a1 == b)
>>
>> s = Solver()
>> s.add(ForAll([b, tmp1, a1], f == g))
>>
>> if s.check() == sat:
>>     print 'a =', s.model()[a]
>> else:
>>     print 'Unsat'
>>
>> However, this simple code runs forever without giving back result. I 
>> think that is because of the ForAll. Any idea on how to fix this 
>> code?
>>
>>
>> *(B) I tried again with another version. This time I dont prove two 
>> formulas to be equivalent, but put them all into one formula 
>> "f".*Logically, I think this is true, but please correct me if I am 
>> wrong here:
>>
>>
>> from z3 import *
>>
>> a, b, a1, tmp = BitVecs('a b a1 tmp', 32)
>>
>> f = True
>> f = And(f, tmp == b)
>> f = And(f, a1 == a * tmp)
>> f = And(f, a1 == b)
>>
>> s = Solver()
>> s.add(ForAll([b, a1], f))
>>
>> if s.check() == sat:
>>     print 'a =', s.model()[a]
>> else:
>>     print 'Unsat'
>>
>>
>> This time the code does not hang, but immediately returns 'Unsat'. 
>> Any idea
>> on how to fix this?
>>
>> Thanks so much!
>>
>> Jun
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
>>

_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib