[SMT-LIB] Re : Combine Boolean & BitVector?

[Jun Koi]

On Wed, Aug 24, 2011 at 6:32 PM, Matthieu Wipliez <mwipliez at yahoo.fr> wrote:
> Hi,
> I'd say like this, with the "if-then-else" function:
>
> (assert (= a (ite (= b #x0) #x1 #x0)))
> That's the closest to what you want to do I can think of :-)

this is exactly what i am looking for, thanks!!!

> In your example, it does not work because the type (called sort with SMT) of
> "=" is boolean, not bit vector.
> By the way, this answers your question in the other mail: the only way to
> assign a value to a is to create an assertion that the "= a value" (which is
> an expression) is true.
> But still, like I said this is not equivalent to an assignment in an
> imperative language: you cannot "assign" a the value 4, and then the value
> 5.
> You can assert that a equals 4 or that a equals 5, but not both.
> If you want to translate code to SMT, you should probably use SSA (Static
> Single Assignment) to differentiate variables.

thanks for your recommendation!


J




> ________________________________
> De : Jun Koi <junkoi2004 at gmail.com>
> À : smt-lib at cs.nyu.edu
> Envoyé le : Mercredi 24 Août 2011 11h28
> Objet : [SMT-LIB] Combine Boolean & BitVector?
>
> hi,
>
> i want to do a simple logic on a variable, like this:
>
> a = (b == 0? 1 : 0)
>
> that is, a will be 1 if b is 0, or 0 if b is not 0.
>
> i implemented the logic in below code. but Z3 complains "operator is
> applied to arguments of the wrong sort" on line 4.
> i guess this means it is not allowed to AND a Boolean value and a
> Bitvector value.
>
> but then how can i implement my idea?
>
> thanks a lot,
> Jun
>
> -------
> (set-logic QF_BV)
> (declare-fun a () (_ BitVec 4))
> (declare-fun b () (_ BitVec 4))
> (assert (= a (bvand (= b #x0) #x1)))
> (check-sat)
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>
>