From 9ef6c2bc13c8474fa7848e06f312cdcd05254b6b Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Tue, 8 May 2018 10:56:09 -0700 Subject: [PATCH] Adding a new abstraction for elements: must have value --- src/Backend/satelemencoder.cc | 80 +++++++++++++++++++++++++++++++++ src/Backend/satencoder.h | 5 ++- src/Encoders/elementencoding.cc | 1 + src/Encoders/elementencoding.h | 1 + src/Test/anyvaluetest.cc | 27 +++++++++++ src/ccsolver.cc | 5 +++ src/ccsolver.h | 1 + src/csolver.cc | 14 ++++-- src/csolver.h | 2 + 9 files changed, 131 insertions(+), 5 deletions(-) create mode 100644 src/Test/anyvaluetest.cc diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 1fc1bb4..fbf09e6 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -214,12 +214,16 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) { ASSERT(encoding->type == BINARYVAL); allocElementConstraintVariables(encoding, encoding->numBits); getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables); + if(encoding->anyValue) + generateAnyValueBinaryValueEncoding(encoding); } void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) { ASSERT(encoding->type == BINARYINDEX); allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1)); getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables); + if(encoding->anyValue) + generateAnyValueBinaryIndexEncoding(encoding); } void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) { @@ -231,6 +235,8 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) { } } addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables)); + if(encoding->anyValue) + generateAnyValueOneHotEncoding(encoding); } void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) { @@ -240,6 +246,8 @@ void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) { for (uint i = 1; i < encoding->numVars; i++) { addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i]))); } + if(encoding->anyValue) + generateAnyValueUnaryEncoding(encoding); } void SATEncoder::generateElementEncoding(Element *element) { @@ -265,3 +273,75 @@ void SATEncoder::generateElementEncoding(Element *element) { } } +void SATEncoder::generateAnyValueOneHotEncoding(ElementEncoding *encoding){ + if(encoding->numVars == 0) + return; + Edge carray[encoding->numVars]; + int size = 0; + for (uint i = 0; i < encoding->encArraySize; i++) { + if (encoding->isinUseElement(i)){ + carray[size++] = encoding->variables[i]; + } + } + if(size > 0){ + addConstraintCNF(cnf, constraintOR(cnf, size, carray)); + } +} + +void SATEncoder::generateAnyValueUnaryEncoding(ElementEncoding *encoding){ + if (encoding->numVars == 0) + return; + Edge carray[encoding->numVars]; + int size = 0; + for (uint i = 0; i < encoding->encArraySize; i++) { + if (encoding->isinUseElement(i)) { + if (i == 0) + carray[size++] = constraintNegate(encoding->variables[0]); + else if ((i + 1) == encoding->encArraySize) + carray[size++] = encoding->variables[i - 1]; + else + carray[size++] = constraintAND2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])); + } + } + if(size > 0){ + addConstraintCNF(cnf, constraintOR(cnf, size, carray)); + } +} + +void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){ + if(encoding->numVars == 0) + return; + Edge carray[encoding->numVars]; + int size = 0; + int index = -1; + for(uint i= encoding->encArraySize-1; i>=0; i--){ + if(encoding->isinUseElement(i)){ + if(i+1 < encoding->encArraySize){ + index = i+1; + } + break; + } + } + if( index != -1 ){ + carray[size++] = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index); + } + index = index == -1? encoding->encArraySize-1 : index-1; + for(int i= index; i>=0; i--){ + if (!encoding->isinUseElement(i)){ + carray[size++] = constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)); + } + } + if(size > 0){ + addConstraintCNF(cnf, constraintAND(cnf, size, carray)); + } +} + +void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){ + uint64_t minvalueminusoffset = encoding->low - encoding->offset; + uint64_t maxvalueminusoffset = encoding->high - encoding->offset; + model_print("This is minvalueminus offset: %lu", minvalueminusoffset); + Edge lowerbound = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, maxvalueminusoffset); + Edge upperbound = constraintNegate(generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, minvalueminusoffset)); + addConstraintCNF(cnf, constraintAND2(cnf, lowerbound, upperbound)); +} + diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 2217777..115bc31 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -61,7 +61,10 @@ private: Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint); void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This); void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This); - + void generateAnyValueOneHotEncoding(ElementEncoding *encoding); + void generateAnyValueUnaryEncoding(ElementEncoding *encoding); + void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding); + void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding); CNF *cnf; CSolver *solver; BooleanToEdgeMap booledgeMap; diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc index 02d4898..6cb3993 100644 --- a/src/Encoders/elementencoding.cc +++ b/src/Encoders/elementencoding.cc @@ -8,6 +8,7 @@ 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 346d735..d153793 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -33,6 +33,7 @@ public: } void print(); + bool anyValue; ElementEncodingType type; Element *element; Edge *variables;/* List Variables Used To Encode Element */ diff --git a/src/Test/anyvaluetest.cc b/src/Test/anyvaluetest.cc new file mode 100644 index 0000000..84e9ad6 --- /dev/null +++ b/src/Test/anyvaluetest.cc @@ -0,0 +1,27 @@ +#include "csolver.h" + + +int main(int numargs, char **argv) { + CSolver *solver = new CSolver(); + uint64_t set1[] = {10, 8, 18}; + uint64_t set2[] = {10, 13, 7}; + Set *s1 = solver->createSet(0, set1, 3); + Set *s2 = solver->createSet(1, set2, 3); + Element *e1 = solver->getElementVar(s1); + Element *e2 = solver->getElementVar(s2); + solver->mustHaveValue(e1); + solver->mustHaveValue(e2); + + Set *domain[] = {s1, s2}; + Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2); + Element *inputs[] = {e1, e2}; + BooleanEdge b = solver->applyPredicate(equals, inputs, 2); + b = solver->applyLogicalOperation(SATC_NOT, b); + solver->addConstraint(b); + + if (solver->solve() == 1) + printf("e1=%" PRIu64 "e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2)); + else + printf("UNSAT\n"); + delete solver; +} diff --git a/src/ccsolver.cc b/src/ccsolver.cc index 823b2f2..f6b73b0 100644 --- a/src/ccsolver.cc +++ b/src/ccsolver.cc @@ -139,3 +139,8 @@ void printConstraints(void* solver){ void serialize(void* solver){ CCSOLVER(solver)->serialize(); } + + +void mustHaveValue(void *solver, void *element){ + CCSOLVER(solver)->mustHaveValue( (Element*) element); +} diff --git a/src/ccsolver.h b/src/ccsolver.h index d47e5ae..d8e3921 100644 --- a/src/ccsolver.h +++ b/src/ccsolver.h @@ -40,6 +40,7 @@ int getBooleanValue(void* solver,void* boolean); int getOrderConstraintValue(void* solver,void *order, long first, long second); void printConstraints(void* solver); void serialize(void* solver); +void mustHaveValue(void *solver, void *element); #ifdef __cplusplus } #endif diff --git a/src/csolver.cc b/src/csolver.cc index 2a440ac..7c13eae 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -222,6 +222,10 @@ Element *CSolver::getElementVar(Set *set) { return element; } +void CSolver::mustHaveValue(Element *element){ + element->getElementEncoding()->anyValue = true; +} + Set *CSolver::getElementRange (Element *element) { return element->getRange(); } @@ -347,9 +351,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) { return applyLogicalOperation(op, array, 1); } -static int ptrcompares(const void *p1, const void *p2) { - uintptr_t b1 = *(uintptr_t const *) p1; - uintptr_t b2 = *(uintptr_t const *) p2; +static int booleanEdgeCompares(const void *p1, const void *p2) { + BooleanEdge be1 = *(BooleanEdge const *) p1; + BooleanEdge be2 = *(BooleanEdge const *) p2; + uint64_t b1 = be1->id; + uint64_t b2 = be2->id; if (b1 < b2) return -1; else if (b1 == b2) @@ -421,7 +427,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } else if (newindex == 1) { return newarray[0]; } else { - bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares); + bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares); array = newarray; asize = newindex; } diff --git a/src/csolver.h b/src/csolver.h index b84d324..fa2ee14 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -57,6 +57,8 @@ public: Set *getElementRange (Element *element); + void mustHaveValue(Element *element); + BooleanEdge getBooleanTrue(); BooleanEdge getBooleanFalse(); -- 2.34.1