Bug fix for the tuner: missing mustHaveValue constraints

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 9642d9cedaf0e3050c816dbb73f957a64101f755..d8072315ca3a04e8f44a7fe0ee78ddc6aa852716 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -8,7 +8,8 @@
 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
-       encoding(this) {
+       encoding(this),
+       anyValue(false){
 }
 
 ElementSet::ElementSet(Set *s) :
@@ -35,7 +36,9 @@ ElementConst::ElementConst(uint64_t _value, Set *_set) :
 }
 
 Element *ElementConst::clone(CSolver *solver, CloneMap *map) {
-       return solver->getElementConst(type, value);
+       Element* e= solver->getElementConst(type, value);
+       e->anyValue = anyValue;
+       return e;
 }
 
 Element *ElementSet::clone(CSolver *solver, CloneMap *map) {
@@ -44,6 +47,7 @@ Element *ElementSet::clone(CSolver *solver, CloneMap *map) {
                return e;
        e = solver->getElementVar(set->clone(solver, map));
        map->put(this, e);
+       e->anyValue = anyValue;
        return e;
 }
 
@@ -54,6 +58,7 @@ Element *ElementFunction::clone(CSolver *solver, CloneMap *map) {
        }
        BooleanEdge ofstatus = overflowstatus ? cloneEdge(solver, map, overflowstatus) : BooleanEdge();
        Element *e = solver->applyFunction(function->clone(solver, map), array, inputs.getSize(), ofstatus);
+       e->anyValue = anyValue;
        return e;
 }
 
@@ -75,6 +80,7 @@ void ElementSet::serialize(Serializer *serializer) {
        set->serialize(serializer);
 
        serializer->mywrite(&type, sizeof(ASTNodeType));
+       serializer->mywrite(&anyValue, sizeof(bool));
        ElementSet *This = this;
        serializer->mywrite(&This, sizeof(ElementSet *));
        serializer->mywrite(&set, sizeof(Set *));
@@ -96,6 +102,7 @@ void ElementConst::serialize(Serializer *serializer) {
        set->serialize(serializer);
 
        serializer->mywrite(&type, sizeof(ASTNodeType));
+       serializer->mywrite(&anyValue, sizeof(bool));
        ElementSet *This = this;
        serializer->mywrite(&This, sizeof(ElementSet *));
        VarType type = set->getType();
@@ -121,6 +128,7 @@ void ElementFunction::serialize(Serializer *serializer) {
        serializeBooleanEdge(serializer, overflowstatus);
 
        serializer->mywrite(&type, sizeof(ASTNodeType));
+       serializer->mywrite(&anyValue, sizeof(bool));
        ElementFunction *This = this;
        serializer->mywrite(&This, sizeof(ElementFunction *));
        serializer->mywrite(&function, sizeof(Function *));

diff --git a/src/AST/element.h b/src/AST/element.h
index ac1ed2f63a51f11cd9932659b40fc15dab8c72b5..a7217b5a44052999119debc7cb2c0b3c3dae0e06 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -21,6 +21,7 @@ public:
        virtual void updateParents() {}
        virtual Set *getRange() = 0;
        CMEMALLOC;
+        bool anyValue;
 };
 
 class ElementSet : public Element {

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 60625917a9f8ffde48e169319103e52b262c4077..ad0722b2d262bf4a89a792fa220c2d1b8a554013 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -214,7 +214,7 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYVAL);
        allocElementConstraintVariables(encoding, encoding->numBits);
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->anyValue)
+       if (encoding->element->anyValue)
                generateAnyValueBinaryValueEncoding(encoding);
 }
 
@@ -222,7 +222,7 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->anyValue)
+       if (encoding->element->anyValue)
                generateAnyValueBinaryIndexEncoding(encoding);
 }
 
@@ -234,7 +234,7 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
                        addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }
-       if (encoding->anyValue)
+       if (encoding->element->anyValue)
                addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }
 

diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc
index 6cb399346a9a14765ba7e318811c722dbedecf0d..02d4898e3515959b969e869494ff2f4d23a27aa8 100644 (file)
--- a/src/Encoders/elementencoding.cc
+++ b/src/Encoders/elementencoding.cc
@@ -8,7 +8,6 @@
 const char *elemEncTypeNames[] = {"UNASSIGNED", "ONEHOT", "UNARY", "BINARYINDEX", "BINARYVAL"};
 
 ElementEncoding::ElementEncoding(Element *_element) :
-       anyValue(false),
        type(ELEM_UNASSIGNED),
        element(_element),
        variables(NULL),

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 3fda7040e42e75364213b08958b4d213e4f4e238..ac6e6bf5a4626903e3a12fd3e43a82214ec0779f 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -33,7 +33,6 @@ public:
        }
        void print();
 
