search

swtv-kaist / cs458-fall22

1 stars 0 forks source link

HW7: about QF_BV #31

Open Akkanit opened 1 year ago

Akkanit commented 1 year ago

I wonder about comparison function such as (less than) or (more than or equal) Should I implement these function manully or just using bv2int as below? (>= (bv2int bigger_2) (bv2int a))

If bv2int can be used can I ask how this formula is satisfied? (< (bv2int (bvsub a b)) 1) when b -> #x00000000 a -> #x00000001

And also should I implement a and b value declaration as bitvectors?

And if I tried to implement by bvlt (bvlt (bvsub a b) (( int2bv 32) 1))) It got error: ERROR: line 11 column 99: could not find overload for 'bvlt' Argument: (bvsub a b) has type ( BitVec 32). Argument: (( int2bv 32) 1) has type ( BitVec 32). WARNING: could not parse file 'max_qf_bv4.smt'. ERROR: solving 'max_qf_bv4.smt'. What is the meaning of this error?

moonzoo commented 1 year ago

You can use bvslt, bvsle, and so on. You can find more detail on how to write BV specification from the lecture slide.

image

moonzoo commented 1 year ago

I found that the lecture slide on BV was outdated (i.e., now all BV predicate should explicitly indicate if its operands are signed or unsigned such as bvslt, bvult). I modified my previous comment and updated/uploaded the SMTlib lecture slides to the CS458 home page.