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
#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;
}
}
+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++){
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);
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(){
}
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);
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;
-#ifndef ALLOYENC_H
-#define ALLOYENC_H
+#ifndef ALLOYINTERPRETER_H
+#define ALLOYINTERPRETER_H
#include "classlist.h"
#include "signatureenc.h"
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);
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
--- /dev/null
+#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";
+
+}
--- /dev/null
+#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
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);
}
}
void Interpreter::writeToFile(string str){
- output << str << endl;
+ if(!str.empty()){
+ output << str << endl;
+ }
}
bool Interpreter::getBooleanValue(Boolean *b){
#include "classlist.h"
#include "signatureenc.h"
+#include "signature.h"
#include <iostream>
#include <fstream>
using namespace std;
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;
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;
#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)
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;
}
-#ifndef ELEMENTSIG_H
-#define ELEMENTSIG_H
+#ifndef SIGNATURE_H
+#define SIGNATURE_H
#include <string>
#include <iostream>
#include "classlist.h"
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
#include "element.h"
#include "set.h"
#include "signature.h"
-#include "alloyinterpreter.h"
-#include "math.h"
+#include "interpreter.h"
SignatureEnc::SignatureEnc(Interpreter *inter):
interpreter(inter),
}
}
-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){
}
}
-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());
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());
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;}
--- /dev/null
+#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);
+ }
+}
+
+
--- /dev/null
+#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
--- /dev/null
+#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;
+
+}
--- /dev/null
+#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
#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),
if (filedesc < 0) {
exit(-1);
}
- if(alloy){
- solver->setAlloyEncoder();
+ if(itype != SATUNE){
+ solver->setInterpreter(itype);
}
}
*/
class Deserializer {
public:
- Deserializer(const char *file, bool alloy = false);
+ Deserializer(const char *file, InterpreterType itype = SATUNE);
CSolver *deserialize();
virtual ~Deserializer();
private:
#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]);
}
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) {
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;
#include <time.h>
#include <stdarg.h>
#include "alloyinterpreter.h"
+#include "smtinterpreter.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
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();
}
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
- if(!useAlloyCompiler()){
+ if(!useInterpreter()){
BooleanEdge newarray[asize];
switch (op) {
case SATC_NOT: {
}
}
Boolean *constraint = new BooleanOrder(order, first, second);
- if (!useAlloyCompiler() ){
+ if (!useInterpreter() ){
Boolean *b = boolMap.get(constraint);
if (b == NULL) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if(!useAlloyCompiler()){
+ if(!useInterpreter()){
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
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{
{
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);
+ }
}
}
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return useAlloyCompiler()? interpreter->getValue(element):
+ return useInterpreter()? interpreter->getValue(element):
getElementValueSATTranslator(this, element);
default:
ASSERT(0);
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);
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();
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
projects / satune.git / commitdiff