src/Interpreter/interpreter.cc

   1 #include "interpreter.h"
   2 #include <string>
   3 #include "signatureenc.h"
   4 #include "structs.h"
   5 #include "csolver.h"
   6 #include "boolean.h"
   7 #include "predicate.h"
   8 #include "element.h"
   9 #include "signature.h"
  10 #include "set.h"
  11 #include "function.h"
  12 #include "inc_solver.h"
  13 #include <fstream>
  14
  15 using namespace std;
  16
  17 Interpreter::Interpreter(CSolver *_solver) :
  18         csolver(_solver),
  19         sigEnc(this)
  20 {
  21 }
  22
  23 Interpreter::~Interpreter() {
  24 }
  25
  26 void Interpreter::encode() {
  27         dumpHeader();
  28         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
  29         Vector<char *> facts;
  30         while (iterator->hasNext()) {
  31                 BooleanEdge constraint = iterator->next();
  32                 string constr = encodeConstraint(constraint);
  33                 char *cstr = new char [constr.length() + 1];
  34                 strcpy (cstr, constr.c_str());
  35                 facts.push(cstr);
  36         }
  37         dumpAllConstraints(facts);
  38         for (uint i = 0; i < facts.getSize(); i++) {
  39                 char *cstr = facts.get(i);
  40                 delete[] cstr;
  41         }
  42         delete iterator;
  43 }
  44
  45 uint Interpreter::getTimeout() {
  46         uint timeout = csolver->getSatSolverTimeout();
  47         return timeout == (uint)NOTIMEOUT ? 1000 : timeout;
  48 }
  49
  50 int Interpreter::solve() {
  51         dumpFooter();
  52         int result = IS_INDETER;
  53         char buffer [512];
  54         if ( output.is_open()) {
  55                 output.close();
  56         }
  57         compileRunCommand(buffer, sizeof(buffer));
  58         int status = system(buffer);
  59         if (status == 0 || status == 512 ) {//For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
  60                 //Read data in from results file
  61                 result = getResult();
  62         } else {
  63                 model_print("Error in running command<returned %d>: %s\n", status, buffer);
  64                 exit(-1);
  65         }
  66         return result;
  67 }
  68
  69 string Interpreter::encodeConstraint(BooleanEdge c) {
  70         Boolean *constraint = c.getBoolean();
  71         string res;
  72         switch (constraint->type) {
  73         case LOGICOP: {
  74                 res = encodeBooleanLogic((BooleanLogic *) constraint);
  75                 break;
  76         }
  77         case PREDICATEOP: {
  78                 res = encodePredicate((BooleanPredicate *) constraint);
  79                 break;
  80         }
  81         case BOOLEANVAR: {
  82                 res = encodeBooleanVar( (BooleanVar *) constraint);
  83                 break;
  84         }
  85         default:
  86                 ASSERT(0);
  87         }
  88         if (c.isNegated()) {
  89                 return negateConstraint(res);
  90         }
  91         return res;
  92 }
  93
  94 string Interpreter::encodePredicate( BooleanPredicate *bp) {
  95         switch (bp->predicate->type) {
  96         case TABLEPRED:
  97                 ASSERT(0);
  98         case OPERATORPRED:
  99                 return encodeOperatorPredicate(bp);
 100         default:
 101                 ASSERT(0);
 102         }
 103 }
 104
 105 string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint) {
 106         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 107         ASSERT(constraint->inputs.getSize() == 2);
 108         string str;
 109         Element *elem0 = constraint->inputs.get(0);
 110         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 111         ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0);
 112         if (elem0->type == ELEMFUNCRETURN) {
 113                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
 114         }
 115         Element *elem1 = constraint->inputs.get(1);
 116         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 117         ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1);
 118         if (elem1->type == ELEMFUNCRETURN) {
 119                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
 120         }
 121         str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
 122         return str;
 123 }
 124
 125 void Interpreter::writeToFile(string str) {
 126         if (!str.empty()) {
 127                 output << str << endl;
 128         }
 129 }
 130
 131 bool Interpreter::getBooleanValue(Boolean *b) {
 132         return (bool)sigEnc.getValue(b);
 133 }
 134
 135 uint64_t Interpreter::getValue(Element *element) {
 136         return (uint64_t)sigEnc.getValue(element);
 137 }
 138