4 SMTBoolSig::SMTBoolSig(uint id):
9 string SMTBoolSig::toString() const{
10 return "b" + to_string(id);
13 string SMTBoolSig::getSignature() const{
14 return "(declare-const b" + to_string(id) + " Bool)";
17 string SMTBoolSig::getAbsSignature() const{
21 SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig):
27 string SMTElementSig::toString() const{
28 return "e" + to_string(id);
31 string SMTElementSig::getSignature() const{
32 string str = "(declare-const e" + to_string(id) + " Int)\n";
33 string constraint = ssig->getAbsSignature();
35 string placeholder = "$";
36 while((start_pos = constraint.find(placeholder)) != string::npos){
37 constraint.replace(start_pos, placeholder.size(), to_string(id));
39 //constraint.replace(constraint.begin(), constraint.end(), "$", );
44 string SMTElementSig::getAbsSignature() const{
49 SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
50 ASSERT(set->getSize() > 0);
51 int min = set->getElement(0), max = set->getElement(set->getSize()-1);
53 int prev = set->getElement(0);
54 for(uint i=1; i< set->getSize(); i++){
55 int curr = set->getElement(i);
57 for(int j=prev+1; j< curr; j++){
63 constraint = "(assert (<= e$ " + to_string(max) +"))\n";
64 constraint += "(assert (>= e$ " + to_string(min) +"))\n";
65 for(uint i=0; i< holes.getSize(); i++){
66 constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
70 string SMTSetSig::toString() const{
74 string SMTSetSig::getSignature() const{
78 string SMTSetSig::getAbsSignature() const{