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

[Matthieu Wipliez]

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

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.


Cheers
Matthieu




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