Adding Support for BooleanVar

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 033985a5a576868c6a9ef31da3005531d74d7b8a..9951644d0b80605216fcce1b6c51c12208e6c8f8 100644 (file)
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -87,7 +87,7 @@ int AlloyEnc::solve(){
        if( output.is_open()){
                output.close();
        }
-       snprintf(buffer, sizeof(buffer), "./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
+       snprintf(buffer, sizeof(buffer), "./run.sh java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
        int status = system(buffer);
        if (status == 0) {
                //Read data in from results file
@@ -108,6 +108,10 @@ string AlloyEnc::encodeConstraint(BooleanEdge c){
                        res = encodePredicate((BooleanPredicate *) constraint);
                        break;
                }
+               case BOOLEANVAR:{
+                       res = encodeBooleanVar( (BooleanVar *) constraint);
+                       break;
+               }
                default:
                        ASSERT(0);
        }
@@ -157,6 +161,11 @@ string AlloyEnc::encodePredicate( BooleanPredicate *bp){
        }
 }
 
+string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
+       BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
+       return *boolSig + " = 1";
+}
+
 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
        PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
        ASSERT(constraint->inputs.getSize() == 2);
@@ -183,6 +192,14 @@ void AlloyEnc::writeToFile(string str){
        output << str << endl;
 }
 
+bool AlloyEnc::getBooleanValue(Boolean *b){
+       if (b->boolVal == BV_MUSTBETRUE)
+               return true;
+       else if (b->boolVal == BV_MUSTBEFALSE)
+               return false;
+       return sigEnc.getBooleanSignature(b);
+}
+
 uint64_t AlloyEnc::getValue(Element * element){
        ElementEncoding *elemEnc = element->getElementEncoding();
        if (elemEnc->numVars == 0)//case when the set has only one item

diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h
index dd93eb039f7d65e22f3359bfe5a90403687bce7b..7864b846ca2f242252f902d3567afed313a872c8 100644 (file)
--- a/src/AlloyEnc/alloyenc.h
+++ b/src/AlloyEnc/alloyenc.h
@@ -13,13 +13,15 @@ public:
        void encode();
        int solve();
        void writeToFile(string str);
-       uint64_t getValue(Element * element);
+       uint64_t getValue(Element *element);
+       bool getBooleanValue(Boolean *element);
        ~AlloyEnc();
 private:
        void dumpAlloyIntScope();
        string encodeConstraint(BooleanEdge constraint);
        int getResult();
        string encodeBooleanLogic( BooleanLogic *bl);
+       string encodeBooleanVar( BooleanVar *bv);
        string encodePredicate( BooleanPredicate *bp);
        string encodeOperatorPredicate(BooleanPredicate *constraint);
        CSolver *csolver;

diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 62c1c1a9972dfcc8dd657066275d43fa54b6e759..4237fd6e25e042a976986013141a7dbdf657ec18 100644 (file)
--- a/src/AlloyEnc/signature.cc
+++ b/src/AlloyEnc/signature.cc
@@ -1,12 +1,46 @@
 #include "signature.h"
 #include "set.h"
 
+bool BooleanSig::encodeSet = true;
+
+BooleanSig::BooleanSig(uint id):
+       Signature(id),
+       value(-1)
+{
+}
+
+bool BooleanSig::getValue(){
+       ASSERT(value != -1);
+       return (bool) value;
+}
+
+string BooleanSig::toString() const{
+       return "Boolean" + to_string(id) + ".value";
+}
+
+string BooleanSig::getSignature() const{
+       string str;
+       if(encodeSet){
+               encodeSet = false;
+               str += "one sig BooleanSet {\n\
+               domain: set Int\n\
+               }{\n\
+               domain = 0 + 1 \n\
+               }\n";
+       }
+       str += "one sig Boolean" + to_string(id) + " {\n\
+       value: Int\n\
+       }{\n\
+       value in BooleanSet.domain\n\
+       }";
+       return str;
+}
+
 ElementSig::ElementSig(uint id, SetSig *_ssig): 
        Signature(id),
        ssig(_ssig),
        value(0)
 {
-       
 }
 
 string ElementSig::toString() const{

diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h
index 6dcb2e9c92f9ec492141a48216e90268b7f46a65..107002ac021b6d4e7b82feb399ca950e39c1af3c 100644 (file)
--- a/src/AlloyEnc/signature.h
+++ b/src/AlloyEnc/signature.h
@@ -16,6 +16,19 @@ protected:
        uint id;
 };
 
+class BooleanSig: public Signature{
+public:
+       BooleanSig(uint id);
+       bool getValue();
+       void setValue(bool v) {value = v; }
+       virtual ~BooleanSig(){}
+       virtual string toString() const;
+       virtual string getSignature() const;
+private:
+       int value;
+       static bool encodeSet;
+};
+
 class SetSig: public Signature{
 public:
        SetSig(uint id, Set *set);

diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc
index f0ed880fb33a6c8b8836dea2b37f5f81a24016b2..6971a5edcda4978f700531735ba3d81e934d5a35 100644 (file)
--- a/src/AlloyEnc/signatureenc.cc
+++ b/src/AlloyEnc/signatureenc.cc
@@ -31,6 +31,17 @@ void SignatureEnc::updateMaxValue(Set *set){
        }
 }
 
+BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
+       BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar);
+       if(bsig == NULL){
+               bsig = new BooleanSig(signatures.getSize());
+               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){
@@ -44,8 +55,6 @@ ElementSig *SignatureEnc::getElementSignature(Element *element){
                        updateMaxValue(set);
                }
                esig = new ElementSig(signatures.getSize(), ssig);
-               element->print();
-               model_print(" = Element%u\n", signatures.getSize());
                encoded.put(element, esig);
                signatures.push(esig);
                alloyEncoder->writeToFile(esig->getSignature());

diff --git a/src/AlloyEnc/signatureenc.h b/src/AlloyEnc/signatureenc.h
index 76481954bd380bc3728c5f108b41dd3a0d690e20..f1756df7913c061b84f9936485d05b60d4b97022 100644 (file)
--- a/src/AlloyEnc/signatureenc.h
+++ b/src/AlloyEnc/signatureenc.h
@@ -11,6 +11,7 @@ public:
        ~SignatureEnc();
        void setValue(uint id, uint64_t value);
        ElementSig *getElementSignature(Element *element);
+       BooleanSig *getBooleanSignature(Boolean *bvar);
        int getAlloyIntScope();
        uint64_t getValue(Element *element);
 private:

diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
index 2d6cc25ef3040ea28ebbb163e6271a0c9fd23578..d607621358bd0d814be54fead7f15cad23ffd224 100644 (file)
--- a/src/Test/deserializealloytest.cc
+++ b/src/Test/deserializealloytest.cc
@@ -10,7 +10,7 @@ int main(int argc, char **argv) {
        }
        CSolver *solver = CSolver::deserialize(argv[1]);
        if(argc == 3)
-               solver->setAlloyEncode();
+               solver->setAlloyEncoder();
        int value = solver->solve();
        if (value == 1) {
                printf("%s is SAT\n", argv[1]);

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index 69d002ef9714433ba6ceed59cc7041fa45e92d87..e5958ed5cc89aa8ca5641d0307fd255d3dc90624 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 setAlloyEncode(void *solver){
-       CCSOLVER(solver)->setAlloyEncode();
+void setAlloyEncoder(void *solver){
+       CCSOLVER(solver)->setAlloyEncoder();
 }
 
 void *clone(void *solver) {

diff --git a/src/ccsolver.h b/src/ccsolver.h
index b4a803ae350f78d3c0b6d7c6de0931418a117e73..2051cc91b9126e2e8b8ccfbdd61c6cb9eca46df0 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -41,7 +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 setAlloyEncoder(void *solver);
 void *clone(void *solver);
 #ifdef __cplusplus
 }

diff --git a/src/classlist.h b/src/classlist.h
index 3986a3051927f4ba1204957062112539240ffd88..55ead2954e92ea34cbd6a30f4bd7f625f1748f27 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -76,6 +76,7 @@ class SignatureEnc;
 class Signature;
 class ElementSig;
 class SetSig;
+class BooleanSig;
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;

diff --git a/src/csolver.cc b/src/csolver.cc
index a8eb999de296c7b58b90af4057deb97e5f1faedb..5b0d073de4568a237861dca4a34992dea23a6a43 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -658,7 +658,7 @@ int CSolver::solve() {
        return result;
 }
 
-void CSolver::setAlloyEncode(){
+void CSolver::setAlloyEncoder(){
        alloyEncoder = new AlloyEnc(this);
 }
 
@@ -680,8 +680,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return alloyEncoder == NULL? getElementValueSATTranslator(this, element):
-                       alloyEncoder->getValue(element);
+               return useAlloyCompiler()? alloyEncoder->getValue(element):
+                       getElementValueSATTranslator(this, element);
        default:
                ASSERT(0);
        }
@@ -692,7 +692,8 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) {
        Boolean *boolean = bedge.getBoolean();
        switch (boolean->type) {
        case BOOLEANVAR:
-               return getBooleanVariableValueSATTranslator(this, boolean);
+               return useAlloyCompiler()? alloyEncoder->getBooleanValue(boolean):
+                       getBooleanVariableValueSATTranslator(this, boolean);
        default:
                ASSERT(0);
        }

diff --git a/src/csolver.h b/src/csolver.h
index 0dc3ceffe99ba68085cca2a9b7703c3eed90673a..e972b7c598471fd77adacbdd741dcbce78a92828 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -165,8 +165,8 @@ public:
        void autoTune(uint budget);
        void inferFixedOrders();
        void inferFixedOrder(Order *order);
-       void setAlloyEncode();
-
+       void setAlloyEncoder();
+       bool useAlloyCompiler() {return alloyEncoder != 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 da911dbdc801ac10b5b6fdcaa7af077eab79bbf1..7c3440e03b028eb794797b097eb9d23505e36ea7 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.setAlloyEncode.argtypes = [c_void_p]
-       csolverlb.setAlloyEncode.restype = None
+        csolverlb.setAlloyEncoder.argtypes = [c_void_p]
+       csolverlb.setAlloyEncoder.restype = None
        return csolverlb