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 }