Boolector #3

What if we want to create vars with constant value. What? vars and constant? You must be joking, right?

Well let’s just say, it’s there.

Now to actually manipulate the device, we have to ON the device. Same kind of function is done by BTOR_OPT_MODEL_GEN.

Here x,y,z are three vars of bsort8 (bit vector 8) data type in device btor.

But _5, _10 are two vars of bsort8 data type having value 5 and 10 respectively.

x=boolector_eq(btor,x,_5);
y=boolector_eq(btor,y,_10);

These two statements are putting constraints over x and y saying x=_5,y=_10 in device btor.

z=boolector_and(btor,x,y);

boolector_and takes parameters as device name (btor), two vars of same bit width x and y and returns result as and of x and y of same bit width as params.

boolector_sat(btor)

This function checks the device btor, if it can satisfy the constraints. If yes it returns BOOLECTOR_SAT if the instance is satisfiable and BOOLECTOR_UNSAT if the instance is unsatisfiable.

Now z is a pointer to a node BoolectorNode. So boolector provides us an option to parse the result into a char array using boolector_bv_assignment.

The result is parsed into resz and we can stdout it.

Geeky!! If you create a picture of a actual hardware device btor in your hand, you will remember to release and free the vars and function and at last delete the device.

For next part click here.