From: Hamed Gorjiara Date: Thu, 21 Feb 2019 20:19:46 +0000 (-0800) Subject: Adding SMT Interpreters X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=4c58af641a877bb6d65769994c8fd57ecedbd22c;ds=sidebyside Adding SMT Interpreters --- diff --git a/src/AST/ops.h b/src/AST/ops.h index 8b08202..6d6fd97 100644 --- a/src/AST/ops.h +++ b/src/AST/ops.h @@ -26,4 +26,8 @@ typedef enum OverFlowBehavior OverFlowBehavior; enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, SATC_FLAGFORCEUNDEFINED, SATC_UNDEFINEDSETSFLAG, SATC_FLAGIFFUNDEFINED}; typedef enum UndefinedBehavior UndefinedBehavior; +enum InterpreterType {SATUNE, ALLOY, Z3, MATHSAT, SMTRAT}; +typedef enum InterpreterType InterpreterType; + + #endif diff --git a/src/Interpreter/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc index f910ac6..c0e4a60 100644 --- a/src/Interpreter/alloyinterpreter.cc +++ b/src/Interpreter/alloyinterpreter.cc @@ -6,12 +6,13 @@ #include "boolean.h" #include "predicate.h" #include "element.h" -#include "signature.h" +#include "alloysig.h" #include "set.h" #include "function.h" #include "inc_solver.h" #include #include "cppvector.h" +#include "math.h" using namespace std; @@ -34,6 +35,18 @@ AlloyInterpreter::~AlloyInterpreter(){ } } +ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){ + return new AlloyBoolSig(id); +} + +ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){ + return new AlloyElementSig(id, ssig); +} + +Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){ + return new AlloySetSig(id, set); +} + void AlloyInterpreter::dumpAllConstraints(Vector &facts){ output << "fact {" << endl; for(uint i=0; i< facts.getSize(); i++){ @@ -60,7 +73,6 @@ int AlloyInterpreter::getResult(){ strcpy ( cline, line.c_str() ); char *token = strtok(cline, delim); while( token != NULL ) { - printf( " %s\n", token ); uint i1, i2, i3; if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){ model_print("Signature%u = %u\n", i1, i3); @@ -73,9 +85,15 @@ int AlloyInterpreter::getResult(){ return IS_SAT; } + +int AlloyInterpreter::getAlloyIntScope(){ + double mylog = log2(sigEnc.getMaxValue() + 1); + return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2; +} + void AlloyInterpreter::dumpFooter(){ output << "pred show {}" << endl; - output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl; + output << "run show for " << getAlloyIntScope() << " int" << endl; } void AlloyInterpreter::dumpHeader(){ @@ -142,15 +160,15 @@ string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){ } string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){ - BooleanSig * boolSig = sigEnc.getBooleanSignature(bv); + ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv); return *boolSig + " = 1"; } -string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){ +string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){ FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction(); uint numDomains = elemFunc->inputs.getSize(); ASSERT(numDomains > 1); - ElementSig *inputs[numDomains]; + ValuedSignature *inputs[numDomains]; string result; for (uint i = 0; i < numDomains; i++) { Element *elem = elemFunc->inputs.get(i); @@ -178,7 +196,7 @@ string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, Eleme return result; } -string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){ +string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){ switch (op) { case SATC_EQUALS: return *elemSig1 + " = " + *elemSig2; diff --git a/src/Interpreter/alloyinterpreter.h b/src/Interpreter/alloyinterpreter.h index ec2e4a3..e4a1e3b 100644 --- a/src/Interpreter/alloyinterpreter.h +++ b/src/Interpreter/alloyinterpreter.h @@ -1,5 +1,5 @@ -#ifndef ALLOYENC_H -#define ALLOYENC_H +#ifndef ALLOYINTERPRETER_H +#define ALLOYINTERPRETER_H #include "classlist.h" #include "signatureenc.h" @@ -10,10 +10,14 @@ class AlloyInterpreter: public Interpreter{ public: AlloyInterpreter(CSolver *solver); + virtual ValuedSignature *getBooleanSignature(uint id); + virtual ValuedSignature *getElementSignature(uint id, Signature *ssig); + virtual Signature *getSetSignature(uint id, Set *set); virtual ~AlloyInterpreter(); protected: virtual void dumpFooter(); virtual void dumpHeader(); + int getAlloyIntScope(); virtual void compileRunCommand(char * command , size_t size); virtual int getResult(); virtual void dumpAllConstraints(Vector &facts); @@ -21,8 +25,8 @@ protected: virtual string encodeBooleanLogic( BooleanLogic *bl); virtual string encodeBooleanVar( BooleanVar *bv); string encodeOperatorPredicate(BooleanPredicate *constraint); - virtual string processElementFunction(ElementFunction *element, ElementSig *signature); - virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2); + virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature); + virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2); }; #endif diff --git a/src/Interpreter/alloysig.cc b/src/Interpreter/alloysig.cc new file mode 100644 index 0000000..1b98cd8 --- /dev/null +++ b/src/Interpreter/alloysig.cc @@ -0,0 +1,104 @@ +#include "alloysig.h" +#include "set.h" + +bool AlloyBoolSig::encodeAbs = true; +bool AlloySetSig::encodeAbs = true; +bool AlloyElementSig::encodeAbs = true; + +AlloyBoolSig::AlloyBoolSig(uint id): + ValuedSignature(id) +{ +} + +string AlloyBoolSig::toString() const{ + return "Boolean" + to_string(id) + ".value"; +} + +string AlloyBoolSig::getSignature() const{ + string str; + if(encodeAbs){ + encodeAbs = false; + str += getAbsSignature(); + } + str += "one sig Boolean" + to_string(id) + " extends AbsBool {}"; + return str; +} + +string AlloyBoolSig::getAbsSignature() const{ + string str; + if(AlloySetSig::encodeAbs){ + AlloySetSig::encodeAbs = false; + str += "abstract sig AbsSet {\ + domain: set Int\ + }\n"; + } + str +="one sig BooleanSet extends AbsSet {}{\n\ + domain = 0 + 1 \n\ + }\n\ + abstract sig AbsBool {\ + value: Int\ + }{\n\ + value in BooleanSet.domain\n\ + }\n"; + return str; +} + +AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig): + ValuedSignature(id), + ssig(_ssig) +{ +} + +string AlloyElementSig::toString() const{ + return "Element" + to_string(id) + ".value"; +} + +string AlloyElementSig::getSignature() const{ + string str; + if(encodeAbs){ + encodeAbs = false; + str += getAbsSignature(); + } + str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\ + value in " + *ssig + "\n\ + }"; + return str; +} + +string AlloyElementSig::getAbsSignature() const{ + return "abstract sig AbsElement {\n\ + value: Int\n\ + }\n"; + +} + +AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){ + ASSERT(set->getSize() > 0); + domain = to_string(set->getElement(0)); + for(uint i=1; i< set->getSize(); i++){ + domain += " + " + to_string(set->getElement(i)); + } +} + +string AlloySetSig::toString() const{ + return "Set" + to_string(id) + ".domain"; +} + +string AlloySetSig::getSignature() const{ + string str; + if(encodeAbs){ + encodeAbs = false; + str += getAbsSignature(); + } + str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\ + domain = " + domain + "\n\ + }"; + return str; +} + +string AlloySetSig::getAbsSignature() const{ + return "abstract sig AbsSet {\n\ + domain: set Int\n\ + }\n"; + +} diff --git a/src/Interpreter/alloysig.h b/src/Interpreter/alloysig.h new file mode 100644 index 0000000..3fb2d10 --- /dev/null +++ b/src/Interpreter/alloysig.h @@ -0,0 +1,44 @@ +#ifndef ALLOYSIG_H +#define ALLOYSIG_H +#include +#include +#include "signature.h" +#include "classlist.h" +using namespace std; + +class AlloyBoolSig: public ValuedSignature{ +public: + AlloyBoolSig(uint id); + virtual ~AlloyBoolSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +private: + static bool encodeAbs; +}; + +class AlloySetSig: public Signature{ +public: + AlloySetSig(uint id, Set *set); + virtual ~AlloySetSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; + static bool encodeAbs; +private: + string domain; +}; + +class AlloyElementSig: public ValuedSignature{ +public: + AlloyElementSig(uint id, Signature *ssig); + virtual ~AlloyElementSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +private: + Signature *ssig; + static bool encodeAbs; +}; + +#endif diff --git a/src/Interpreter/interpreter.cc b/src/Interpreter/interpreter.cc index bab92b4..d87cbd9 100644 --- a/src/Interpreter/interpreter.cc +++ b/src/Interpreter/interpreter.cc @@ -105,13 +105,13 @@ string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){ string str; Element *elem0 = constraint->inputs.get(0); ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST); - ElementSig *elemSig1 = sigEnc.getElementSignature(elem0); + ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0); if(elem0->type == ELEMFUNCRETURN){ str += processElementFunction((ElementFunction *) elem0, elemSig1); } Element *elem1 = constraint->inputs.get(1); ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST); - ElementSig *elemSig2 = sigEnc.getElementSignature(elem1); + ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1); if(elem1->type == ELEMFUNCRETURN){ str += processElementFunction((ElementFunction *) elem1, elemSig2); } @@ -120,7 +120,9 @@ string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){ } void Interpreter::writeToFile(string str){ - output << str << endl; + if(!str.empty()){ + output << str << endl; + } } bool Interpreter::getBooleanValue(Boolean *b){ diff --git a/src/Interpreter/interpreter.h b/src/Interpreter/interpreter.h index 814511b..32eed4a 100644 --- a/src/Interpreter/interpreter.h +++ b/src/Interpreter/interpreter.h @@ -3,6 +3,7 @@ #include "classlist.h" #include "signatureenc.h" +#include "signature.h" #include #include using namespace std; @@ -15,6 +16,9 @@ public: void writeToFile(string str); uint64_t getValue(Element *element); bool getBooleanValue(Boolean *element); + virtual ValuedSignature *getBooleanSignature(uint id) = 0; + virtual ValuedSignature *getElementSignature(uint id, Signature *ssig) = 0; + virtual Signature *getSetSignature(uint id, Set *set) = 0; virtual ~Interpreter(); protected: virtual void dumpFooter() = 0; @@ -29,8 +33,8 @@ protected: virtual string encodeBooleanVar( BooleanVar *bv) = 0; string encodePredicate( BooleanPredicate *bp); string encodeOperatorPredicate(BooleanPredicate *constraint); - virtual string processElementFunction(ElementFunction *element, ElementSig *signature) = 0; - virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2) = 0; + virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature) = 0; + virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) = 0; CSolver *csolver; SignatureEnc sigEnc; ofstream output; diff --git a/src/Interpreter/signature.cc b/src/Interpreter/signature.cc index ad7d2e7..94efbb2 100644 --- a/src/Interpreter/signature.cc +++ b/src/Interpreter/signature.cc @@ -1,10 +1,6 @@ #include "signature.h" #include "set.h" -bool BooleanSig::encodeAbs = true; -bool SetSig::encodeAbs = true; -bool ElementSig::encodeAbs = true; - ValuedSignature::ValuedSignature(uint id): Signature(id), value(-1) @@ -16,104 +12,6 @@ int ValuedSignature::getValue(){ return value; } -BooleanSig::BooleanSig(uint id): - ValuedSignature(id) -{ -} - -string BooleanSig::toString() const{ - return "Boolean" + to_string(id) + ".value"; -} - -string BooleanSig::getSignature() const{ - string str; - if(encodeAbs){ - encodeAbs = false; - str += getAbsSignature(); - } - str += "one sig Boolean" + to_string(id) + " extends AbsBool {}"; - return str; -} - -string BooleanSig::getAbsSignature() const{ - string str; - if(SetSig::encodeAbs){ - SetSig::encodeAbs = false; - str += "abstract sig AbsSet {\ - domain: set Int\ - }\n"; - } - str +="one sig BooleanSet extends AbsSet {}{\n\ - domain = 0 + 1 \n\ - }\n\ - abstract sig AbsBool {\ - value: Int\ - }{\n\ - value in BooleanSet.domain\n\ - }\n"; - return str; -} - -ElementSig::ElementSig(uint id, SetSig *_ssig): - ValuedSignature(id), - ssig(_ssig) -{ -} - -string ElementSig::toString() const{ - return "Element" + to_string(id) + ".value"; -} - -string ElementSig::getSignature() const{ - string str; - if(encodeAbs){ - encodeAbs = false; - str += getAbsSignature(); - } - str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\ - value in " + *ssig + "\n\ - }"; - return str; -} - -string ElementSig::getAbsSignature() const{ - return "abstract sig AbsElement {\n\ - value: Int\n\ - }\n"; - -} - -SetSig::SetSig(uint id, Set *set): Signature(id){ - ASSERT(set->getSize() > 0); - domain = to_string(set->getElement(0)); - for(uint i=1; i< set->getSize(); i++){ - domain += " + " + to_string(set->getElement(i)); - } -} - -string SetSig::toString() const{ - return "Set" + to_string(id) + ".domain"; -} - -string SetSig::getSignature() const{ - string str; - if(encodeAbs){ - encodeAbs = false; - str += getAbsSignature(); - } - str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\ - domain = " + domain + "\n\ - }"; - return str; -} - -string SetSig::getAbsSignature() const{ - return "abstract sig AbsSet {\n\ - domain: set Int\n\ - }\n"; - -} - string Signature::operator+(const string& str){ return toString() + str; } diff --git a/src/Interpreter/signature.h b/src/Interpreter/signature.h index 1b321a6..e8c9e1c 100644 --- a/src/Interpreter/signature.h +++ b/src/Interpreter/signature.h @@ -1,5 +1,5 @@ -#ifndef ELEMENTSIG_H -#define ELEMENTSIG_H +#ifndef SIGNATURE_H +#define SIGNATURE_H #include #include #include "classlist.h" @@ -26,41 +26,6 @@ protected: int value; }; -class BooleanSig: public ValuedSignature{ -public: - BooleanSig(uint id); - virtual ~BooleanSig(){} - virtual string toString() const; - virtual string getAbsSignature() const; - virtual string getSignature() const; -private: - static bool encodeAbs; -}; - -class SetSig: public Signature{ -public: - SetSig(uint id, Set *set); - virtual ~SetSig(){} - virtual string toString() const; - virtual string getAbsSignature() const; - virtual string getSignature() const; - static bool encodeAbs; -private: - string domain; -}; - -class ElementSig: public ValuedSignature{ -public: - ElementSig(uint id, SetSig *ssig); - virtual ~ElementSig(){} - virtual string toString() const; - virtual string getAbsSignature() const; - virtual string getSignature() const; -private: - SetSig *ssig; - static bool encodeAbs; -}; - string operator+(const string& str, const Signature& sig); #endif diff --git a/src/Interpreter/signatureenc.cc b/src/Interpreter/signatureenc.cc index 5e0a900..cdc8aa1 100644 --- a/src/Interpreter/signatureenc.cc +++ b/src/Interpreter/signatureenc.cc @@ -2,8 +2,7 @@ #include "element.h" #include "set.h" #include "signature.h" -#include "alloyinterpreter.h" -#include "math.h" +#include "interpreter.h" SignatureEnc::SignatureEnc(Interpreter *inter): interpreter(inter), @@ -18,11 +17,6 @@ SignatureEnc::~SignatureEnc(){ } } -int SignatureEnc::getAlloyIntScope(){ - double mylog = log2(maxValue + 1); - return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2; -} - void SignatureEnc::updateMaxValue(Set *set){ for(uint i=0; i< set->getSize(); i++){ if(set->getElement(i) > maxValue){ @@ -31,10 +25,10 @@ void SignatureEnc::updateMaxValue(Set *set){ } } -BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){ - BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar); +ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){ + ValuedSignature *bsig = (ValuedSignature *)encoded.get((void *)bvar); if(bsig == NULL){ - bsig = new BooleanSig(getUniqueSigID()); + bsig = interpreter->getBooleanSignature(getUniqueSigID()); encoded.put(bvar, bsig); signatures.push(bsig); interpreter->writeToFile(bsig->getSignature()); @@ -42,19 +36,19 @@ BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){ return bsig; } -ElementSig *SignatureEnc::getElementSignature(Element *element){ - ElementSig *esig = (ElementSig *)encoded.get((void *)element); +ValuedSignature *SignatureEnc::getElementSignature(Element *element){ + ValuedSignature *esig = (ValuedSignature *)encoded.get((void *)element); if(esig == NULL){ Set *set = element->getRange(); - SetSig *ssig = (SetSig *)encoded.get((void *)set); + Signature *ssig = (Signature *)encoded.get((void *)set); if(ssig == NULL){ - ssig = new SetSig(getUniqueSigID(), set); + ssig = interpreter->getSetSignature(getUniqueSigID(), set); encoded.put(set, ssig); signatures.push(ssig); interpreter->writeToFile(ssig->getSignature()); updateMaxValue(set); } - esig = new ElementSig(getUniqueSigID(), ssig); + esig = interpreter->getElementSignature(getUniqueSigID(), ssig); encoded.put(element, esig); signatures.push(esig); interpreter->writeToFile(esig->getSignature()); diff --git a/src/Interpreter/signatureenc.h b/src/Interpreter/signatureenc.h index b195d03..988ac71 100644 --- a/src/Interpreter/signatureenc.h +++ b/src/Interpreter/signatureenc.h @@ -7,13 +7,13 @@ class SignatureEnc { public: - SignatureEnc(Interpreter *_alloyEncoder); + SignatureEnc(Interpreter *_interpreter); ~SignatureEnc(); void setValue(uint id, uint value); - ElementSig *getElementSignature(Element *element); - BooleanSig *getBooleanSignature(Boolean *bvar); - int getAlloyIntScope(); + ValuedSignature *getElementSignature(Element *element); + ValuedSignature *getBooleanSignature(Boolean *bvar); int getValue(void *astnode); + uint64_t getMaxValue(){ return maxValue;} private: ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);} uint getUniqueSigID(){return signatures.getSize() +1;} diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc new file mode 100644 index 0000000..dc8f1cd --- /dev/null +++ b/src/Interpreter/smtinterpreter.cc @@ -0,0 +1,211 @@ +#include "smtinterpreter.h" +#include +#include "signatureenc.h" +#include "structs.h" +#include "csolver.h" +#include "boolean.h" +#include "predicate.h" +#include "element.h" +#include "set.h" +#include "function.h" +#include "inc_solver.h" +#include +#include "cppvector.h" +#include "smtsig.h" + +using namespace std; + +#define SMTFILENAME "satune.smt" +#define SMTSOLUTIONFILE "solution.sol" + +SMTInterpreter::SMTInterpreter(CSolver *_solver): + Interpreter(_solver) +{ + output.open(SMTFILENAME); + if(!output.is_open()){ + model_print("AlloyEnc:Error in opening the dump file satune.smt\n"); + exit(-1); + } +} + +SMTInterpreter::~SMTInterpreter(){ + if(output.is_open()){ + output.close(); + } +} + + +ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){ + return new SMTBoolSig(id); +} + +ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){ + return new SMTElementSig(id, (SMTSetSig *)ssig); +} + +Signature *SMTInterpreter::getSetSignature(uint id, Set *set){ + return new SMTSetSig(id, set); +} + +void SMTInterpreter::dumpAllConstraints(Vector &facts){ + for(uint i=0; i< facts.getSize(); i++){ + char *cstr = facts.get(i); + writeToFile("(assert " + string(cstr) + ")"); + } +} + +void SMTInterpreter::extractValue(char *idline, char *valueline){ + uint id; + if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){ + char valuestr [512]; + ASSERT(1 == sscanf(valueline,"%s)", valuestr)); + uint value; + if (strcmp (valuestr, "true)") == 0 ){ + value =1; + }else if (strcmp(valuestr, "false)") == 0){ + value = 0; + }else { + ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value)); + } + + model_print("Signature%u = %u\n", id, value); + sigEnc.setValue(id, value); + } else { + ASSERT(0); + } +} + +int SMTInterpreter::getResult(){ + ifstream input(SMTSOLUTIONFILE, ios::in); + string line; + while(getline(input, line)){ + if(line.find("unsat")!= line.npos){ + return IS_UNSAT; + } + if(line.find("(define-fun") != line.npos){ + string valueline; + ASSERT(getline(input, valueline)); + char cline [line.size()+1]; + strcpy ( cline, line.c_str() ); + char vline [valueline.size()+1]; + strcpy ( vline, valueline.c_str() ); + extractValue(cline, vline); + } + } + return IS_SAT; +} + +void SMTInterpreter::dumpFooter(){ + output << "(check-sat)" << endl; + output << "(get-model)" << endl; +} + +void SMTInterpreter::dumpHeader(){ +} + +void SMTInterpreter::compileRunCommand(char * command, size_t size){ + snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE); +} + +string SMTInterpreter::negateConstraint(string constr){ + return "( not " + constr + " )"; +} + +string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){ + uint size = bl->inputs.getSize(); + string array[size]; + for (uint i = 0; i < size; i++) + array[i] = encodeConstraint(bl->inputs.get(i)); + string op; + switch (bl->op){ + case SATC_OR: + op = "or"; + break; + case SATC_AND: + op = "and"; + break; + case SATC_NOT: + op = "not"; + break; + case SATC_IMPLIES: + op = "=>"; + break; + case SATC_XOR: + default: + ASSERT(0); + } + switch (bl->op) { + case SATC_XOR: + case SATC_OR: + case SATC_AND:{ + ASSERT(size >= 2); + string res = array[0]; + for( uint i=1; i< size; i++){ + res = "( " + op + " " + res + " " + array[i] + " )"; + } + return res; + } + case SATC_NOT:{ + return "( not " + array[0] + " )"; + } + case SATC_IMPLIES: + return "( " + op + " " + array[0] + " " + array[1] + " )"; + case SATC_IFF: + default: + ASSERT(0); + + } +} + +string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){ + ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv); + return *boolSig + ""; +} + +string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){ + FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction(); + uint numDomains = elemFunc->inputs.getSize(); + ASSERT(numDomains > 1); + ValuedSignature *inputs[numDomains]; + string result; + for (uint i = 0; i < numDomains; i++) { + Element *elem = elemFunc->inputs.get(i); + inputs[i] = sigEnc.getElementSignature(elem); + if(elem->type == ELEMFUNCRETURN){ + result += processElementFunction((ElementFunction *) elem, inputs[i]); + } + } + string op; + switch(function->op){ + case SATC_ADD: + op = "+"; + break; + case SATC_SUB: + op = "-"; + break; + default: + ASSERT(0); + } + result += "( = " + *signature; + string tmp = "" + *inputs[0]; + for (uint i = 1; i < numDomains; i++) { + tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )"; + } + result += tmp + " )"; + return result; +} + +string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){ + switch (op) { + case SATC_EQUALS: + return "( = " + *elemSig1 + " " + *elemSig2 +" )"; + case SATC_LT: + return "( < " + *elemSig1 + " " + *elemSig2 + " )"; + case SATC_GT: + return "(> " + *elemSig1 + " " + *elemSig2 + " )"; + default: + ASSERT(0); + } +} + + diff --git a/src/Interpreter/smtinterpreter.h b/src/Interpreter/smtinterpreter.h new file mode 100644 index 0000000..ac62fd7 --- /dev/null +++ b/src/Interpreter/smtinterpreter.h @@ -0,0 +1,31 @@ +#ifndef SMTINTERPRETER_H +#define SMTINTERPRETER_H + +#include "classlist.h" +#include "signatureenc.h" +#include "interpreter.h" +#include +#include + +class SMTInterpreter: public Interpreter{ +public: + SMTInterpreter(CSolver *solver); + virtual ValuedSignature *getBooleanSignature(uint id); + virtual ValuedSignature *getElementSignature(uint id, Signature *ssig); + virtual Signature *getSetSignature(uint id, Set *set); + virtual ~SMTInterpreter(); +protected: + virtual void dumpFooter(); + virtual void dumpHeader(); + virtual void compileRunCommand(char * command , size_t size); + virtual int getResult(); + virtual void dumpAllConstraints(Vector &facts); + virtual string negateConstraint(string constr); + virtual string encodeBooleanLogic( BooleanLogic *bl); + virtual string encodeBooleanVar( BooleanVar *bv); + void extractValue(char *idline, char *valueline); + virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature); + virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2); +}; + +#endif diff --git a/src/Interpreter/smtsig.cc b/src/Interpreter/smtsig.cc new file mode 100644 index 0000000..4c77493 --- /dev/null +++ b/src/Interpreter/smtsig.cc @@ -0,0 +1,81 @@ +#include "smtsig.h" +#include "set.h" + +SMTBoolSig::SMTBoolSig(uint id): + ValuedSignature(id) +{ +} + +string SMTBoolSig::toString() const{ + return "b" + to_string(id); +} + +string SMTBoolSig::getSignature() const{ + return "(declare-const b" + to_string(id) + " Bool)"; +} + +string SMTBoolSig::getAbsSignature() const{ + return ""; +} + +SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig): + ValuedSignature(id), + ssig(_ssig) +{ +} + +string SMTElementSig::toString() const{ + return "e" + to_string(id); +} + +string SMTElementSig::getSignature() const{ + string str = "(declare-const e" + to_string(id) + " Int)\n"; + string constraint = ssig->getAbsSignature(); + size_t start_pos; + string placeholder = "$"; + while((start_pos = constraint.find(placeholder)) != string::npos){ + constraint.replace(start_pos, placeholder.size(), to_string(id)); + } + //constraint.replace(constraint.begin(), constraint.end(), "$", ); + str += constraint; + return str; +} + +string SMTElementSig::getAbsSignature() const{ + return ""; + +} + +SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){ + ASSERT(set->getSize() > 0); + int min = set->getElement(0), max = set->getElement(set->getSize()-1); + Vector holes; + int prev = set->getElement(0); + for(uint i=1; i< set->getSize(); i++){ + int curr = set->getElement(i); + if(prev != curr -1){ + for(int j=prev+1; j< curr; j++){ + holes.push(j); + } + } + prev = curr; + } + constraint = "(assert (<= e$ " + to_string(max) +"))\n"; + constraint += "(assert (>= e$ " + to_string(min) +"))\n"; + for(uint i=0; i< holes.getSize(); i++){ + constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n"; + } +} + +string SMTSetSig::toString() const{ + return ""; +} + +string SMTSetSig::getSignature() const{ + return ""; +} + +string SMTSetSig::getAbsSignature() const{ + return constraint; + +} diff --git a/src/Interpreter/smtsig.h b/src/Interpreter/smtsig.h new file mode 100644 index 0000000..7804176 --- /dev/null +++ b/src/Interpreter/smtsig.h @@ -0,0 +1,40 @@ +#ifndef SMTSIG_H +#define SMTSIG_H +#include +#include +#include "signature.h" +#include "classlist.h" +using namespace std; + +class SMTBoolSig: public ValuedSignature{ +public: + SMTBoolSig(uint id); + virtual ~SMTBoolSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +}; + +class SMTSetSig: public Signature{ +public: + SMTSetSig(uint id, Set *set); + virtual ~SMTSetSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +private: + string constraint; +}; + +class SMTElementSig: public ValuedSignature{ +public: + SMTElementSig(uint id, SMTSetSig *ssig); + virtual ~SMTElementSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +private: + SMTSetSig *ssig; +}; + +#endif diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc index 8b1e3fd..eac11e9 100644 --- a/src/Serialize/deserializer.cc +++ b/src/Serialize/deserializer.cc @@ -17,7 +17,7 @@ #define READBUFFERSIZE 16384 -Deserializer::Deserializer(const char *file, bool alloy) : +Deserializer::Deserializer(const char *file, InterpreterType itype) : buffer((char *) ourmalloc(READBUFFERSIZE)), bufferindex(0), bufferbytes(0), @@ -29,8 +29,8 @@ Deserializer::Deserializer(const char *file, bool alloy) : if (filedesc < 0) { exit(-1); } - if(alloy){ - solver->setAlloyEncoder(); + if(itype != SATUNE){ + solver->setInterpreter(itype); } } diff --git a/src/Serialize/deserializer.h b/src/Serialize/deserializer.h index 6af5880..1a93674 100644 --- a/src/Serialize/deserializer.h +++ b/src/Serialize/deserializer.h @@ -19,7 +19,7 @@ */ class Deserializer { public: - Deserializer(const char *file, bool alloy = false); + Deserializer(const char *file, InterpreterType itype = SATUNE); CSolver *deserialize(); virtual ~Deserializer(); private: diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc index 3cb13fe..187e384 100644 --- a/src/Test/deserializealloytest.cc +++ b/src/Test/deserializealloytest.cc @@ -1,16 +1,32 @@ #include "csolver.h" +InterpreterType getInterpreterType(char * itype){ + if(strcmp (itype,"--alloy") == 0){ + return ALLOY; + } else if(strcmp (itype,"--z3") == 0){ + return Z3; + } else if(strcmp (itype,"--smtrat") == 0){ + return SMTRAT; + } else if(strcmp (itype,"--alloy") == 0){ + return ALLOY; + } else { + printf("Unknown interpreter type: %s\n", itype); + printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsmt]\n"); + exit(-1); + } +} + int main(int argc, char **argv) { printf("%d\n", argc); if (argc != 2 && argc != 3) { printf("You only specify the name of the file ...\n"); - printf("./run.sh deserializer test.dump [--alloy]\n"); + printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsmt]\n"); exit(-1); } CSolver *solver; if(argc == 3){ - solver = CSolver::deserialize(argv[1], true); + solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2])); } else { solver = CSolver::deserialize(argv[1]); } diff --git a/src/ccsolver.cc b/src/ccsolver.cc index e5958ed..7acd00f 100644 --- a/src/ccsolver.cc +++ b/src/ccsolver.cc @@ -145,8 +145,8 @@ void mustHaveValue(void *solver, void *element) { CCSOLVER(solver)->mustHaveValue( (Element *) element); } -void setAlloyEncoder(void *solver){ - CCSOLVER(solver)->setAlloyEncoder(); +void setInterpreter(void *solver, unsigned int type){ + CCSOLVER(solver)->setInterpreter((InterpreterType)type); } void *clone(void *solver) { diff --git a/src/classlist.h b/src/classlist.h index d81b9bc..9616bc2 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -75,9 +75,9 @@ class EncodingSubGraph; class SignatureEnc; class Signature; class ValuedSignature; -class ElementSig; -class SetSig; -class BooleanSig; +class AlloyElementSig; +class AlloySetSig; +class AlloyBoolSig; struct IncrementalSolver; typedef struct IncrementalSolver IncrementalSolver; struct TableEntry; diff --git a/src/csolver.cc b/src/csolver.cc index fd44646..2670e47 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -30,6 +30,7 @@ #include #include #include "alloyinterpreter.h" +#include "smtinterpreter.h" CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -162,9 +163,9 @@ CSolver *CSolver::clone() { return copy; } -CSolver *CSolver::deserialize(const char *file, bool alloy) { +CSolver *CSolver::deserialize(const char *file, InterpreterType itype) { model_print("deserializing %s ...\n", file); - Deserializer deserializer(file, alloy); + Deserializer deserializer(file, itype); return deserializer.deserialize(); } @@ -394,7 +395,7 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin } BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { - if(!useAlloyCompiler()){ + if(!useInterpreter()){ BooleanEdge newarray[asize]; switch (op) { case SATC_NOT: { @@ -494,7 +495,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco } } Boolean *constraint = new BooleanOrder(order, first, second); - if (!useAlloyCompiler() ){ + if (!useInterpreter() ){ Boolean *b = boolMap.get(constraint); if (b == NULL) { @@ -531,7 +532,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco } void CSolver::addConstraint(BooleanEdge constraint) { - if(!useAlloyCompiler()){ + if(!useInterpreter()){ if (isTrue(constraint)) return; else if (isFalse(constraint)) { @@ -609,11 +610,11 @@ int CSolver::solve() { deleteTuner = true; } int result = IS_INDETER; - if(useAlloyCompiler()){ + if(useInterpreter()){ interpreter->encode(); - model_print("Problem encoded in Alloy\n"); + model_print("Problem encoded in Interpreter\n"); result = interpreter->solve(); - model_print("Problem solved by Alloy\n"); + model_print("Problem solved by Interpreter\n"); } else{ { @@ -679,9 +680,23 @@ int CSolver::solve() { return result; } -void CSolver::setAlloyEncoder(){ +void CSolver::setInterpreter(InterpreterType type){ if(interpreter == NULL){ - interpreter = new AlloyInterpreter(this); + switch(type){ + case SATUNE: + break; + case ALLOY:{ + interpreter = new AlloyInterpreter(this); + break; + }case Z3:{ + interpreter = new SMTInterpreter(this); + break; + } + case MATHSAT: + case SMTRAT: + default: + ASSERT(0); + } } } @@ -703,7 +718,7 @@ uint64_t CSolver::getElementValue(Element *element) { case ELEMSET: case ELEMCONST: case ELEMFUNCRETURN: - return useAlloyCompiler()? interpreter->getValue(element): + return useInterpreter()? interpreter->getValue(element): getElementValueSATTranslator(this, element); default: ASSERT(0); @@ -715,7 +730,7 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) { Boolean *boolean = bedge.getBoolean(); switch (boolean->type) { case BOOLEANVAR: - return useAlloyCompiler()? interpreter->getBooleanValue(boolean): + return useInterpreter()? interpreter->getBooleanValue(boolean): getBooleanVariableValueSATTranslator(this, boolean); default: ASSERT(0); diff --git a/src/csolver.h b/src/csolver.h index 7da50c5..d7ccdb5 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -161,12 +161,12 @@ public: void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb); CSolver *clone(); void serialize(); - static CSolver *deserialize(const char *file, bool alloy = false); + static CSolver *deserialize(const char *file, InterpreterType itype = SATUNE); void autoTune(uint budget); void inferFixedOrders(); void inferFixedOrder(Order *order); - void setAlloyEncoder(); - bool useAlloyCompiler() {return interpreter != NULL;} + void setInterpreter(InterpreterType type); + bool useInterpreter() {return interpreter != NULL;} void setTuner(Tuner *_tuner) { tuner = _tuner; } long long getElapsedTime() { return elapsedTime; } long long getEncodeTime(); diff --git a/src/pycsolver.py b/src/pycsolver.py index 7c3440e..000ff18 100644 --- a/src/pycsolver.py +++ b/src/pycsolver.py @@ -113,7 +113,7 @@ def loadCSolver(): csolverlb.clone.restype = c_void_p csolverlb.serialize.argtypes = [c_void_p] csolverlb.serialize.restype = None - csolverlb.setAlloyEncoder.argtypes = [c_void_p] - csolverlb.setAlloyEncoder.restype = None + csolverlb.setInterpreter.argtypes = [c_void_p, c_uint] + csolverlb.setInterpreter.restype = None return csolverlb