Adding Support for BooleanVar
authorHamed Gorjiara <hgorjiar@uci.edu>
Wed, 23 Jan 2019 21:10:26 +0000 (13:10 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Wed, 23 Jan 2019 21:10:26 +0000 (13:10 -0800)
13 files changed:
src/AlloyEnc/alloyenc.cc
src/AlloyEnc/alloyenc.h
src/AlloyEnc/signature.cc
src/AlloyEnc/signature.h
src/AlloyEnc/signatureenc.cc
src/AlloyEnc/signatureenc.h
src/Test/deserializealloytest.cc
src/ccsolver.cc
src/ccsolver.h
src/classlist.h
src/csolver.cc
src/csolver.h
src/pycsolver.py

index 033985a..9951644 100644 (file)
@@ -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
index dd93eb0..7864b84 100644 (file)
@@ -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;
index 62c1c1a..4237fd6 100644 (file)
@@ -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{
index 6dcb2e9..107002a 100644 (file)
@@ -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);
index f0ed880..6971a5e 100644 (file)
@@ -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());
index 7648195..f1756df 100644 (file)
@@ -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:
index 2d6cc25..d607621 100644 (file)
@@ -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]);
index 69d002e..e5958ed 100644 (file)
@@ -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) {
index b4a803a..2051cc9 100644 (file)
@@ -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
 }
index 3986a30..55ead29 100644 (file)
@@ -76,6 +76,7 @@ class SignatureEnc;
 class Signature;
 class ElementSig;
 class SetSig;
+class BooleanSig;
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
index a8eb999..5b0d073 100644 (file)
@@ -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);
        }
index 0dc3cef..e972b7c 100644 (file)
@@ -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();
index da911db..7c3440e 100644 (file)
@@ -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