how to support the following operations: &, %, |

Reply

xyz031702 Posted: 09-24-2009 9:40 AM

rated by 0 users

Hi, all

     I am a beginner using Z3, which already helps me a lot.

    However I met problems when meeting operations : &(bitwise And) , %(mod) ,|(bitwise Or)

Example:

     I try to prove:

 (benchmark tst  :extrafuns ((a Real)) :formula (not (= (% a 2) 1)) :formula (> a 0))

or

 (benchmark tst  :extrafuns ((a Real)) :formula (not (= (& a 2) 1)) :formula (> a 0))

or

 (benchmark tst  :extrafuns ((a Real)) :formula (not (= (| a 2) 1)) :formula (> a 0))

The prover will throw exceptions saying "Error: could not find overload for '%' ".

Is there anyone knowing how to solve such problem?

Expecting for the replies and suggestions. Thanks a lot.

Ding Sun

Reply

Nikolaj Bjorner replied on 09-24-2009 10:02 AM

rated by 0 users

You need to declare constants as bit-vectors and use bit-vector operation names. The names you use are not used by Z3.

The SMT-LIB syntax is not unique to Z3. More information on SMT-LIB syntax is available from www.smtlib.org

(benchmark tst  :extrafuns ((a BitVec[32]))
:formula (not (= (bvurem a bv2[32]) bv1[32]))
:formula (not (= (bvand a bv2[32]) bv1[32]))
:formula (not (= (bvor a bv2[32]) bv1[32]))
)

Reply

xyz031702 replied on 09-28-2009 5:26 AM

rated by 0 users

many thanks , but how to know the vector size if the variable is from user input,

or is there any mapping rules between data types and vector size? , like the following:

int a <----> BitVec[32]

long b <----> BitVec[?]

thanks very much and best regards

ding sun