Adding a new abstraction for elements: must have value
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 8 May 2018 17:56:09 +0000 (10:56 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 8 May 2018 17:56:09 +0000 (10:56 -0700)
src/Backend/satelemencoder.cc
src/Backend/satencoder.h
src/Encoders/elementencoding.cc
src/Encoders/elementencoding.h
src/Test/anyvaluetest.cc [new file with mode: 0644]
src/ccsolver.cc
src/ccsolver.h
src/csolver.cc
src/csolver.h

index 1fc1bb4..fbf09e6 100644 (file)
@@ -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));
+}
+
index 2217777..115bc31 100644 (file)
@@ -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;
index 02d4898..6cb3993 100644 (file)
@@ -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),
index 346d735..d153793 100644 (file)
@@ -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 (file)
index 0000000..84e9ad6
--- /dev/null
@@ -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;
+}
index 823b2f2..f6b73b0 100644 (file)
@@ -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);
+}
index d47e5ae..d8e3921 100644 (file)
@@ -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
index 2a440ac..7c13eae 100644 (file)
@@ -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;
                }
index b84d324..fa2ee14 100644 (file)
@@ -57,6 +57,8 @@ public:
 
        Set *getElementRange (Element *element);
 
+        void mustHaveValue(Element *element);
+        
        BooleanEdge getBooleanTrue();
 
        BooleanEdge getBooleanFalse();