[SMT-LIB] Some problem with ForAll quantifier in my SMT formula
Jun Koi
junkoi2004 at gmail.com
Fri Jun 21 00:09:02 EDT 2013
hi,
i am extremely grateful, thanks so much for your kind helps!
from your emails, i realize i had the wrong approach.
i should state my problem more clear. here is my original problem: given
some formulas like below: (a, b, c, d are all Bitvec of 32 bits)
c == b
d == a * c
what i need to to is: find the value of "a", so that from above two
formulas, i have "d == b"
now i realize that i should use "Imply" together with "Exists", rather than
"Equivalent".
so i encode this again in Z3, like below:
=====
from z3 import *
a, b, c, d = BitVecs('a b c d', 32)
f = True
f = And(f, c == b)
f = And(f, d == a * c)
s = Solver()
s.add(Exists(a, Implies(f, d == b)))
if s.check() == sat:
print 'model =', s.model()
print 'a =', s.model()[a]
else:
print 'Unsat'
====
but when i run this, the output is:
model = [c = 0, d = 1, a!0 = 0]
a = None
so it seems somehow i still encoded the formula wrong, since what i expect
is having "a = 1", but i got "a = None" instead.
any idea?
thanks so much!
On Fri, Jun 21, 2013 at 7:20 AM, Nikolaj Bjorner <nbjorner at microsoft.com>wrote:
> 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
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
More information about the SMT-LIB
mailing list