+++ /dev/null
-#include "alloyenc.h"
-#include <string>
-#include "signatureenc.h"
-#include "structs.h"
-#include "csolver.h"
-#include "boolean.h"
-#include "predicate.h"
-#include "element.h"
-#include "signature.h"
-#include "set.h"
-#include "function.h"
-#include "inc_solver.h"
-#include <fstream>
-#include <vector>
-
-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(){
- dumpAlloyHeader();
- SetIteratorBooleanEdge *iterator = csolver->getConstraints();
- Vector<char *> facts;
- while(iterator->hasNext()){
- BooleanEdge constraint = iterator->next();
- string constr = encodeConstraint(constraint);
- 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;
-}
-
-void tokenize(string const &str, const char delim, vector<std::string> &out)
-{
- size_t start;
- size_t end = 0;
-
- while ((start = str.find_first_not_of(delim, end)) != string::npos)
- {
- end = str.find(delim, start);
- out.push_back(str.substr(start, end - start));
- }
-}
-
-int AlloyEnc::getResult(){
- ifstream input(solutionFile, ios::in);
- string line;
- while(getline(input, line)){
- if(line.find("Unsatisfiable.")== 0){
- return IS_UNSAT;
- }
- if(line.find("univ") == 0){
- continue;
- }
- if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
- vector<string> values;
- const char delim = ',';
- tokenize(line, delim, values);
- for (uint i=0; i<values.size(); i++){
- uint i1, i2, i3;
- if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
- model_print("Signature%u = %u\n", i1, i3);
- sigEnc.setValue(i1, i3);
- }
- }
- }
- }
- return IS_SAT;
-}
-
-void AlloyEnc::dumpAlloyFooter(){
- output << "pred show {}" << endl;
- output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
-}
-
-uint AlloyEnc::getTimeout(){
- uint timeout =csolver->getSatSolverTimeout();
- return timeout == (uint)NOTIMEOUT? 1000: timeout;
-}
-
-void AlloyEnc::dumpAlloyHeader(){
- output << "open util/integer" << endl;
-}
-
-int AlloyEnc::solve(){
- dumpAlloyFooter();
- int result = IS_INDETER;
- char buffer [512];
- if( output.is_open()){
- output.close();
- }
- snprintf(buffer, sizeof(buffer), "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), 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;
- }
- case BOOLEANVAR:{
- res = encodeBooleanVar( (BooleanVar *) 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));
- 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_IFF:
- op = " iff ";
- break;
- case SATC_IMPLIES:
- op = " implies ";
- break;
- case SATC_XOR:
- default:
- ASSERT(0);
- }
- switch (bl->op) {
- case SATC_OR:
- case SATC_AND:{
- ASSERT(size >= 2);
- string res = "( ";
- res += array[0];
- for( uint i=1; i< size; i++){
- res += op + array[i];
- }
- res += " )";
- return res;
- }
- case SATC_NOT:{
- return "not ( " + array[0] + " )";
- }
- case SATC_IMPLIES:
- case SATC_IFF:
- return "( " + array[0] + op + array[1] + " )";
- case SATC_XOR:
- 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::encodeBooleanVar( BooleanVar *bv){
- BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
- return *boolSig + " = 1";
-}
-
-string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
- FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
- uint numDomains = elemFunc->inputs.getSize();
- ASSERT(numDomains > 1);
- ElementSig *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 = ".add";
- break;
- case SATC_SUB:
- op = ".sub";
- break;
- default:
- ASSERT(0);
- }
- result += *signature + " = " + *inputs[0];
- for (uint i = 1; i < numDomains; i++) {
- result += op + "["+ *inputs[i] +"]";
- }
- result += "\n";
- return result;
-}
-
-string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
- PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
- ASSERT(constraint->inputs.getSize() == 2);
- string str;
- Element *elem0 = constraint->inputs.get(0);
- ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
- ElementSig *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);
- if(elem1->type == ELEMFUNCRETURN){
- str += processElementFunction((ElementFunction *) elem1, elemSig2);
- }
- switch (predicate->getOp()) {
- case SATC_EQUALS:
- str += *elemSig1 + " = " + *elemSig2;
- break;
- case SATC_LT:
- str += *elemSig1 + " < " + *elemSig2;
- break;
- case SATC_GT:
- str += *elemSig1 + " > " + *elemSig2;
- break;
- default:
- ASSERT(0);
- }
- return str;
-}
-
-void AlloyEnc::writeToFile(string str){
- output << str << endl;
-}
-
-bool AlloyEnc::getBooleanValue(Boolean *b){
- return (bool)sigEnc.getValue(b);
-}
-
-uint64_t AlloyEnc::getValue(Element * element){
- return (uint64_t)sigEnc.getValue(element);
-}
-
+++ /dev/null
-#ifndef ALLOYENC_H
-#define ALLOYENC_H
-
-#include "classlist.h"
-#include "signatureenc.h"
-#include <iostream>
-#include <fstream>
-using namespace std;
-
-class AlloyEnc{
-public:
- AlloyEnc(CSolver *solver);
- void encode();
- int solve();
- void writeToFile(string str);
- uint64_t getValue(Element *element);
- bool getBooleanValue(Boolean *element);
- ~AlloyEnc();
-private:
- void dumpAlloyFooter();
- void dumpAlloyHeader();
- inline uint getTimeout();
- string encodeConstraint(BooleanEdge constraint);
- int getResult();
- string encodeBooleanLogic( BooleanLogic *bl);
- string encodeBooleanVar( BooleanVar *bv);
- string encodePredicate( BooleanPredicate *bp);
- string encodeOperatorPredicate(BooleanPredicate *constraint);
- string processElementFunction(ElementFunction *element, ElementSig *signature);
- CSolver *csolver;
- SignatureEnc sigEnc;
- ofstream output;
- static const char * alloyFileName;
- static const char * solutionFile;
-};
-
-#endif
+++ /dev/null
-#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)
-{
-}
-
-int ValuedSignature::getValue(){
- ASSERT(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;
-}
-
-string operator+(const string& str, const Signature& sig){
- return str + sig.toString();
-}
+++ /dev/null
-#ifndef ELEMENTSIG_H
-#define ELEMENTSIG_H
-#include <string>
-#include <iostream>
-#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 getAbsSignature() const =0;
- virtual string getSignature() const =0;
- virtual ~Signature(){}
-protected:
- uint id;
-};
-
-class ValuedSignature: public Signature{
-public:
- ValuedSignature(uint id);
- int getValue();
- void setValue(int v){value = v;}
-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
+++ /dev/null
-#include "signatureenc.h"
-#include "element.h"
-#include "set.h"
-#include "signature.h"
-#include "alloyenc.h"
-#include "math.h"
-
-SignatureEnc::SignatureEnc(AlloyEnc *ae):
- alloyEncoder(ae),
- maxValue(0)
-{
-}
-
-SignatureEnc::~SignatureEnc(){
- for(uint i=0; i<signatures.getSize(); i++){
- Signature *s = signatures.get(i);
- delete s;
- }
-}
-
-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){
- maxValue = set->getElement(i);
- }
- }
-}
-
-BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
- BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar);
- if(bsig == NULL){
- bsig = new BooleanSig(getUniqueSigID());
- encoded.put(bvar, bsig);
- signatures.push(bsig);
- alloyEncoder->writeToFile(bsig->getSignature());
- }
- return bsig;
-}
-
-ElementSig *SignatureEnc::getElementSignature(Element *element){
- ElementSig *esig = (ElementSig *)encoded.get((void *)element);
- if(esig == NULL){
- Set *set = element->getRange();
- SetSig *ssig = (SetSig *)encoded.get((void *)set);
- if(ssig == NULL){
- ssig = new SetSig(getUniqueSigID(), set);
- encoded.put(set, ssig);
- signatures.push(ssig);
- alloyEncoder->writeToFile(ssig->getSignature());
- updateMaxValue(set);
- }
- esig = new ElementSig(getUniqueSigID(), ssig);
- encoded.put(element, esig);
- signatures.push(esig);
- alloyEncoder->writeToFile(esig->getSignature());
-
- }
- return esig;
-}
-
-void SignatureEnc::setValue(uint id, uint value){
- ValuedSignature *sig = getValuedSignature(id);
- ASSERT(sig != NULL);
- sig->setValue(value);
-}
-
-int SignatureEnc::getValue(void *astnode){
- ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
- ASSERT(sig != NULL);
- return sig->getValue();
-}
+++ /dev/null
-#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, uint value);
- ElementSig *getElementSignature(Element *element);
- BooleanSig *getBooleanSignature(Boolean *bvar);
- int getAlloyIntScope();
- int getValue(void *astnode);
-private:
- ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
- uint getUniqueSigID(){return signatures.getSize() +1;}
- void updateMaxValue(Set *set);
- CloneMap encoded;
- Vector<Signature*> signatures;
- AlloyEnc *alloyEncoder;
- uint64_t maxValue;
-};
-#endif
--- /dev/null
+#include "alloyenc.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "signature.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+#include "cppvector.h"
+
+using namespace std;
+
+#define alloyFileName "satune.als"
+#define solutionFile "solution.sol"
+
+AlloyEnc::AlloyEnc(CSolver *_solver):
+ Interpreter(_solver)
+{
+ 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::dumpAllConstraints(Vector<char *> &facts){
+ output << "fact {" << endl;
+ for(uint i=0; i< facts.getSize(); i++){
+ char *cstr = facts.get(i);
+ writeToFile(cstr);
+ }
+ output << "}" << endl;
+}
+
+
+int AlloyEnc::getResult(){
+ ifstream input(solutionFile, ios::in);
+ string line;
+ while(getline(input, line)){
+ if(line.find("Unsatisfiable.")== 0){
+ return IS_UNSAT;
+ }
+ if(line.find("univ") == 0){
+ continue;
+ }
+ if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
+ const char delim [2] = ",";
+ char cline [line.size()+1];
+ 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);
+ sigEnc.setValue(i1, i3);
+ }
+ token = strtok(NULL, delim);
+ }
+ }
+ }
+ return IS_SAT;
+}
+
+void AlloyEnc::dumpFooter(){
+ output << "pred show {}" << endl;
+ output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
+}
+
+void AlloyEnc::dumpHeader(){
+ output << "open util/integer" << endl;
+}
+
+void AlloyEnc::compileRunCommand(char * command, size_t size){
+ snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), alloyFileName, solutionFile);
+}
+
+string AlloyEnc::negateConstraint(string constr){
+ return "not ( " + constr + " )";
+}
+
+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));
+ 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_IFF:
+ op = " iff ";
+ break;
+ case SATC_IMPLIES:
+ op = " implies ";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
+ }
+ switch (bl->op) {
+ case SATC_OR:
+ case SATC_AND:{
+ ASSERT(size >= 2);
+ string res = "( ";
+ res += array[0];
+ for( uint i=1; i< size; i++){
+ res += op + array[i];
+ }
+ res += " )";
+ return res;
+ }
+ case SATC_NOT:{
+ return "not ( " + array[0] + " )";
+ }
+ case SATC_IMPLIES:
+ case SATC_IFF:
+ return "( " + array[0] + op + array[1] + " )";
+ case SATC_XOR:
+ default:
+ ASSERT(0);
+
+ }
+}
+
+string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
+ BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
+ return *boolSig + " = 1";
+}
+
+string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
+ FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
+ uint numDomains = elemFunc->inputs.getSize();
+ ASSERT(numDomains > 1);
+ ElementSig *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 = ".add";
+ break;
+ case SATC_SUB:
+ op = ".sub";
+ break;
+ default:
+ ASSERT(0);
+ }
+ result += *signature + " = " + *inputs[0];
+ for (uint i = 1; i < numDomains; i++) {
+ result += op + "["+ *inputs[i] +"]";
+ }
+ result += "\n";
+ return result;
+}
+
+string AlloyEnc::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *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 ALLOYENC_H
+#define ALLOYENC_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "interpreter.h"
+#include <iostream>
+#include <fstream>
+
+class AlloyEnc: public Interpreter{
+public:
+ AlloyEnc(CSolver *solver);
+ virtual ~AlloyEnc();
+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);
+ string encodeOperatorPredicate(BooleanPredicate *constraint);
+ virtual string processElementFunction(ElementFunction *element, ElementSig *signature);
+ virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2);
+};
+
+#endif
--- /dev/null
+#include "interpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "signature.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+
+using namespace std;
+
+Interpreter::Interpreter(CSolver *_solver):
+ csolver(_solver),
+ sigEnc(this)
+{
+}
+
+Interpreter::~Interpreter(){
+}
+
+void Interpreter::encode(){
+ dumpHeader();
+ SetIteratorBooleanEdge *iterator = csolver->getConstraints();
+ Vector<char *> facts;
+ while(iterator->hasNext()){
+ BooleanEdge constraint = iterator->next();
+ string constr = encodeConstraint(constraint);
+ char *cstr = new char [constr.length()+1];
+ strcpy (cstr, constr.c_str());
+ facts.push(cstr);
+ }
+ dumpAllConstraints(facts);
+ for(uint i=0; i< facts.getSize(); i++){
+ char *cstr = facts.get(i);
+ delete[] cstr;
+ }
+ delete iterator;
+}
+
+uint Interpreter::getTimeout(){
+ uint timeout =csolver->getSatSolverTimeout();
+ return timeout == (uint)NOTIMEOUT? 1000: timeout;
+}
+
+int Interpreter::solve(){
+ dumpFooter();
+ int result = IS_INDETER;
+ char buffer [512];
+ if( output.is_open()){
+ output.close();
+ }
+ compileRunCommand(buffer, sizeof(buffer));
+ int status = system(buffer);
+ if (status == 0) {
+ //Read data in from results file
+ result = getResult();
+ }
+ return result;
+}
+
+string Interpreter::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;
+ }
+ case BOOLEANVAR:{
+ res = encodeBooleanVar( (BooleanVar *) constraint);
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+ if(c.isNegated()){
+ return negateConstraint(res);
+ }
+ return res;
+}
+
+string Interpreter::encodePredicate( BooleanPredicate *bp){
+ switch (bp->predicate->type) {
+ case TABLEPRED:
+ ASSERT(0);
+ case OPERATORPRED:
+ return encodeOperatorPredicate(bp);
+ default:
+ ASSERT(0);
+ }
+}
+
+string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
+ PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
+ ASSERT(constraint->inputs.getSize() == 2);
+ string str;
+ Element *elem0 = constraint->inputs.get(0);
+ ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
+ ElementSig *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);
+ if(elem1->type == ELEMFUNCRETURN){
+ str += processElementFunction((ElementFunction *) elem1, elemSig2);
+ }
+ str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
+ return str;
+}
+
+void Interpreter::writeToFile(string str){
+ output << str << endl;
+}
+
+bool Interpreter::getBooleanValue(Boolean *b){
+ return (bool)sigEnc.getValue(b);
+}
+
+uint64_t Interpreter::getValue(Element * element){
+ return (uint64_t)sigEnc.getValue(element);
+}
+
--- /dev/null
+#ifndef INTERPRETER_H
+#define INTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include <iostream>
+#include <fstream>
+using namespace std;
+
+class Interpreter{
+public:
+ Interpreter(CSolver *solver);
+ void encode();
+ int solve();
+ void writeToFile(string str);
+ uint64_t getValue(Element *element);
+ bool getBooleanValue(Boolean *element);
+ virtual ~Interpreter();
+protected:
+ virtual void dumpFooter() = 0;
+ virtual void dumpHeader() = 0;
+ uint getTimeout();
+ virtual void compileRunCommand(char * command, size_t size) = 0;
+ string encodeConstraint(BooleanEdge constraint);
+ virtual int getResult() = 0;
+ virtual string negateConstraint(string constr) = 0;
+ virtual void dumpAllConstraints(Vector<char *> &facts) = 0;
+ virtual string encodeBooleanLogic( BooleanLogic *bl) = 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;
+ CSolver *csolver;
+ SignatureEnc sigEnc;
+ ofstream output;
+};
+
+#endif
--- /dev/null
+#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)
+{
+}
+
+int ValuedSignature::getValue(){
+ ASSERT(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;
+}
+
+string operator+(const string& str, const Signature& sig){
+ return str + sig.toString();
+}
--- /dev/null
+#ifndef ELEMENTSIG_H
+#define ELEMENTSIG_H
+#include <string>
+#include <iostream>
+#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 getAbsSignature() const =0;
+ virtual string getSignature() const =0;
+ virtual ~Signature(){}
+protected:
+ uint id;
+};
+
+class ValuedSignature: public Signature{
+public:
+ ValuedSignature(uint id);
+ int getValue();
+ void setValue(int v){value = v;}
+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
--- /dev/null
+#include "signatureenc.h"
+#include "element.h"
+#include "set.h"
+#include "signature.h"
+#include "alloyenc.h"
+#include "math.h"
+
+SignatureEnc::SignatureEnc(Interpreter *inter):
+ interpreter(inter),
+ maxValue(0)
+{
+}
+
+SignatureEnc::~SignatureEnc(){
+ for(uint i=0; i<signatures.getSize(); i++){
+ Signature *s = signatures.get(i);
+ delete s;
+ }
+}
+
+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){
+ maxValue = set->getElement(i);
+ }
+ }
+}
+
+BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
+ BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar);
+ if(bsig == NULL){
+ bsig = new BooleanSig(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);
+ if(esig == NULL){
+ Set *set = element->getRange();
+ SetSig *ssig = (SetSig *)encoded.get((void *)set);
+ if(ssig == NULL){
+ ssig = new SetSig(getUniqueSigID(), set);
+ encoded.put(set, ssig);
+ signatures.push(ssig);
+ interpreter->writeToFile(ssig->getSignature());
+ updateMaxValue(set);
+ }
+ esig = new ElementSig(getUniqueSigID(), ssig);
+ encoded.put(element, esig);
+ signatures.push(esig);
+ interpreter->writeToFile(esig->getSignature());
+
+ }
+ return esig;
+}
+
+void SignatureEnc::setValue(uint id, uint value){
+ ValuedSignature *sig = getValuedSignature(id);
+ ASSERT(sig != NULL);
+ sig->setValue(value);
+}
+
+int SignatureEnc::getValue(void *astnode){
+ ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
+ ASSERT(sig != NULL);
+ return sig->getValue();
+}
--- /dev/null
+#ifndef SIGNATUREENC_H
+#define SIGNATUREENC_H
+
+#include "classlist.h"
+#include "structs.h"
+#include "cppvector.h"
+
+class SignatureEnc {
+public:
+ SignatureEnc(Interpreter *_alloyEncoder);
+ ~SignatureEnc();
+ void setValue(uint id, uint value);
+ ElementSig *getElementSignature(Element *element);
+ BooleanSig *getBooleanSignature(Boolean *bvar);
+ int getAlloyIntScope();
+ int getValue(void *astnode);
+private:
+ ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
+ uint getUniqueSigID(){return signatures.getSize() +1;}
+ void updateMaxValue(Set *set);
+ CloneMap encoded;
+ Vector<Signature*> signatures;
+ Interpreter *interpreter;
+ uint64_t maxValue;
+};
+#endif
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) $(wildcard AlloyEnc/*.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 Interpreter/*.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) $(wildcard AlloyEnc/*.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 Interpreter/*.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) $(wildcard AlloyEnc/*.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 Interpreter/*.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 -IAlloyEnc
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IInterpreter
LDFLAGS := -ldl -lrt -rdynamic -g
SHARED := -shared
${MKDIR_P} ${OBJ_DIR}/Backend
${MKDIR_P} ${OBJ_DIR}/Encoders
${MKDIR_P} ${OBJ_DIR}/Serialize
- ${MKDIR_P} ${OBJ_DIR}/AlloyEnc
+ ${MKDIR_P} ${OBJ_DIR}/Interpreter
debug: CFLAGS += -DCONFIG_DEBUG
debug: all
class BooleanLogic;
class Serializer;
class ElementFunction;
-class AlloyEnc;
+class Interpreter;
typedef uint64_t VarType;
typedef unsigned int uint;
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
- alloyEncoder(NULL)
+ interpreter(NULL)
{
satEncoder = new SATEncoder(this);
}
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
}
+
+ if(interpreter != NULL){
+ delete interpreter;
+ }
delete boolTrue.getBoolean();
delete satEncoder;
}
int result = IS_INDETER;
if(useAlloyCompiler()){
- alloyEncoder->encode();
+ interpreter->encode();
model_print("Problem encoded in Alloy\n");
- result = alloyEncoder->solve();
+ result = interpreter->solve();
model_print("Problem solved by Alloy\n");
} else{
}
void CSolver::setAlloyEncoder(){
- if(alloyEncoder == NULL){
- alloyEncoder = new AlloyEnc(this);
+ if(interpreter == NULL){
+ interpreter = new AlloyEnc(this);
}
}
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return useAlloyCompiler()? alloyEncoder->getValue(element):
+ return useAlloyCompiler()? interpreter->getValue(element):
getElementValueSATTranslator(this, element);
default:
ASSERT(0);
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
- return useAlloyCompiler()? alloyEncoder->getBooleanValue(boolean):
+ return useAlloyCompiler()? interpreter->getBooleanValue(boolean):
getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);
void inferFixedOrders();
void inferFixedOrder(Order *order);
void setAlloyEncoder();
- bool useAlloyCompiler() {return alloyEncoder != NULL;}
+ bool useAlloyCompiler() {return interpreter != NULL;}
void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
- AlloyEnc *alloyEncoder;
+ Interpreter *interpreter;
friend class ElementOpt;
friend class VarOrderingOpt;
};
projects / satune.git / commitdiff