Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index a0048bd50aebfe529dc9361f902af821a0416f59..7c3771095a2ca448eab0ab4e84dea940be384da7 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -14,7 +14,7 @@ Boolean::Boolean(ASTNodeType _type) :
 
 BooleanConst::BooleanConst(bool _isTrue) :
        Boolean(BOOLCONST),
-       isTrue(_isTrue) {
+       istrue(_isTrue) {
 }
 
 BooleanVar::BooleanVar(VarType t) :
@@ -49,7 +49,7 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a
 }
 
 Boolean *BooleanConst::clone(CSolver *solver, CloneMap *map) {
-       if (isTrue)
+       if (istrue)
                return solver->getBooleanTrue();
        else
                return solver->getBooleanFalse();

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 7dd0bb3ed2c2d38e014781bce9f1f476c75e1332..afcf512499aa40561b580bce56dc544c0af721cf 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -13,7 +13,9 @@ class Boolean : public ASTNode {
 public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
-       virtual Boolean *clone(CSolver *solver, CloneMap *map) { ASSERT(0); return NULL; }
+       virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
+       virtual bool isTrue() {return false;}
+       virtual bool isFalse() {return false;}
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;
@@ -25,7 +27,9 @@ class BooleanConst : public Boolean {
  public:
        BooleanConst(bool isTrue);
        Boolean *clone(CSolver *solver, CloneMap *map);
-       bool isTrue;
+       bool isTrue() {return istrue;}
+       bool isFalse() {return !istrue;}
+       bool istrue;
        CMEMALLOC;
 };
 

diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
index bbb2485bc3245fa82b55826a69e37de1736e5f35..d3f4a2407f51a72199ddceb5500adbce4be633fe 100644 (file)
--- a/src/Test/buildconstraintstest.cc
+++ b/src/Test/buildconstraintstest.cc
@@ -51,7 +51,7 @@ int main(int numargs, char **argv) {
        Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
        solver->addConstraint(pred);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");

diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc
index 53f82127939f5316072b4c01916d501e3403a322..ff2f59bd2646efa6f64fbab2d11b14ef833c7218 100644 (file)
--- a/src/Test/elemequalsattest.cc
+++ b/src/Test/elemequalsattest.cc
@@ -25,7 +25,7 @@ int main(int numargs, char **argv) {
        Boolean *b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");

diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc
index 5ec2bcafcd9002234d83fba9f867edcb90efa386..cd35ba7d42c1ca84011bb65bc8f86fc9cd521e83 100644 (file)
--- a/src/Test/elemequalunsattest.cc
+++ b/src/Test/elemequalunsattest.cc
@@ -20,7 +20,7 @@ int main(int numargs, char **argv) {
        Boolean *b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");

diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc
index d6a796200d7dc30fee4e8eeafa4d231ac902a3a1..87315f509faa9f4d30e7ee61bea47bf1c9e43c45 100644 (file)
--- a/src/Test/funcencodingtest.cc
+++ b/src/Test/funcencodingtest.cc
@@ -73,7 +73,7 @@ int main(int numargs, char **argv) {
        Boolean *pred = solver->applyPredicate(gt, inputs2, 2);
        solver->addConstraint(pred);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",
                                         solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e7));
        else

diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc
index ece659e4699aafa14fc8861ac2d31a871677d118..a21e9c6fbe1d27ff6aa5fa53ce6864784eb9d793 100644 (file)
--- a/src/Test/logicopstest.cc
+++ b/src/Test/logicopstest.cc
@@ -24,7 +24,7 @@ int main(int numargs, char **argv) {
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
        Boolean *barray5[] = {b1, b4};
        solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("b1=%d b2=%d b3=%d b4=%d\n",
                                         solver->getBooleanValue(b1), solver->getBooleanValue(b2),
                                         solver->getBooleanValue(b3), solver->getBooleanValue(b4));

diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc
index b110f29b8698b06d0e6cd19de9abc863afc7d484..b75bfb64843d9933293b478b6592619e4e74d705 100644 (file)
--- a/src/Test/ltelemconsttest.cc
+++ b/src/Test/ltelemconsttest.cc
@@ -18,7 +18,7 @@ int main(int numargs, char **argv) {
        Element *inputs2[] = {e1, e2};
        Boolean *b = solver->applyPredicate(lt, inputs2, 2);
        solver->addConstraint(b);
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");

diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc
index ccf1933a5e9110dbc99bc81e97410ac602f6a57b..72ad021e7eac2e5d9711871e4f759338c0884f98 100644 (file)
--- a/src/Test/ordergraphtest.cc
+++ b/src/Test/ordergraphtest.cc
@@ -46,7 +46,7 @@ int main(int numargs, char **argv) {
        Boolean * array12[] = {o58, o81};
        solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
        
-       /*      if (solver->startEncoding() == 1)
+       /*      if (solver->solve() == 1)
                printf("SAT\n");
        else
        printf("UNSAT\n");*/

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 893338dd5419da5e9e0617ec1e079019054f9792..1d9029098823bf6dcc4fae7ad9f7c923032e2ef4 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -15,7 +15,7 @@ int main(int numargs, char **argv) {
        Boolean *b2 =  solver->orderConstraint(order, 1, 4);
        solver->addConstraint(b1);
        solver->addConstraint(b2);
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("SAT\n");
        else
                printf("UNSAT\n");

diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc
index e998f3bb6dbf42588c1b1f61ed948e6351c967d2..32522476c9d2ddf462019a1378933b858a877dd6 100644 (file)
--- a/src/Test/tablefuncencodetest.cc
+++ b/src/Test/tablefuncencodetest.cc
@@ -50,7 +50,7 @@ int main(int numargs, char **argv) {
        Boolean *pred = solver->applyPredicate(lte, inputs2, 2);
        solver->addConstraint(pred);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " e4=%" PRIu64 " overFlow:%d\n",
                                         solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e3),
                                         solver->getElementValue(e4), solver->getBooleanValue(overflow));

diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc
index e0575e77450f42051020ed085142a05b9a7b406d..02195ea705e57f3513693ab7b40d3b9d5a2171f0 100644 (file)
--- a/src/Test/tablepredicencodetest.cc
+++ b/src/Test/tablepredicencodetest.cc
@@ -58,7 +58,7 @@ int main(int numargs, char **argv) {
        Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
        solver->addConstraint(pred2);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " undefFlag:%d\n",
                                         solver->getElementValue(e1), solver->getElementValue(e2),
                                         solver->getElementValue(e3), solver->getBooleanValue(undef));

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index e9bd7731e1b5030e97eb3c786c5312d322558bd8..37657590a9b0698fc3ea536d794baf9ae1745315 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -16,7 +16,7 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) {
        CSolver * copy=problem->clone();
        copy->setTuner(tuner);
-       int result = copy->startEncoding();
+       int result = copy->solve();
        long long elapsedTime=copy->getElapsedTime();
        long long encodeTime=copy->getEncodeTime();
        long long solveTime=copy->getSolveTime();

diff --git a/src/csolver.cc b/src/csolver.cc
index 3d589b18f94da8668ecfc1233eef4c05ee3ee243..d0aa32ea175c04b0381df87ee41ed9e20f4135bd 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -95,6 +95,11 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
+Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
+       Set *s = createRangeSet(type, lowrange, highrange);
+       return getElementVar(s);
+}
+
 MutableSet *CSolver::createMutableSet(VarType type) {
        MutableSet *set = new MutableSet(type);
        allSets.push(set);
@@ -216,6 +221,25 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui
        }
 }
 
+bool CSolver::isTrue(Boolean *b) {
+       return b->isTrue();
+}
+
+bool CSolver::isFalse(Boolean *b) {
+       return b->isFalse();
+}
+
+Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2) {
+       Boolean * array[] = {arg1, arg2};
+       return applyLogicalOperation(op, array, 2);
+}
+
+Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) {
+       Boolean * array[] = {arg};
+       return applyLogicalOperation(op, array, 1);
+}
+
+
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
        Boolean * newarray[asize];
        switch(op) {
@@ -223,16 +247,14 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) {
                        return ((BooleanLogic *) array[0])->inputs.get(0);
                } else if (array[0]->type == BOOLCONST) {
-                       bool isTrue = ((BooleanConst *) array[0])->isTrue;
-                       return isTrue ? boolFalse : boolTrue;
+                       return array[0]->isTrue() ? boolFalse : boolTrue;
                }
                break;
        }
        case SATC_XOR: {
                for(uint i=0;i<2;i++) {
                        if (array[i]->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) array[i])->isTrue;
-                               if (isTrue) {
+                               if (array[i]->isTrue()) {
                                        newarray[0]=array[1-i];
                                        return applyLogicalOperation(SATC_NOT, newarray, 1);
                                } else
@@ -246,8 +268,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                        if (b->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) b)->isTrue;
-                               if (isTrue)
+                               if (b->isTrue())
                                        return b;
                                else
                                        continue;
@@ -281,8 +302,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                        if (b->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) b)->isTrue;
-                               if (isTrue)
+                               if (b->isTrue())
                                        continue;
                                else
                                        return b;
@@ -299,16 +319,14 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
        }
        case SATC_IMPLIES: {
                if (array[0]->type == BOOLCONST) {
-                       BooleanConst *b=(BooleanConst *) array[0];
-                       if (b->isTrue) {
+                       if (array[0]->isTrue()) {
                                return array[1];
                        } else {
                                return boolTrue;
                        }
                } else if (array[1]->type == BOOLCONST) {
-                       BooleanConst *b=(BooleanConst *) array[0];
-                       if (b->isTrue) {
-                               return b;
+                       if (array[1]->isTrue()) {
+                               return array[1];
                        } else {
                                return applyLogicalOperation(SATC_NOT, array, 1);
                        }
@@ -350,7 +368,7 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
        return order;
 }
 
-int CSolver::startEncoding() {
+int CSolver::solve() {
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();

diff --git a/src/csolver.h b/src/csolver.h
index a067b2fa1cb1495c7a4bba4329534e88efea5974..aa7ccd071d7b22592348b590ed5038adcd40f4fc 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -17,6 +17,8 @@ public:
 
        Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
+       Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
+               
        /** This function creates a mutable set. */
 
        MutableSet *createMutableSet(VarType type);
@@ -84,6 +86,14 @@ public:
 
        Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
 
+               /** This function applies a logical operation to the Booleans in its input. */
+
+       Boolean *applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2);
+
+       /** This function applies a logical operation to the Booleans in its input. */
+
+       Boolean *applyLogicalOperation(LogicOp op, Boolean *arg);
+
        /** This function adds a boolean constraint to the set of constraints
            to be satisfied */
 
@@ -96,7 +106,7 @@ public:
        Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
 
        /** When everything is done, the client calls this function and then csolver starts to encode*/
-       int startEncoding();
+       int solve();
 
        /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
        uint64_t getElementValue(Element *element);
@@ -106,6 +116,9 @@ public:
 
        HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
+       bool isTrue(Boolean *b);
+       bool isFalse(Boolean *b);
+       
        void setUnSAT() { unsat = true; }
 
        bool isUnSAT() { return unsat; }