Adding support for ElementFunction

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 9951644d0b80605216fcce1b6c51c12208e6c8f8..35ecd45ca50366ee232f690fb24430c298a7d403 100644 (file)
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -8,6 +8,7 @@
 #include "element.h"
 #include "signature.h"
 #include "set.h"
+#include "function.h"
 #include <fstream>
 #include <regex>
 
@@ -34,6 +35,7 @@ AlloyEnc::~AlloyEnc(){
 }
 
 void AlloyEnc::encode(){
+       dumpAlloyHeader();
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        Vector<char *> facts;
        while(iterator->hasNext()){
@@ -75,13 +77,17 @@ int AlloyEnc::getResult(){
        return IS_SAT;
 }
 
-void AlloyEnc::dumpAlloyIntScope(){
+void AlloyEnc::dumpAlloyFooter(){
        output << "pred show {}" << endl;
        output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
 }
 
+void AlloyEnc::dumpAlloyHeader(){
+       output << "open util/integer" << endl;
+}
+
 int AlloyEnc::solve(){
-       dumpAlloyIntScope();
+       dumpAlloyFooter();
        int result = IS_INDETER;
        char buffer [512];
        if( output.is_open()){
@@ -166,26 +172,69 @@ string AlloyEnc::encodeBooleanVar( BooleanVar *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){
+       constraint->print();
        PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
        ASSERT(constraint->inputs.getSize() == 2);
+       string str;
        Element *elem0 = constraint->inputs.get(0);
-       ASSERT(elem0->type = ELEMSET);
+       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);
+       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:
-                       return *elemSig1 + " = " + *elemSig2;
+                       str += *elemSig1 + " = " + *elemSig2;
+                       break;
                case SATC_LT:
-                       return *elemSig1 + " < " + *elemSig2;
+                       str += *elemSig1 + " < " + *elemSig2;
+                       break;
                case SATC_GT:
-                       return *elemSig1 + " > " + *elemSig2; 
+                       str += *elemSig1 + " > " + *elemSig2;
+                       break; 
                default:
                        ASSERT(0);
        }
-       exit(-1);
+       return str;
 }
 
 void AlloyEnc::writeToFile(string str){

diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h
index 7864b846ca2f242252f902d3567afed313a872c8..97049e2fefdbb60e733287d5eca0a3a4f80fde32 100644 (file)
--- a/src/AlloyEnc/alloyenc.h
+++ b/src/AlloyEnc/alloyenc.h
@@ -17,13 +17,15 @@ public:
        bool getBooleanValue(Boolean *element);
        ~AlloyEnc();
 private:
-       void dumpAlloyIntScope();
+       void dumpAlloyFooter();
+       void dumpAlloyHeader();
        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;

diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 4237fd6e25e042a976986013141a7dbdf657ec18..4b898d8230d66347a13c66f3197fc26fd6630706 100644 (file)
--- a/src/AlloyEnc/signature.cc
+++ b/src/AlloyEnc/signature.cc
@@ -1,7 +1,7 @@
 #include "signature.h"
 #include "set.h"
 
-bool BooleanSig::encodeSet = true;
+bool BooleanSig::encodeAbsSig = true;
 
 BooleanSig::BooleanSig(uint id):
        Signature(id),
@@ -20,8 +20,8 @@ string BooleanSig::toString() const{
 
 string BooleanSig::getSignature() const{
        string str;
-       if(encodeSet){
-               encodeSet = false;
+       if(encodeAbsSig){
+               encodeAbsSig = false;
                str += "one sig BooleanSet {\n\
                domain: set Int\n\
                }{\n\

diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h
index 107002ac021b6d4e7b82feb399ca950e39c1af3c..b3ebf47b84bbfba798b394e865fc7ca9301b7149 100644 (file)
--- a/src/AlloyEnc/signature.h
+++ b/src/AlloyEnc/signature.h
@@ -26,7 +26,7 @@ public:
        virtual string getSignature() const;
 private:
        int value;
-       static bool encodeSet;
+       static bool encodeAbsSig;
 };
 
 class SetSig: public Signature{