From 3896ad686a910868d7bf2988cd83a4fe3da700b2 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 23 Jan 2019 13:10:26 -0800 Subject: [PATCH] Adding Support for BooleanVar --- src/AlloyEnc/alloyenc.cc | 19 ++++++++++++++++- src/AlloyEnc/alloyenc.h | 4 +++- src/AlloyEnc/signature.cc | 36 +++++++++++++++++++++++++++++++- src/AlloyEnc/signature.h | 13 ++++++++++++ src/AlloyEnc/signatureenc.cc | 13 ++++++++++-- src/AlloyEnc/signatureenc.h | 1 + src/Test/deserializealloytest.cc | 2 +- src/ccsolver.cc | 4 ++-- src/ccsolver.h | 2 +- src/classlist.h | 1 + src/csolver.cc | 9 ++++---- src/csolver.h | 4 ++-- src/pycsolver.py | 4 ++-- 13 files changed, 95 insertions(+), 17 deletions(-) diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc index 033985a..9951644 100644 --- 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 dd93eb0..7864b84 100644 --- 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 62c1c1a..4237fd6 100644 --- 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 6dcb2e9..107002a 100644 --- 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 f0ed880..6971a5e 100644 --- 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 7648195..f1756df 100644 --- 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 2d6cc25..d607621 100644 --- 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 69d002e..e5958ed 100644 --- 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 b4a803a..2051cc9 100644 --- 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 3986a30..55ead29 100644 --- 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 a8eb999..5b0d073 100644 --- 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 0dc3cef..e972b7c 100644 --- 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 da911db..7c3440e 100644 --- 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 -- 2.34.1