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

[cok at frontiernet.net]

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)

- David



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