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