Boolector #4
Now let’s work on the example from documentation, because they are not that bad😜.
Example is to implement : 0<x<=100 && 0<y<=100 && x*y<100
Looks simple? Because it is. Let’s dive in.
#include <iostream>
#include “boolector.h”
using namespace std;int main(int, char**) {
Btor *btor=boolector_new();boolector_set_opt(btor,BTOR_OPT_MODEL_GEN,1);BoolectorSort bsort8=boolector_bitvec_sort(btor,8);//0<x<=100 && 0<y<=100 && x*y<100BoolectorNode *x=boolector_var(btor,bsort8,”x”);
BoolectorNode *y=boolector_var(btor,bsort8,”y”);BoolectorNode *_100=boolector_int(btor,100,bsort8);
BoolectorNode *_0=boolector_zero(btor,bsort8);BoolectorNode *u1=boolector_ugt(btor,x,_0);
boolector_assert(btor,u1);BoolectorNode *u2=boolector_ulte(btor,x,_100);
boolector_assert(btor,u2);BoolectorNode *u3=boolector_ugt(btor,y,_0);
boolector_assert(btor,u3);BoolectorNode *u4=boolector_ulte(btor,y,_100);
boolector_assert(btor,u4);BoolectorNode *z=boolector_mul(btor,x,y);
BoolectorNode *u5=boolector_ulte(btor,z,_100);
boolector_assert(btor,u5);BoolectorNode *u6=boolector_umulo(btor,x,y);
BoolectorNode *u7=boolector_not(btor,u6);
boolector_assert(btor,u7);
int result=boolector_sat(btor);
if(result==BOOLECTOR_SAT)
cout<<”SAT”<<endl;
else if(result==BOOLECTOR_UNSAT)
cout<<”UNSAT”<<endl;
else
cout<<”OTHER”<<endl;const char *x1=boolector_bv_assignment(btor,x);
const char *y1=boolector_bv_assignment(btor,y);
const char *z1=boolector_bv_assignment(btor,z);
cout<<”x: “<<x1<<” y: “<<y1<<” z: “<<z1<<endl;cout<<”Stdout model in btor format”<<endl;
boolector_print_model(btor,”btor”,stdout);cout<<”Stdout model in smt-lib2 format”<<endl;
boolector_print_model(btor,”smt2",stdout);boolector_release_all(btor);
boolector_free_bv_assignment(btor,x1);
boolector_free_bv_assignment(btor,y1);
boolector_free_bv_assignment(btor,z1);boolector_delete(btor);
}
> First we get a device of Btor company from shop with function boolector_new(). [A instance of Boolector].
> We have to ON the device with BTOR_OPT_MODEL_GEN with value 1 to enable it.
> Now we create a bit-vector data type of bit width 8.
> Now we create variable (BoolectorNode) x and y of data type bsort8 in device btor.
> To implement above constraints, we’ll need constants 100 and zero.
for 100 and 0 variable _100 and _0 are created with functions boolector_int and boolector_zero respectively.
> BoolectorNode *u1 implements x>0
boolector_assert will ensure the constraint has been applied. Asserted node cannot be deleted.
> BoolectorNode *u2 implements x≤100
> Similarly for y : y>0 and y≤100 [u3 and u4]
> at BoolectorNode *z we multiply x and y and u5 ensures z≤100
> u6 and u7 to ensure multiplication is not overflowed nore than 8 bits (bsort8).
> boolector_sat will solve the input formula. Formulas are the ones we added with boolector_assert. It will check and tells if the constraints added are even possible (BOOLECTOR_SAT) or not (BOOLECTOR_UNSAT).
> only after boolector_sat, one can print any BoolectorNode.
> boolector_bv_assignment converts BoolectorNode data into char array than we can stdout.
> We printed x,y,z, and it shows one of the possible values for x,y,z satisfiable with constraints.
> boolector_print_model is to print the asked model, e.g. btor, smt2. There are basically two forms of display for all the input vars, only input.
> boolector_release_all can release all the BoolectorNodes associated with device at once.
> rest are free statements for all assignments.
> at last delete the device from system.
For next part click here.