-       bool anyValue;
        ElementEncodingType type;
        Element *element;
        Edge *variables;/* List Variables Used To Encode Element */

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 42b565e1cf962a8ea2f52bfecc2e7951cd42b603..2c4d7bb2fee5cbfb76f9fc3c1aa730408d00788f 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -315,26 +315,36 @@ void Deserializer::deserializeTable() {
 
 
 void Deserializer::deserializeElementSet() {
+       bool anyValue = false;
+       myread(&anyValue, sizeof(bool));
        ElementSet *es_ptr;
        myread(&es_ptr, sizeof(ElementSet *));
        Set *set;
        myread(&set, sizeof(Set *));
        ASSERT(map.contains(set));
        set  = (Set *) map.get(set);
-       map.put(es_ptr, solver->getElementVar(set));
+       Element *newEl = solver->getElementVar(set);
+       newEl->anyValue = anyValue;
+       map.put(es_ptr, newEl);
 }
 
 void Deserializer::deserializeElementConst() {
+       bool anyValue = false;
+       myread(&anyValue, sizeof(bool));
        ElementSet *es_ptr;
        myread(&es_ptr, sizeof(ElementSet *));
        VarType type;
        myread(&type, sizeof(VarType));
        uint64_t value;
        myread(&value, sizeof(uint64_t));
-       map.put(es_ptr, solver->getElementConst(type, value));
+       Element *newEl = solver->getElementConst(type, value);
+       newEl->anyValue = anyValue;
+       map.put(es_ptr, newEl);
 }
 
 void Deserializer::deserializeElementFunction() {
+       bool anyValue = false;
+       myread(&anyValue, sizeof(bool));
        ElementFunction *ef_ptr;
        myread(&ef_ptr, sizeof(ElementFunction *));
        Function *function;
@@ -360,7 +370,9 @@ void Deserializer::deserializeElementFunction() {
        overflowstatus = (Boolean *) map.get(tmp.getBoolean());
        BooleanEdge res(overflowstatus);
        BooleanEdge undefStatus = isNegated ? res.negate() : res;
-       map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
+       Element *newEl = solver->applyFunction(function, members.expose(), size, undefStatus);
+       newEl->anyValue = anyValue;
+       map.put(ef_ptr, newEl);
 }
 
 

diff --git a/src/csolver.cc b/src/csolver.cc
index fb351037c3ba12192db164b254db8d1f5e3f5d67..b7c9aa4fcb9f9ac6d4bab090dc1b41b2a9e0c2bd 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -224,7 +224,7 @@ Element *CSolver::getElementVar(Set *set) {
 }
 
 void CSolver::mustHaveValue(Element *element) {
-       element->getElementEncoding()->anyValue = true;
+       element->anyValue = true;
 }
 
 Set *CSolver::getElementRange (Element *element) {
@@ -577,7 +577,7 @@ void CSolver::inferFixedOrders() {
 
 #define NANOSEC 1000000000.0
 int CSolver::solve() {
-       long long starttime = getTimeNano();
+       long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
@@ -597,17 +597,17 @@ int CSolver::solve() {
                delete orderit;
        }
        computePolarities(this);
-       long long time2 = getTimeNano();
-       model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
+       long long time1 = getTimeNano();
+       model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
        Preprocess pp(this);
        pp.doTransform();
-       long long time3 = getTimeNano();
-       model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+       long long time2 = getTimeNano();
+       model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 
        DecomposeOrderTransform dot(this);
        dot.doTransform();
-       long long time4 = getTimeNano();
-       model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
+       time1 = getTimeNano();
+       model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 
        IntegerEncodingTransform iet(this);
        iet.doTransform();
@@ -615,27 +615,27 @@ int CSolver::solve() {
        ElementOpt eop(this);
        eop.doTransform();
 
-       EncodingGraph eg(this);
-       eg.buildGraph();
-       eg.encode();
+//     EncodingGraph eg(this);
+//     eg.buildGraph();
+//     eg.encode();
 
        naiveEncodingDecision(this);
 //     eg.validate();
        
-       long long time5 = getTimeNano();
-       model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
+       time2 = getTimeNano();
+       model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 
-       long long startTime = getTimeNano();
        satEncoder->encodeAllSATEncoder(this);
-       long long endTime = getTimeNano();
-
-       elapsedTime = endTime - startTime;
-       model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
+       time1 = getTimeNano();
 
+       model_print("Elapse Encode time: %f\n", (time1- startTime) / NANOSEC);
+       
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in SAT solver: %d\n", result);
-
+       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : " UNSAT");
+       time2 = getTimeNano();
+       elapsedTime = time2 - startTime;
+       model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;