Adding a new abstraction for elements: must have value

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 1fc1bb4e1dce563c7b7e1bd9529db5bef528cc23..fbf09e620a097b0573d101ac30412f70f3ce8bf7 100644 (file)
--- 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 22177772542ae6f5c3100862ec356f071339eb2f..115bc319556c3dced152ff0718d9bbbd572d4583 100644 (file)
--- 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 02d4898e3515959b969e869494ff2f4d23a27aa8..6cb399346a9a14765ba7e318811c722dbedecf0d 100644 (file)
--- 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 346d735718baf487bd31c40b5962b335f0a1f4be..d153793fc8d557dfb6ff828610305d23f73b8be2 100644 (file)
--- 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 (file)
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 823b2f20ac33cb0ed23cd667c2169c627776c847..f6b73b0ee21a7082ed51010cd0465bd77e554f22 100644 (file)
--- 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 d47e5ae29710223ef9063b58c818c10557424c9f..d8e392150ec0cb06dd3b07f3ad5c350eef74f8e1 100644 (file)
--- 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 2a440ac3c4689b547662bb839ceebf2a02b133ce..7c13eae9c8bebe007000abf801f735522dd36d67 100644 (file)
--- 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 b84d3245801d801e1524876841d9d378c26e4f81..fa2ee1426fad6288162bc880ef7c1fdd72dd03d5 100644 (file)
--- 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();