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

[Jun Koi]

On Wed, Aug 24, 2011 at 7:48 PM,  <cok at frontiernet.net> wrote:
> One other way of writing that a is 4 would be
>
> (define-fun a () (_ BitVec 4) #x4)
>
> Now a is treated as an abbreviation for #x4 (depending on the solver)

got it, thanks David!

best,
J


> ----- "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 :-)
>>
>> 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
>> >
>> >
>> >
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>