Adding SMT Interpreters

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 8b082025348ffaeab34916512eb55368068473d9..6d6fd97a36242e1eac656145f145fc05bd348c86 100644 (file)
--- 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 f910ac60529453a2d8ed660c625d9704c358e6d5..c0e4a6094d97b8784fb8680eba9656f3e454d088 100644 (file)
--- 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 <fstream>
 #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<char *> &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 ec2e4a3f9dc120d780f437a79d16172d8e627d15..e4a1e3b0531761aa33bde0e41868a163d7b57d3a 100644 (file)
--- 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<char *> &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 (file)
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 (file)
index 0000000..3fb2d10
--- /dev/null
+++ b/src/Interpreter/alloysig.h
@@ -0,0 +1,44 @@
+#ifndef ALLOYSIG_H
+#define ALLOYSIG_H
+#include <string>
+#include <iostream>
+#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 bab92b474256294f024b783f5ef074a19afdf378..d87cbd9fbad083de008e8f82a9ce656c82ffc9cd 100644 (file)
--- 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 814511bf5496543ec6534f2cb8486a2a268d5206..32eed4a0de824a1d63d021682e6cad3ae009dba6 100644 (file)
--- a/src/Interpreter/interpreter.h
+++ b/src/Interpreter/interpreter.h
@@ -3,6 +3,7 @@
 
 #include "classlist.h"
 #include "signatureenc.h"
+#include "signature.h"
 #include <iostream>
 #include <fstream>
 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 ad7d2e700fe9b81bbf2f3268c5340e07718c66bf..94efbb2303cf850f7bfe47e0ed1621ff97aab810 100644 (file)
--- 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 1b321a6f134590f8d7bbac8fbcece632119d9861..e8c9e1c999c499207d2399d4119834c513655d11 100644 (file)
--- 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 <string>
 #include <iostream>
 #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 5e0a900206a078ae23e47522ced89827db46b2aa..cdc8aa11b26a7fce870bed915f85c43fa88cbfb7 100644 (file)
--- 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 b195d032eb9de69c89863f51032151cf404a7d93..988ac71c84af8ffc83a815d1a60d7ea8b2406d6d 100644 (file)
--- 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 (file)
index 0000000..dc8f1cd
--- /dev/null
+++ b/src/Interpreter/smtinterpreter.cc
@@ -0,0 +1,211 @@
+#include "smtinterpreter.h"
+#include <string>
+#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 <fstream>
+#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<char *> &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 (file)
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 <iostream>
+#include <fstream>
+
+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<char *> &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 (file)
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<int> 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 (file)
index 0000000..7804176
--- /dev/null
+++ b/src/Interpreter/smtsig.h
@@ -0,0 +1,40 @@
+#ifndef SMTSIG_H
+#define SMTSIG_H
+#include <string>
+#include <iostream>
+#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 8b1e3fd00cf1a81745763b8f0236dafea783a249..eac11e9709296311733611220024de8898f34a4a 100644 (file)
--- 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 6af58800ca8ec739be548f4e062bb7bf0c631642..1a936743576dd3b8522ea69c2e0b2bf5464073bb 100644 (file)
--- 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 3cb13feb95f9fc8b3c2147f02d55fe29826081c5..187e384617ebbd1c4a45a2548bc64d92c70d98ce 100644 (file)
--- 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 e5958ed5cc89aa8ca5641d0307fd255d3dc90624..7acd00f4f4eb00ac48c9163e36527d6ea03b078b 100644 (file)
--- 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 d81b9bc9c6e683e8f45d8cc67df45f73dd392b45..9616bc2e7154adc2f55eaba6bc6cab22169e9140 100644 (file)
--- 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 fd4464686ad8afbe99b268a078d97f786ff49835..2670e4745a24c0371aaa4db082be7890bec86666 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -30,6 +30,7 @@
 #include <time.h>
 #include <stdarg.h>
 #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 7da50c55b9bf60667e994cf50bb8178d5f009f3d..d7ccdb53ee3bd58f46857b7ceb496fa7440b1923 100644 (file)
--- 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 7c3440e03b028eb794797b097eb9d23505e36ea7..000ff18f63663264b44bf508637cc241cd83ac03 100644 (file)
--- 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