From 356f40eb6a306c5924bf465a5cfc6a4e649a2921 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 12 Sep 2018 11:27:57 -0700 Subject: [PATCH] Bug fix for the tuner: missing mustHaveValue constraints --- src/AST/element.cc | 12 ++++++++-- src/AST/element.h | 1 + src/Backend/satelemencoder.cc | 6 ++--- src/Encoders/elementencoding.cc | 1 - src/Encoders/elementencoding.h | 1 - src/Serialize/deserializer.cc | 18 ++++++++++++--- src/csolver.cc | 40 ++++++++++++++++----------------- 7 files changed, 49 insertions(+), 30 deletions(-) diff --git a/src/AST/element.cc b/src/AST/element.cc index 9642d9c..d807231 100644 --- 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 ac1ed2f..a7217b5 100644 --- 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 6062591..ad0722b 100644 --- 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 6cb3993..02d4898 100644 --- 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 3fda704..ac6e6bf 100644 --- 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 42b565e..2c4d7bb 100644 --- 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 fb35103..b7c9aa4 100644 --- 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; -- 2.34.1