Merge branch 'hamed' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler into...

diff --git a/.gitignore b/.gitignore
index 2d1b9f1b8d7cd96e8299ce2f07102a6b4914e384..bbff0e1594c76c80d5a8b17306af2f00528772bb 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -9,3 +9,6 @@ src/lib_cons_comp.so
 /src/mymemory.cc
 .*
 *.dSYM
+
+#Ignoring Benchmarks
+src/Benchmarks/

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index c576268058f3b5203687a2d6cef9e496a90bcf2e..647f548d352f21e5a98c149ce519b427941099bc 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -5,11 +5,13 @@
 #include "order.h"
 #include "predicate.h"
 
+uint64_t Boolean::counter = 0;
+
 Boolean::Boolean(ASTNodeType _type) :
        ASTNode(_type),
        polarity(P_UNDEFINED),
        boolVal(BV_UNDEFINED),
-       parents() {
+       parents(), id(counter++) {
 }
 
 BooleanConst::BooleanConst(bool _isTrue) :

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 1b5d24dea0b90e32f9ff7c26470cd424f332f5b1..de96bfc4e21a2ad1699132f85e3b5fb934597f1a 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -11,6 +11,8 @@
 #include "serializer.h"
 
 class Boolean : public ASTNode {
+private:
+    static uint64_t counter;
 public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
@@ -23,7 +25,7 @@ public:
        BooleanValue boolVal;
        Vector<ASTNode *> parents;
        virtual void updateParents() {}
-       
+        uint64_t id;
        CMEMALLOC;
 };
 

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 1fc1bb4e1dce563c7b7e1bd9529db5bef528cc23..b80978ec0c5a620809544b08376171d939729662 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) {
@@ -265,3 +271,55 @@ 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::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..b67708da00a749dbe0d9b9473c68d97f06f79e0a 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -61,7 +61,9 @@ private:
        Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
-
+        void generateAnyValueOneHotEncoding(ElementEncoding *encoding);
+       void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+       void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;
        CSolver *solver;
        BooleanToEdgeMap booledgeMap;

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 79b13033ebdc40f4ffd82963ac83885d936f3cdc..1fea1a58f41ebf23391bba824a6744bc84662ae8 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -190,8 +190,8 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(cnf, cor);
+       Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(cnf, cand);
        deleteVectorEdge(clauses);
 }
 

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/Test/buildsimple.cc b/src/Test/buildsimple.cc
new file mode 100644 (file)
index 0000000..f7ab9d3
--- /dev/null
+++ b/src/Test/buildsimple.cc
@@ -0,0 +1,47 @@
+#include "csolver.h"
+#include <unistd.h>
+
+/**
+ * e1={0, 1, 2}
+ * e2={0, 1, 2}
+ * e1 == e2
+ * e3= e1+e2 {0, 1, 2, 3, 4}
+ * e4 = f(e1, e2)
+ *     0 1 => 0
+ *     1 1 => 0
+ *     2 1 => 2
+ *     2 2 => 2
+ * e3 == e4
+ * Result: UNSAT!
+ */
+int main(int numargs, char **argv) {
+       CSolver *solver = new CSolver();
+       uint64_t set1[] = {1, 2, 3};
+       Set *s1 = solver->createSet(1, set1, 3);
+       Set *s2 = solver->createSet(1, set1, 3);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
+       solver->mustHaveValue(e1);
+       solver->mustHaveValue(e2);
+       Set *domain[] = {s1, s2};
+       Element *inputs[] = {e1, e2};
+
+       uint64_t set2[] = {3};
+       Set *rangef1 = solver->createSet(1, set2, 1);
+       Function *f1 = solver->createFunctionOperator(SATC_ADD, domain, 2, rangef1, SATC_FLAGIFFOVERFLOW);
+
+       BooleanEdge overflow = solver->getBooleanVar(2);
+       Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
+       Element *e4 = solver->getElementConst(5, 3);
+       Set *domain2[] = {rangef1,rangef1};
+       Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
+       Element *inputs2 [] = {e4, e3};
+       BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
+       solver->addConstraint(pred);
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, overflow));
+       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 53e1901d101624c6296d45f3824be341bc6e7b0c..c5c3b8d6fff90869b2be6338a3c0bcd3c477bfb1 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();

diff --git a/src/pycsolver.py b/src/pycsolver.py
index d78836e023e1e6188880d6187ee198d0ec978d09..3dd296b7c6c6ba0cb77a221c2026af2c8ef65fcf 100644 (file)
--- a/src/pycsolver.py
+++ b/src/pycsolver.py
@@ -15,6 +15,19 @@ class CompOp:
        SATC_LTE=3
        SATC_GTE=4
 
+class ArithOp:
+    SATC_ADD=0
+    SATC_SUB=1
+
+class OverFlowBehavior:
+    SATC_IGNORE=0
+    SATC_WRAPAROUND=1
+    SATC_FLAGFORCESOVERFLOW=2
+    SATC_OVERFLOWSETSFLAG=3
+    SATC_FLAGIFFOVERFLOW=4
+    SATC_NOOVERFLOW=5
+
+
 def loadCSolver():
         csolverlb = cdll.LoadLibrary("lib_cons_comp.so")
         csolverlb.createCCSolver.restype = c_void_p