src/Interpreter/smtsig.cc

   1 #include "smtsig.h"
   2 #include "set.h"
   3
   4 SMTBoolSig::SMTBoolSig(uint id):
   5         ValuedSignature(id)
   6 {
   7 }
   8
   9 string SMTBoolSig::toString() const{
  10         return "b" + to_string(id);
  11 }
  12
  13 string SMTBoolSig::getSignature() const{
  14         return "(declare-const b" + to_string(id) + " Bool)";
  15 }
  16
  17 string SMTBoolSig::getAbsSignature() const{
  18         return "";
  19 }
  20
  21 SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig):
  22         ValuedSignature(id),
  23         ssig(_ssig)
  24 {
  25 }
  26
  27 string SMTElementSig::toString() const{
  28         return "e" + to_string(id);
  29 }
  30
  31 string SMTElementSig::getSignature() const{
  32         string str = "(declare-const e" + to_string(id) + " Int)\n";
  33         string constraint = ssig->getAbsSignature();
  34         size_t start_pos;
  35         string placeholder = "$";
  36         while((start_pos = constraint.find(placeholder)) != string::npos){
  37                 constraint.replace(start_pos, placeholder.size(), to_string(id));
  38         }
  39         //constraint.replace(constraint.begin(), constraint.end(), "$", );
  40         str += constraint;
  41         return str;
  42 }
  43
  44 string SMTElementSig::getAbsSignature() const{
  45         return "";
  46
  47 }
  48
  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);
  52         Vector<int> holes;
  53         int prev = set->getElement(0);
  54         for(uint i=1; i< set->getSize(); i++){
  55                 int curr = set->getElement(i);
  56                 if(prev != curr -1){
  57                         for(int j=prev+1; j< curr; j++){
  58                                 holes.push(j);
  59                         }
  60                 }
  61                 prev = curr;
  62         }
  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";
  67         }
  68 }
  69
  70 string SMTSetSig::toString() const{
  71         return "";
  72 }
  73
  74 string SMTSetSig::getSignature() const{
  75         return "";
  76 }
  77
  78 string SMTSetSig::getAbsSignature() const{
  79         return constraint;
  80
  81 }