[SMT-LIB] Re : BVDIV on Bitvector (SMTLIB2) ?

[Matthieu Wipliez]

Hi Jun,

the second line means "make sure that a equals 4".
I don't know if that should be considered an assignment, because you don't give a the value 4 explicitly, rather you add a constraint that it should be equal to 4 (so it's more than a comparison) :-)
Obviously, later you can add an assertion that contradicts this one (say, "(assert (= a #x5))"), which will make your script unsatisfiable (a cannot equal 4 and 5 simultaneously).


Cheers
Matthieu



>________________________________
>De : Jun Koi <junkoi2004 at gmail.com>
>À : Christopher L Conway <cconway at cs.nyu.edu>
>Cc : smt-lib at cs.nyu.edu
>Envoyé le : Mercredi 24 Août 2011 9h43
>Objet : Re: [SMT-LIB] BVDIV on Bitvector (SMTLIB2) ?
>
>On Wed, Aug 24, 2011 at 11:28 AM, Christopher L Conway
><cconway at cs.nyu.edu> wrote:
>> On Tue, Aug 23, 2011 at 10:49 PM, Jun Koi <junkoi2004 at gmail.com> wrote:
>>> another question: i found bvule, bvugt, etc. but i cannot find
>>> anything to compare 2 vectors, so i can know if 2 vectors are equal.
>>> or did i miss something?
>>
>>
>> Yeah, you missed =.
>>
>> ;-)
>>
>> The equality operator is overloaded to work on any type.
>
>hmm, this is confused for me. i always think that "=" is for
>assignment, but it is used for comparison, too?
>
>so the 2nd line below should be understood as assignment, or comparison??
>
>(declare-fun a () (_ BitVec 4))
>(assert (= a #x4))
>
>
>thanks,
>Jun
>_______________________________________________
>SMT-LIB mailing list
>SMT-LIB at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>
>