From: Hamed Gorjiara Date: Tue, 22 Jan 2019 08:20:39 +0000 (-0800) Subject: Alloy interpreter X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=342c3e59b76a3e79741a0867f7770255eaa82c63 Alloy interpreter --- diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc new file mode 100644 index 0000000..c7acf23 --- /dev/null +++ b/src/AlloyEnc/alloyenc.cc @@ -0,0 +1,182 @@ +#include "alloyenc.h" +#include +#include "signatureenc.h" +#include "structs.h" +#include "csolver.h" +#include "boolean.h" +#include "predicate.h" +#include "element.h" +#include "signature.h" +#include +#include + +using namespace std; + +const char * AlloyEnc::alloyFileName = "satune.als"; +const char * AlloyEnc::solutionFile = "solution.sol"; + +AlloyEnc::AlloyEnc(CSolver *_solver): + csolver(_solver), + sigEnc(this) +{ + output.open(alloyFileName); + if(!output.is_open()){ + model_print("AlloyEnc:Error in opening the dump file satune.als\n"); + exit(-1); + } +} + +AlloyEnc::~AlloyEnc(){ + if(output.is_open()){ + output.close(); + } +} + +void AlloyEnc::encode(){ + SetIteratorBooleanEdge *iterator = csolver->getConstraints(); + Vector facts; + while(iterator->hasNext()){ + BooleanEdge constraint = iterator->next(); + string constr = encodeConstraint(constraint); + //model_print("constr=%s\n", constr.c_str()); + char *cstr = new char [constr.length()+1]; + strcpy (cstr, constr.c_str()); + facts.push(cstr); + } + output << "fact {" << endl; + for(uint i=0; i< facts.getSize(); i++){ + char *cstr = facts.get(i); + writeToFile(cstr); + delete[] cstr; + } + output << "}" << endl; + delete iterator; +} + +int AlloyEnc::getResult(){ + ifstream input(solutionFile, ios::in); + string line; + while(getline(input, line)){ + if(regex_match(line, regex("Unsatisfiable."))){ + return IS_UNSAT; + } + if(regex_match(line, regex(".*Element\\d+.*value=.*Element\\d+.*->\\d+.*"))){ + int tmp=0, index=0, value=0; + const char* s = line.c_str(); + uint i1, i2, i3; + uint64_t i4; + if (4 == sscanf(s,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3, &i4)){ + model_print("Element%d = %" PRId64 "\n", i1, i4); + sigEnc.setValue(i1, i4); + } + } + } + return IS_SAT; +} + +int AlloyEnc::solve(){ + int result = IS_INDETER; + char buffer [512]; + if( output.is_open()){ + output.close(); + } + snprintf(buffer, sizeof(buffer), "./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile); + int status = system(buffer); + if (status == 0) { + //Read data in from results file + result = getResult(); + } + return result; +} + +string AlloyEnc::encodeConstraint(BooleanEdge c){ + Boolean *constraint = c.getBoolean(); + string res; + switch(constraint->type){ + case LOGICOP:{ + res = encodeBooleanLogic((BooleanLogic *) constraint); + break; + } + case PREDICATEOP:{ + res = encodePredicate((BooleanPredicate *) constraint); + break; + } + default: + ASSERT(0); + } + if(c.isNegated()){ + return "not ( " + res + " )"; + } + return res; +} + +string AlloyEnc::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)); + switch (bl->op) { + case SATC_AND:{ + ASSERT(size >= 2); + string res = ""; + res += array[0]; + for( uint i=1; i< size; i++){ + res += " and " + array[i]; + } + return res; + } + case SATC_NOT:{ + return "not " + array[0]; + } + case SATC_IFF: + return array[0] + " iff " + array[1]; + case SATC_OR: + case SATC_XOR: + case SATC_IMPLIES: + default: + ASSERT(0); + + } +} + +string AlloyEnc::encodePredicate( BooleanPredicate *bp){ + switch (bp->predicate->type) { + case TABLEPRED: + ASSERT(0); + case OPERATORPRED: + return encodeOperatorPredicate(bp); + default: + ASSERT(0); + } +} + +string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){ + PredicateOperator *predicate = (PredicateOperator *) constraint->predicate; + ASSERT(constraint->inputs.getSize() == 2); + Element *elem0 = constraint->inputs.get(0); + ASSERT(elem0->type = ELEMSET); + ElementSig *elemSig1 = sigEnc.getElementSignature(elem0); + Element *elem1 = constraint->inputs.get(1); + ASSERT(elem1->type = ELEMSET); + ElementSig *elemSig2 = sigEnc.getElementSignature(elem1); + switch (predicate->getOp()) { + case SATC_EQUALS: + return *elemSig1 + " = " + *elemSig2; + case SATC_LT: + return *elemSig1 + " < " + *elemSig2; + case SATC_GT: + return *elemSig1 + " > " + *elemSig2; + default: + ASSERT(0); + } + exit(-1); +} + +void AlloyEnc::writeToFile(string str){ + output << str << endl; +} + +uint64_t AlloyEnc::getValue(Element * element){ + return sigEnc.getValue(element); +} + diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h new file mode 100644 index 0000000..94d991e --- /dev/null +++ b/src/AlloyEnc/alloyenc.h @@ -0,0 +1,31 @@ +#ifndef ALLOYENC_H +#define ALLOYENC_H + +#include "classlist.h" +#include "signatureenc.h" +#include +#include +using namespace std; + +class AlloyEnc{ +public: + AlloyEnc(CSolver *solver); + void encode(); + int solve(); + void writeToFile(string str); + uint64_t getValue(Element * element); + ~AlloyEnc(); +private: + string encodeConstraint(BooleanEdge constraint); + int getResult(); + string encodeBooleanLogic( BooleanLogic *bl); + string encodePredicate( BooleanPredicate *bp); + string encodeOperatorPredicate(BooleanPredicate *constraint); + CSolver *csolver; + SignatureEnc sigEnc; + ofstream output; + static const char * alloyFileName; + static const char * solutionFile; +}; + +#endif diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc new file mode 100644 index 0000000..9b02d32 --- /dev/null +++ b/src/AlloyEnc/signature.cc @@ -0,0 +1,51 @@ +#include "signature.h" +#include "set.h" + +ElementSig::ElementSig(uint id, SetSig *_ssig): + Signature(id), + ssig(_ssig) +{ + +} + +string ElementSig::toString() const{ + return "Element" + to_string(id) + ".value"; +} + +string ElementSig::getSignature() const{ + return "one sig Element" + to_string(id) + " {\n\ + value: Int\n\ + }{\n\ + value in " + *ssig + "\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{ + return "one sig Set" + to_string(id) + " {\n\ + domain: set Int\n\ + }{\n\ + domain = " + domain + "\n\ + }"; + +} + +string Signature::operator+(const string& str){ + return toString() + str; +} + +string operator+(const string& str, const Signature& sig){ + return str + sig.toString(); +} diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h new file mode 100644 index 0000000..6dcb2e9 --- /dev/null +++ b/src/AlloyEnc/signature.h @@ -0,0 +1,44 @@ +#ifndef ELEMENTSIG_H +#define ELEMENTSIG_H +#include +#include +#include "classlist.h" +using namespace std; + +class Signature{ +public: + Signature(uint _id):id(_id){} + string operator+(const string& s); + virtual string toString() const = 0; + virtual string getSignature() const =0; + virtual ~Signature(){} +protected: + uint id; +}; + +class SetSig: public Signature{ +public: + SetSig(uint id, Set *set); + virtual ~SetSig(){} + virtual string toString() const; + virtual string getSignature() const; +private: + string domain; +}; + +class ElementSig: public Signature{ +public: + ElementSig(uint id, SetSig *ssig); + uint64_t getValue() { return value;} + void setValue(uint64_t v){value = v;} + virtual ~ElementSig(){} + virtual string toString() const; + virtual string getSignature() const; +private: + SetSig *ssig; + uint64_t value; +}; + +string operator+(const string& str, const Signature& sig); + +#endif diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc new file mode 100644 index 0000000..4c11957 --- /dev/null +++ b/src/AlloyEnc/signatureenc.cc @@ -0,0 +1,46 @@ +#include "signatureenc.h" +#include "element.h" +#include "set.h" +#include "signature.h" +#include "alloyenc.h" + +SignatureEnc::SignatureEnc(AlloyEnc *ae): alloyEncoder(ae){ +} + +SignatureEnc::~SignatureEnc(){ + for(uint i=0; igetRange(); + SetSig *ssig = (SetSig *)encoded.get((void *)set); + if(ssig == NULL){ + ssig = new SetSig(signatures.getSize(), set); + encoded.put(set, ssig); + signatures.push(ssig); + alloyEncoder->writeToFile(ssig->getSignature()); + } + esig = new ElementSig(signatures.getSize(), ssig); + encoded.put(element, esig); + signatures.push(esig); + alloyEncoder->writeToFile(esig->getSignature()); + + } + return esig; +} + +void SignatureEnc::setValue(uint id, uint64_t value){ + ElementSig *sig = (ElementSig *)signatures.get(id); + sig->setValue(value); +} + +uint64_t SignatureEnc::getValue(Element *element){ + ElementSig *sig = (ElementSig *)encoded.get((void *) element); + ASSERT(sig != NULL); + return sig->getValue(); +} diff --git a/src/AlloyEnc/signatureenc.h b/src/AlloyEnc/signatureenc.h new file mode 100644 index 0000000..d98a636 --- /dev/null +++ b/src/AlloyEnc/signatureenc.h @@ -0,0 +1,20 @@ +#ifndef SIGNATUREENC_H +#define SIGNATUREENC_H + +#include "classlist.h" +#include "structs.h" +#include "cppvector.h" + +class SignatureEnc { +public: + SignatureEnc(AlloyEnc *_alloyEncoder); + ~SignatureEnc(); + void setValue(uint id, uint64_t value); + ElementSig *getElementSignature(Element *element); + uint64_t getValue(Element *element); +private: + CloneMap encoded; + Vector signatures; + AlloyEnc *alloyEncoder; +}; +#endif diff --git a/src/Makefile b/src/Makefile index 838a478..457ca9a 100644 --- a/src/Makefile +++ b/src/Makefile @@ -4,17 +4,17 @@ PHONY += directories MKDIR_P = mkdir -p OBJ_DIR = bin -CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) +CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) $(wildcard AlloyEnc/*.cc) -C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) +C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard AlloyEnc/*.c) -HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) +HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard AlloyEnc/*.h) OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o) CFLAGS := -Wall -O0 -g CXXFLAGS := -std=c++1y -pthread -CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize +CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IAlloyEnc LDFLAGS := -ldl -lrt -rdynamic -g SHARED := -shared @@ -44,6 +44,7 @@ ${OBJ_DIR}: ${MKDIR_P} ${OBJ_DIR}/Backend ${MKDIR_P} ${OBJ_DIR}/Encoders ${MKDIR_P} ${OBJ_DIR}/Serialize + ${MKDIR_P} ${OBJ_DIR}/AlloyEnc debug: CFLAGS += -DCONFIG_DEBUG debug: all diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc new file mode 100644 index 0000000..2d6cc25 --- /dev/null +++ b/src/Test/deserializealloytest.cc @@ -0,0 +1,23 @@ +#include "csolver.h" + + +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"); + exit(-1); + } + CSolver *solver = CSolver::deserialize(argv[1]); + if(argc == 3) + solver->setAlloyEncode(); + int value = solver->solve(); + if (value == 1) { + printf("%s is SAT\n", argv[1]); + } else { + printf("%s is UNSAT\n", argv[1]); + } + delete solver; + return 1; + +} diff --git a/src/Test/deserializertest.cc b/src/Test/deserializertest.cc deleted file mode 100644 index c8d35c9..0000000 --- a/src/Test/deserializertest.cc +++ /dev/null @@ -1,14 +0,0 @@ -#include "csolver.h" - - -int main(int argc, char **argv) { - if (argc != 2) { - printf("You only specify the name of the file ..."); - exit(-1); - } - CSolver *solver = CSolver::deserialize(argv[1]); - solver->printConstraints(); - delete solver; - return 1; - -} diff --git a/src/Test/run.sh b/src/Test/run.sh index 4590ede..870ba15 100755 --- a/src/Test/run.sh +++ b/src/Test/run.sh @@ -1,5 +1,6 @@ #!/bin/bash +export CLASSPATH=../bin/original.jar:.:$CLASSPATH export LD_LIBRARY_PATH=../bin # For Mac OSX export DYLD_LIBRARY_PATH=../bin diff --git a/src/ccsolver.cc b/src/ccsolver.cc index f9ebdbb..69d002e 100644 --- a/src/ccsolver.cc +++ b/src/ccsolver.cc @@ -145,6 +145,10 @@ void mustHaveValue(void *solver, void *element) { CCSOLVER(solver)->mustHaveValue( (Element *) element); } +void setAlloyEncode(void *solver){ + CCSOLVER(solver)->setAlloyEncode(); +} + void *clone(void *solver) { return CCSOLVER(solver)->clone(); } \ No newline at end of file diff --git a/src/ccsolver.h b/src/ccsolver.h index c88214e..b4a803a 100644 --- a/src/ccsolver.h +++ b/src/ccsolver.h @@ -41,6 +41,7 @@ int getOrderConstraintValue(void *solver,void *order, long first, long second); void printConstraints(void *solver); void serialize(void *solver); void mustHaveValue(void *solver, void *element); +void setAlloyEncode(void *solver); void *clone(void *solver); #ifdef __cplusplus } diff --git a/src/classes.h b/src/classes.h index 58f5a02..6f476ee 100644 --- a/src/classes.h +++ b/src/classes.h @@ -28,6 +28,7 @@ class Set; class BooleanLogic; class Serializer; class ElementFunction; +class AlloyEnc; typedef uint64_t VarType; typedef unsigned int uint; diff --git a/src/classlist.h b/src/classlist.h index c182063..3986a30 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -72,7 +72,10 @@ class EncodingGraph; class EncodingNode; class EncodingEdge; class EncodingSubGraph; - +class SignatureEnc; +class Signature; +class ElementSig; +class SetSig; struct IncrementalSolver; typedef struct IncrementalSolver IncrementalSolver; struct TableEntry; diff --git a/src/csolver.cc b/src/csolver.cc index 45163be..a8eb999 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -29,6 +29,7 @@ #include "varorderingopt.h" #include #include +#include "alloyenc.h" CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -37,7 +38,8 @@ CSolver::CSolver() : booleanVarUsed(false), tuner(NULL), elapsedTime(0), - satsolverTimeout(NOTIMEOUT) + satsolverTimeout(NOTIMEOUT), + alloyEncoder(NULL) { satEncoder = new SATEncoder(this); } @@ -638,11 +640,17 @@ int CSolver::solve() { model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC); model_print("Is problem UNSAT after encoding: %d\n", unsat); - int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout); - model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT"); - time2 = getTimeNano(); - elapsedTime = time2 - startTime; - model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC); + int result = IS_INDETER; + if(alloyEncoder != NULL){ + alloyEncoder->encode(); + result = alloyEncoder->solve(); + }else{ + result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout); + model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT"); + time2 = getTimeNano(); + elapsedTime = time2 - startTime; + model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC); + } if (deleteTuner) { delete tuner; tuner = NULL; @@ -650,6 +658,10 @@ int CSolver::solve() { return result; } +void CSolver::setAlloyEncode(){ + alloyEncoder = new AlloyEnc(this); +} + void CSolver::printConstraints() { SetIteratorBooleanEdge *it = getConstraints(); while (it->hasNext()) { @@ -668,7 +680,8 @@ uint64_t CSolver::getElementValue(Element *element) { case ELEMSET: case ELEMCONST: case ELEMFUNCRETURN: - return getElementValueSATTranslator(this, element); + return alloyEncoder == NULL? getElementValueSATTranslator(this, element): + alloyEncoder->getValue(element); default: ASSERT(0); } diff --git a/src/csolver.h b/src/csolver.h index c604486..0dc3cef 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -165,7 +165,7 @@ public: void autoTune(uint budget); void inferFixedOrders(); void inferFixedOrder(Order *order); - + void setAlloyEncode(); void setTuner(Tuner *_tuner) { tuner = _tuner; } long long getElapsedTime() { return elapsedTime; } @@ -222,6 +222,7 @@ private: Tuner *tuner; long long elapsedTime; long satsolverTimeout; + AlloyEnc *alloyEncoder; friend class ElementOpt; friend class VarOrderingOpt; }; diff --git a/src/pycsolver.py b/src/pycsolver.py index b0e43a9..da911db 100644 --- a/src/pycsolver.py +++ b/src/pycsolver.py @@ -113,5 +113,7 @@ def loadCSolver(): csolverlb.clone.restype = c_void_p csolverlb.serialize.argtypes = [c_void_p] csolverlb.serialize.restype = None + csolverlb.setAlloyEncode.argtypes = [c_void_p] + csolverlb.setAlloyEncode.restype = None return csolverlb