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

[Adrien Champion]

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
>>
>>