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

[Morgan Deters]

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


-- 
Morgan Deters
Postdoctoral Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/