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);
60 //Read data in from results file
66 string Interpreter::encodeConstraint(BooleanEdge c){
67 Boolean *constraint = c.getBoolean();
69 switch(constraint->type){
71 res = encodeBooleanLogic((BooleanLogic *) constraint);
75 res = encodePredicate((BooleanPredicate *) constraint);
79 res = encodeBooleanVar( (BooleanVar *) constraint);
86 return negateConstraint(res);
91 string Interpreter::encodePredicate( BooleanPredicate *bp){
92 switch (bp->predicate->type) {
96 return encodeOperatorPredicate(bp);
102 string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
103 PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
104 ASSERT(constraint->inputs.getSize() == 2);
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);
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);
118 str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
122 void Interpreter::writeToFile(string str){
123 output << str << endl;
126 bool Interpreter::getBooleanValue(Boolean *b){
127 return (bool)sigEnc.getValue(b);
130 uint64_t Interpreter::getValue(Element * element){
131 return (uint64_t)sigEnc.getValue(element);