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) {
  60                 //Read data in from results file
  61                 result = getResult();
  62         }
  63         return result;
  64 }
  65
  66 string Interpreter::encodeConstraint(BooleanEdge c){
  67         Boolean *constraint = c.getBoolean();
  68         string res;
  69         switch(constraint->type){
  70                 case LOGICOP:{
  71                         res = encodeBooleanLogic((BooleanLogic *) constraint);
  72                         break;
  73                 }
  74                 case PREDICATEOP:{
  75                         res = encodePredicate((BooleanPredicate *) constraint);
  76                         break;
  77                 }
  78                 case BOOLEANVAR:{
  79                         res = encodeBooleanVar( (BooleanVar *) constraint);
  80                         break;
  81                 }
  82                 default:
  83                         ASSERT(0);
  84         }
  85         if(c.isNegated()){
  86                 return negateConstraint(res);
  87         }
  88         return res;
  89 }
  90
  91 string Interpreter::encodePredicate( BooleanPredicate *bp){
  92         switch (bp->predicate->type) {
  93                 case TABLEPRED:
  94                         ASSERT(0);
  95                 case OPERATORPRED:
  96                         return encodeOperatorPredicate(bp);
  97                 default:
  98                         ASSERT(0);
  99         }
 100 }
 101
 102 string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
 103         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 104         ASSERT(constraint->inputs.getSize() == 2);
 105         string str;
 106         Element *elem0 = constraint->inputs.get(0);
 107         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 108         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
 109         if(elem0->type == ELEMFUNCRETURN){
 110                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
 111         }
 112         Element *elem1 = constraint->inputs.get(1);
 113         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 114         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
 115         if(elem1->type == ELEMFUNCRETURN){
 116                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
 117         }
 118         str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
 119         return str;
 120 }
 121
 122 void Interpreter::writeToFile(string str){
 123         output << str << endl;
 124 }
 125
 126 bool Interpreter::getBooleanValue(Boolean *b){
 127         return (bool)sigEnc.getValue(b);
 128 }
 129
 130 uint64_t Interpreter::getValue(Element * element){
 131         return (uint64_t)sigEnc.getValue(element);
 132 }
 133