1 #include "interpreter.h"
3 #include "signatureenc.h"
12 #include "inc_solver.h"
17 Interpreter::Interpreter(CSolver *_solver):
23 Interpreter::~Interpreter(){
26 void Interpreter::encode(){
28 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
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());
37 dumpAllConstraints(facts);
38 for(uint i=0; i< facts.getSize(); i++){
39 char *cstr = facts.get(i);
45 uint Interpreter::getTimeout(){
46 uint timeout =csolver->getSatSolverTimeout();
47 return timeout == (uint)NOTIMEOUT? 1000: timeout;
50 int Interpreter::solve(){
52 int result = IS_INDETER;
54 if( output.is_open()){
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
63 model_print("Error in running command<returned %d>: %s\n", status, buffer);
69 string Interpreter::encodeConstraint(BooleanEdge c){
70 Boolean *constraint = c.getBoolean();
72 switch(constraint->type){
74 res = encodeBooleanLogic((BooleanLogic *) constraint);
78 res = encodePredicate((BooleanPredicate *) constraint);
82 res = encodeBooleanVar( (BooleanVar *) constraint);
89 return negateConstraint(res);
94 string Interpreter::encodePredicate( BooleanPredicate *bp){
95 switch (bp->predicate->type) {
99 return encodeOperatorPredicate(bp);
105 string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
106 PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
107 ASSERT(constraint->inputs.getSize() == 2);
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);
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);
121 str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
125 void Interpreter::writeToFile(string str){
127 output << str << endl;
131 bool Interpreter::getBooleanValue(Boolean *b){
132 return (bool)sigEnc.getValue(b);
135 uint64_t Interpreter::getValue(Element * element){
136 return (uint64_t)sigEnc.getValue(element);