Compiles

diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc
index 9fed23623616133b54dfa36e6fcf54bb6470d70f..827f9e1c02fdbff2d9354b9d1059bbf4125c9162 100644 (file)
--- a/src/AST/asthash.cc
+++ b/src/AST/asthash.cc
@@ -4,7 +4,7 @@
 #include "boolean.h"
 #include "element.h"
 
-bool compareArray(Array<Boolean *> *inputs1, Array<Boolean *> *inputs2) {
+bool compareArray(Array<BooleanEdge> *inputs1, Array<BooleanEdge> *inputs2) {
        if (inputs1->getSize() != inputs2->getSize())
                return false;
        for (uint i = 0; i < inputs1->getSize(); i++) {
@@ -24,10 +24,10 @@ bool compareArray(Array<Element *> *inputs1, Array<Element *> *inputs2) {
        return true;
 }
 
-uint hashArray(Array<Boolean *> *inputs) {
+uint hashArray(Array<BooleanEdge> *inputs) {
        uint hash = inputs->getSize();
        for (uint i = 0; i < inputs->getSize(); i++) {
-               uint newval = (uint)(uintptr_t) inputs->get(i);
+               uint newval = (uint)(uintptr_t) inputs->get(i).getRaw();
                hash ^= newval;
                hash = (hash << 3) | (hash >> 29);
        }

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 7c3771095a2ca448eab0ab4e84dea940be384da7..0f9491a4c2277dd1565ae1911e572432f2a6e596 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -31,7 +31,7 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
        order->constraints.push(this);
 }
 
-BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) :
+BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus) :
        Boolean(PREDICATEOP),
        predicate(_predicate),
        encoding(this),
@@ -42,39 +42,44 @@ BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uin
        }
 }
 
-BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) :
+BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) :
        Boolean(LOGICOP),
        op(_op),
        inputs(array, asize) {
 }
 
+BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) {
+       bool isnegated=e.isNegated();
+       Boolean *b=e->clone(solver, map);
+       BooleanEdge be=BooleanEdge(b);
+       return isnegated ? be.negate() : be;
+}
+
 Boolean *BooleanConst::clone(CSolver *solver, CloneMap *map) {
-       if (istrue)
-               return solver->getBooleanTrue();
-       else
-               return solver->getBooleanFalse();
+       return solver->getBooleanTrue().getRaw();
 }
 
 Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
        Boolean *b = (Boolean *) map->get(this);
        if (b != NULL)
                return b;
-       Boolean *bvar = solver->getBooleanVar(type);
-       map->put(this, bvar);
-       return bvar;
+       BooleanEdge bvar = solver->getBooleanVar(type);
+       Boolean * base=bvar.getRaw();
+       map->put(this, base);
+       return base;
 }
 
 Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) {
        Order *ordercopy = order->clone(solver, map);
-       return solver->orderConstraint(ordercopy, first, second);
+       return solver->orderConstraint(ordercopy, first, second).getRaw();
 }
 
 Boolean *BooleanLogic::clone(CSolver *solver, CloneMap *map) {
-       Boolean *array[inputs.getSize()];
+       BooleanEdge array[inputs.getSize()];
        for (uint i = 0; i < inputs.getSize(); i++) {
-               array[i] = inputs.get(i)->clone(solver, map);
+               array[i] = cloneEdge(solver, map, inputs.get(i));
        }
-       return solver->applyLogicalOperation(op, array, inputs.getSize());
+       return solver->applyLogicalOperation(op, array, inputs.getSize()).getRaw();
 }
 
 Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
@@ -83,7 +88,7 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
                array[i] = inputs.get(i)->clone(solver, map);
        }
        Predicate *pred = predicate->clone(solver, map);
-       Boolean *defstatus = (undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL;
+       BooleanEdge defstatus = undefStatus ? cloneEdge(solver, map, undefStatus) : BooleanEdge();
 
-       return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus);
+       return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw();
 }

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 5a4b5af48fd0568fb43c4c5c769bf484ff0a46fb..218fc501dab56b41e4fc7f1cb1258406a304b6a7 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -9,6 +9,8 @@
 #include "functionencoding.h"
 #include "constraint.h"
 
+
+
 class Boolean : public ASTNode {
 public:
        Boolean(ASTNodeType _type);
@@ -56,24 +58,24 @@ public:
 
 class BooleanPredicate : public Boolean {
 public:
-       BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus);
+       BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus);
        Boolean *clone(CSolver *solver, CloneMap *map);
 
        Predicate *predicate;
        FunctionEncoding encoding;
        Array<Element *> inputs;
-       Boolean *undefStatus;
+       BooleanEdge undefStatus;
        FunctionEncoding *getFunctionEncoding() {return &encoding;}
        CMEMALLOC;
 };
 
 class BooleanLogic : public Boolean {
 public:
-       BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize);
+       BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize);
        Boolean *clone(CSolver *solver, CloneMap *map);
 
        LogicOp op;
-       Array<Boolean *> inputs;
+       Array<BooleanEdge> inputs;
        CMEMALLOC;
 };
 #endif

diff --git a/src/AST/element.cc b/src/AST/element.cc
index e47d195eff65058896da811c77e90ef79c713c1f..3fe8cef45710eee5c3ced313c9325700c73629db 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -16,7 +16,7 @@ ElementSet::ElementSet(Set *s) :
        set(s) {
 }
 
-ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) :
+ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, BooleanEdge _overflowstatus) :
        Element(ELEMFUNCRETURN),
        function(_function),
        inputs(array, numArrays),

diff --git a/src/AST/element.h b/src/AST/element.h
index f1ba4ebb139bf064a34ba686fc08b0c83a5636a3..c3a3ed9fe2bd764207756b8fdfbc755cd1dfd0cc 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -38,10 +38,10 @@ public:
 
 class ElementFunction : public Element {
 public:
-       ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
+       ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
        Function *function;
        Array<Element *> inputs;
-       Boolean *overflowstatus;
+       BooleanEdge overflowstatus;
        FunctionEncoding functionencoding;
        Element *clone(CSolver *solver, CloneMap *map);
        CMEMALLOC;

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 9751e057f3e599ce320571fb6cc7bd98bc29b087..80e1f1a90d4b34085527de89e2fdd678949ac2fc 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -2,7 +2,11 @@
 #include "boolean.h"
 #include "csolver.h"
 
-void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
+void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
+       if (constraints.contains(bexpr.negate())) {
+               constraints.remove(bexpr.negate());
+               setUnSAT();
+       }       
        if (constraints.contains(bexpr)) {
                constraints.remove(bexpr);
        }
@@ -15,12 +19,10 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
                case SATC_AND:
                        handleANDTrue(logicop, bexpr);
                        break;
-               case SATC_NOT:
-                       replaceBooleanWithFalse(parent);
-                       break;
                case SATC_IFF:
                        handleIFFTrue(logicop, bexpr);
                        break;
+               case SATC_NOT:
                case SATC_OR:
                case SATC_XOR:
                case SATC_IMPLIES:
@@ -29,12 +31,22 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
        }
 }
 
-void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
+void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
+       //Canonicalize
+       if (oldb.isNegated()) {
+               oldb=oldb.negate();
+               newb=newb.negate();
+       }
        if (constraints.contains(oldb)) {
                constraints.remove(oldb);
                constraints.add(newb);
        }
+       if (constraints.contains(oldb.negate())) {
+               constraints.remove(oldb.negate());
+               constraints.add(newb.negate());
+       }
 
+       BooleanEdge oldbnegated = oldb.negate();
        uint size = oldb->parents.getSize();
        for (uint i = 0; i < size; i++) {
                Boolean *parent = oldb->parents.get(i);
@@ -43,74 +55,60 @@ void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
                uint parentsize = logicop->inputs.getSize();
 
                for (uint j = 0; j < parentsize; j++) {
-                       Boolean *b = logicop->inputs.get(i);
+                       BooleanEdge b = logicop->inputs.get(i);
                        if (b == oldb) {
                                logicop->inputs.set(i, newb);
                                newb->parents.push(parent);
+                       } else if (b == oldbnegated) {
+                               logicop->inputs.set(i, newb.negate());
+                               newb->parents.push(parent);
                        }
                }
        }
 }
 
-void handleIFFFalse(BooleanLogic *bexpr, Boolean *child) {
-       uint size = bexpr->inputs.getSize();
-       Boolean *b = bexpr->inputs.get(0);
-       uint childindex = (b == child) ? 0 : 1;
-       bexpr->inputs.remove(childindex);
-       bexpr->op = SATC_NOT;
-}
-
-void CSolver::handleIFFTrue(BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
        uint size = bexpr->inputs.getSize();
-       Boolean *b = bexpr->inputs.get(0);
-       uint otherindex = (b == child) ? 1 : 0;
-       replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
+       BooleanEdge b0 = bexpr->inputs.get(0);
+       BooleanEdge b1 = bexpr->inputs.get(1);
+       BooleanEdge childnegate = child.negate();
+       if (b0 == child) {
+               replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
+       } else if (b0 == childnegate) {
+               replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
+       } else if (b1 == child) {
+               replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
+       } else if (b1 == childnegate) {
+               replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
+       } else
+               ASSERT(0);
 }
 
-void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
-       uint size = bexpr->inputs.getSize();
-
-       if (size == 1) {
-               replaceBooleanWithTrue(bexpr);
-               return;
-       }
-
-       for (uint i = 0; i < size; i++) {
-               Boolean *b = bexpr->inputs.get(i);
+void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
+       BooleanEdge childNegate=child.negate();
+       
+       for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
+               BooleanEdge b = bexpr->inputs.get(i);
+               
                if (b == child) {
                        bexpr->inputs.remove(i);
+                       i--;
+               }
+               
+               if (b == childNegate) {
+                       replaceBooleanWithFalse(bexpr);
+                       return;
                }
        }
 
-       if (size == 2) {
+       uint size=bexpr->inputs.getSize();
+       if (size == 0) {
+               replaceBooleanWithTrue(bexpr);
+       } else if (size == 1) {
                replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
        }
 }
 
-void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
-       if (constraints.contains(bexpr)) {
-               setUnSAT();
-               constraints.remove(bexpr);
-       }
-
-       uint size = bexpr->parents.getSize();
-       for (uint i = 0; i < size; i++) {
-               Boolean *parent = bexpr->parents.get(i);
-               BooleanLogic *logicop = (BooleanLogic *) parent;
-               switch (logicop->op) {
-               case SATC_AND:
-                       replaceBooleanWithFalse(parent);
-                       break;
-               case SATC_NOT:
-                       replaceBooleanWithTrue(parent);
-                       break;
-               case SATC_IFF:
-                       handleIFFFalse(logicop, bexpr);
-                       break;
-               case SATC_OR:
-               case SATC_XOR:
-               case SATC_IMPLIES:
-                       ASSERT(0);
-               }
-       }
+void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
+       replaceBooleanWithTrue(bexpr.negate());
 }

diff --git a/src/AST/rewriter.h b/src/AST/rewriter.h
index 3e3488f67ca5ef29396af60affdc5fbaa4b2816a..7c48092601848903e6c8eebbe7773a4fdaaab913 100644 (file)
--- a/src/AST/rewriter.h
+++ b/src/AST/rewriter.h
@@ -2,6 +2,4 @@
 #define REWRITER_H
 #include "classlist.h"
 
-void handleIFFFalse(BooleanLogic *bexpr, Boolean *child);
-
 #endif

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 2aa9e5d8e491ac24cf03690243cbb0147339e633..6b634361a3f0727fa1ac1b86163cb905c7e71f5f 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -2,12 +2,19 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
-       SetIteratorBoolean *iterator = This->getConstraints();
+       SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
-               Boolean *boolean = iterator->next();
-               updatePolarity(boolean, P_TRUE);
-               updateMustValue(boolean, BV_MUSTBETRUE);
-               computePolarityAndBooleanValue(boolean);
+               BooleanEdge boolean = iterator->next();
+               Boolean *b = boolean.getBoolean();
+               bool isNegated = boolean.isNegated();
+               if (isNegated) {
+                       updatePolarity(b, P_FALSE);
+                       updateMustValue(b, BV_MUSTBEFALSE);
+               } else {
+                       updatePolarity(b, P_TRUE);
+                       updateMustValue(b, BV_MUSTBETRUE);
+               }
+               computePolarityAndBooleanValue(b);
        }
        delete iterator;
 }
@@ -35,9 +42,9 @@ void computePolarityAndBooleanValue(Boolean *This) {
 }
 
 void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
-       if (This->undefStatus != NULL) {
-               updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
-               computePolarityAndBooleanValue(This->undefStatus);
+       if (This->undefStatus) {
+               updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
+               computePolarityAndBooleanValue(This->undefStatus.getBoolean());
        }
 }
 
@@ -46,7 +53,7 @@ void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
        computeLogicOpPolarity(This);
        uint size = This->inputs.getSize();
        for (uint i = 0; i < size; i++) {
-               computePolarityAndBooleanValue(This->inputs.get(i));
+               computePolarityAndBooleanValue(This->inputs.get(i).getBoolean());
        }
 }
 
@@ -84,19 +91,15 @@ void computeLogicOpPolarity(BooleanLogic *This) {
        case SATC_AND: {
                uint size = This->inputs.getSize();
                for (uint i = 0; i < size; i++) {
-                       Boolean *tmp = This->inputs.get(i);
-                       updatePolarity(tmp, parentpolarity);
+                       BooleanEdge tmp = This->inputs.get(i);
+                       Boolean *btmp = tmp.getBoolean();
+                       updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity);
                }
                break;
        }
-       case SATC_NOT: {
-               Boolean *tmp = This->inputs.get(0);
-               updatePolarity(tmp, negatePolarity(parentpolarity));
-               break;
-       }
        case SATC_IFF: {
-               updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
-               updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
+               updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE);
+               updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE);
                break;
        }
        default:
@@ -111,14 +114,12 @@ void computeLogicOpBooleanValue(BooleanLogic *This) {
                if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
                        uint size = This->inputs.getSize();
                        for (uint i = 0; i < size; i++) {
-                               updateMustValue(This->inputs.get(i), parentbv);
+                               BooleanEdge be=This->inputs.get(i);
+                               updateMustValue(be.getBoolean(), be.isNegated()?negateBooleanValue(parentbv):parentbv);
                        }
                }
                return;
        }
-       case SATC_NOT:
-               updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
-               return;
        case SATC_IFF:
                return;
        default:

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 6664a677f2b10664e7e11ab894f8f98287e807e4..a4aacdf5a1f93d171d963e57c1eff127f8bdd430 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -55,7 +55,7 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder,
        Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
        Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
-       Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
+       BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
        solver->addConstraint(boolean);
        solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index fd60f45df737ab7ebcab9cbbda7830808a34a075..4020ad625b49271aa1c255e10645ad312ef4aca2 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -26,20 +26,22 @@ int SATEncoder::solve() {
 }
 
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
-       SetIteratorBoolean *iterator = csolver->getConstraints();
+       SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
-               Boolean *constraint = iterator->next();
+               BooleanEdge constraint = iterator->next();
                Edge c = encodeConstraintSATEncoder(constraint);
                addConstraintCNF(cnf, c);
        }
        delete iterator;
 }
 
-Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
+Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        Edge result;
+       Boolean * constraint = c.getBoolean();
+
        if (booledgeMap.contains(constraint)) {
                Edge e = {(Node *) booledgeMap.get(constraint)};
-               return e;
+               return c.isNegated() ? constraintNegate(e) : e;
        }
 
        switch (constraint->type) {
@@ -60,7 +62,7 @@ Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
                exit(-1);
        }
        booledgeMap.put(constraint, result.node_ptr);
-       return result;
+       return c.isNegated() ? constraintNegate(result) : result;
 }
 
 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 25f6918238c99641cd9cc18b0556330c83b1ea2b..7af3e559178c87a1e7dc796ea715260d43a53ab4 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -14,7 +14,7 @@ public:
        SATEncoder(CSolver *solver);
        ~SATEncoder();
        void encodeAllSATEncoder(CSolver *csolver);
-       Edge encodeConstraintSATEncoder(Boolean *constraint);
+       Edge encodeConstraintSATEncoder(BooleanEdge constraint);
        CNF *getCNF() { return cnf;}
        long long getSolveTime() { return cnf->solveTime; }
        long long getEncodeTime() { return cnf->encodeTime; }

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 41b687ec17aa2d6cac9d10511c91ea33c9af52c9..ba8b32b507f1a2c2f6672dbd3a7c4594813bfaaf 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -108,7 +108,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                vals[i] = set->getElement(indices[i]);
        }
 
-       Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var;
+       Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 
        bool notfinished = true;
        while (notfinished) {

diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h
index 982e0c5cfed2d397e95a3f1f8bdf486aedfcd8e8..e30a5309b57b0330c37fe9ff307ddc5f02fc1163 100644 (file)
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -4,9 +4,33 @@
 #include "cppvector.h"
 #include "hashset.h"
 
-typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
+class BooleanEdge {
+ public:
+ BooleanEdge() : b(NULL) {}
+ BooleanEdge(Boolean * _b) : b(_b) {}
+       BooleanEdge negate() {return BooleanEdge((Boolean *)(((uintptr_t) b) ^ 1));}
+       bool operator==(BooleanEdge e) { return b==e.b;}
+       bool operator!=(BooleanEdge e) { return b!=e.b;}
+       bool isNegated() { return ((uintptr_t) b) & 1; }
+       Boolean * getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
+       Boolean * getRaw() {return b;}
+       Boolean * operator->() {return getBoolean();}
+       operator bool() const {return b != NULL;}
+ private:
+       Boolean *b;
+};
+
+inline bool boolEdgeEquals(BooleanEdge b1, BooleanEdge b2) {
+       return b1==b2;
+}
+
+inline unsigned int boolEdgeHash(BooleanEdge b) {
+       return (unsigned int) (((uintptr_t)b.getRaw())>>4);
+}
+                                                                       
+typedef Hashset<BooleanEdge, uintptr_t, 4, & boolEdgeHash, & boolEdgeEquals> HashsetBooleanEdge;
 typedef Hashset<Order *, uintptr_t, 4> HashsetOrder;
-typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
+typedef SetIterator<BooleanEdge, uintptr_t, 4, & boolEdgeHash, & boolEdgeEquals> SetIteratorBooleanEdge;
 typedef SetIterator<Order *, uintptr_t, 4> SetIteratorOrder;
 
 #endif

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 9b4487ebbbfd055e7e280bdd22a16a9e16e4fbbe..466d839f625a882fe416676ccf5038bea7627fc0 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -14,10 +14,10 @@
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-       SetIteratorBoolean *iterator = This->getConstraints();
+       SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
-               Boolean *boolean = iterator->next();
-               naiveEncodingConstraint(boolean);
+               BooleanEdge b = iterator->next();
+               naiveEncodingConstraint(b.getBoolean());
        }
        delete iterator;
 }
@@ -46,7 +46,7 @@ void naiveEncodingConstraint(Boolean *This) {
 
 void naiveEncodingLogicOp(BooleanLogic *This) {
        for (uint i = 0; i < This->inputs.getSize(); i++) {
-               naiveEncodingConstraint(This->inputs.get(i));
+               naiveEncodingConstraint(This->inputs.get(i).getBoolean());
        }
 }
 

diff --git a/src/csolver.cc b/src/csolver.cc
index c3208b91ec5fdd2747ffc763fa3e3b52dd60291a..9112e54dc29c265c20fe4efe00369ac0532101df 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -20,8 +20,8 @@
 #include <stdlib.h>
 
 CSolver::CSolver() :
-       boolTrue(new BooleanConst(true)),
-       boolFalse(new BooleanConst(false)),
+       boolTrue(BooleanEdge(new BooleanConst(true))),
+       boolFalse(boolTrue.negate()),
        unsat(false),
        tuner(NULL),
        elapsedTime(0)
@@ -67,17 +67,16 @@ CSolver::~CSolver() {
                delete allFunctions.get(i);
        }
 
-       delete boolTrue;
-       delete boolFalse;
+       delete boolTrue.getBoolean();
        delete satEncoder;
 }
 
 CSolver *CSolver::clone() {
        CSolver *copy = new CSolver();
        CloneMap map;
-       SetIteratorBoolean *it = getConstraints();
+       SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
-               Boolean *b = it->next();
+               BooleanEdge b = it->next();
                copy->addConstraint(b->clone(copy, &map));
        }
        delete it;
@@ -140,7 +139,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
        }
 }
 
-Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
+Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
        Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
        Element *e = elemMap.get(element);
        if (e == NULL) {
@@ -191,52 +190,52 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
        return function;
 }
 
-Boolean *CSolver::getBooleanVar(VarType type) {
+BooleanEdge CSolver::getBooleanVar(VarType type) {
        Boolean *boolean = new BooleanVar(type);
        allBooleans.push(boolean);
-       return boolean;
+       return BooleanEdge(boolean);
 }
 
-Boolean *CSolver::getBooleanTrue() {
+BooleanEdge CSolver::getBooleanTrue() {
        return boolTrue;
 }
 
-Boolean *CSolver::getBooleanFalse() {
+BooleanEdge CSolver::getBooleanFalse() {
        return boolFalse;
 }
 
-Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
+BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
        return applyPredicateTable(predicate, inputs, numInputs, NULL);
 }
 
-Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
+BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
        BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
        Boolean *b = boolMap.get(boolean);
        if (b == NULL) {
                boolMap.put(boolean, boolean);
                allBooleans.push(boolean);
-               return boolean;
+               return BooleanEdge(boolean);
        } else {
                delete boolean;
-               return b;
+               return BooleanEdge(b);
        }
 }
 
-bool CSolver::isTrue(Boolean *b) {
-       return b->isTrue();
+bool CSolver::isTrue(BooleanEdge b) {
+       return b.isNegated()?b->isFalse():b->isTrue();
 }
 
-bool CSolver::isFalse(Boolean *b) {
-       return b->isFalse();
+bool CSolver::isFalse(BooleanEdge b) {
+       return b.isNegated()?b->isTrue():b->isFalse();
 }
 
-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) {
-       Boolean *array[] = {arg1, arg2};
+BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
+       BooleanEdge array[] = {arg1, arg2};
        return applyLogicalOperation(op, array, 2);
 }
 
-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) {
-       Boolean *array[] = {arg};
+BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
+       BooleanEdge array[] = {arg};
        return applyLogicalOperation(op, array, 1);
 }
 
@@ -251,16 +250,11 @@ static int ptrcompares(const void *p1, const void *p2) {
                return 1;
 }
 
-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
-       Boolean *newarray[asize];
+BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
+       BooleanEdge newarray[asize];
        switch (op) {
        case SATC_NOT: {
-               if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) {
-                       return ((BooleanLogic *) array[0])->inputs.get(0);
-               } else if (array[0]->type == BOOLCONST) {
-                       return array[0]->isTrue() ? boolFalse : boolTrue;
-               }
-               break;
+               return array[0].negate();
        }
        case SATC_IFF: {
                for (uint i = 0; i < 2; i++) {
@@ -284,7 +278,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
        case SATC_AND: {
                uint newindex = 0;
                for (uint i = 0; i < asize; i++) {
-                       Boolean *b = array[i];
+                       BooleanEdge b = array[i];
                        if (b->type == BOOLCONST) {
                                if (b->isTrue())
                                        continue;
@@ -298,7 +292,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                } else if (newindex == 1) {
                        return newarray[0];
                } else {
-                       qsort(newarray, asize, sizeof(Boolean *), ptrcompares);
+                       qsort(newarray, asize, sizeof(BooleanEdge), ptrcompares);
                        array = newarray;
                        asize = newindex;
                }
@@ -320,27 +314,27 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
        if (b == NULL) {
                boolMap.put(boolean, boolean);
                allBooleans.push(boolean);
-               return boolean;
+               return BooleanEdge(boolean);
        } else {
                delete boolean;
-               return b;
+               return BooleanEdge(b);
        }
 }
 
-Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
+BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
        Boolean *constraint = new BooleanOrder(order, first, second);
        allBooleans.push(constraint);
-       return constraint;
+       return BooleanEdge(constraint);
 }
 
-void CSolver::addConstraint(Boolean *constraint) {
+void CSolver::addConstraint(BooleanEdge constraint) {
        if (constraint == boolTrue)
                return;
        else if (constraint == boolFalse)
                setUnSAT();
        else {
-               if (constraint->type == LOGICOP) {
-                       BooleanLogic *b=(BooleanLogic *) constraint;
+               if (!constraint.isNegated() && constraint->type == LOGICOP) {
+                       BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
                        if (b->op==SATC_AND) {
                                for(uint i=0;i<b->inputs.getSize();i++) {
                                        addConstraint(b->inputs.get(i));
@@ -401,7 +395,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        exit(-1);
 }
 
-bool CSolver::getBooleanValue(Boolean *boolean) {
+bool CSolver::getBooleanValue(BooleanEdge bedge) {
+       Boolean *boolean=bedge.getBoolean();
        switch (boolean->type) {
        case BOOLEANVAR:
                return getBooleanVariableValueSATTranslator(this, boolean);

diff --git a/src/csolver.h b/src/csolver.h
index 618f88e0b4ed0635454f8f86d763dbdb70acf687..2875a9c78365e708912ddcd5ef2620837212af66 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -41,13 +41,13 @@ public:
        /** This function creates an element constrant. */
        Element *getElementConst(VarType type, uint64_t value);
 
-       Boolean *getBooleanTrue();
+       BooleanEdge getBooleanTrue();
 
-       Boolean *getBooleanFalse();
+       BooleanEdge getBooleanFalse();
 
        /** This function creates a boolean variable. */
 
-       Boolean *getBooleanVar(VarType type);
+       BooleanEdge getBooleanVar(VarType type);
 
        /** This function creates a function operator. */
 
@@ -75,36 +75,36 @@ public:
 
        /** This function applies a function to the Elements in its input. */
 
-       Element *applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
+       Element *applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
 
        /** This function applies a predicate to the Elements in its input. */
 
-       Boolean *applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus);
+       BooleanEdge applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus);
 
-       Boolean *applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
+       BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
 
        /** This function applies a logical operation to the Booleans in its input. */
 
-       Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
+       BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
 
        /** This function applies a logical operation to the Booleans in its input. */
 
-       Boolean *applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2);
+       BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2);
 
        /** This function applies a logical operation to the Booleans in its input. */
 
-       Boolean *applyLogicalOperation(LogicOp op, Boolean *arg);
+       BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg);
 
        /** This function adds a boolean constraint to the set of constraints
            to be satisfied */
 
-       void addConstraint(Boolean *constraint);
+       void addConstraint(BooleanEdge constraint);
 
        /** This function instantiates an order of type type over the set set. */
        Order *createOrder(OrderType type, Set *set);
 
        /** This function instantiates a boolean on two items in an order. */
-       Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
+       BooleanEdge 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 solve();
@@ -113,12 +113,12 @@ public:
        uint64_t getElementValue(Element *element);
 
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
-       bool getBooleanValue(Boolean *boolean);
+       bool getBooleanValue(BooleanEdge boolean);
 
        bool getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
-       bool isTrue(Boolean *b);
-       bool isFalse(Boolean *b);
+       bool isTrue(BooleanEdge b);
+       bool isFalse(BooleanEdge b);
 
        void setUnSAT() { unsat = true; }
 
@@ -129,13 +129,13 @@ public:
 
        Tuner *getTuner() { return tuner; }
 
-       SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
+       SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
 
        SATEncoder *getSATEncoder() {return satEncoder;}
 
-       void replaceBooleanWithTrue(Boolean *bexpr);
-       void replaceBooleanWithFalse(Boolean *bexpr);
-       void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+       void replaceBooleanWithTrue(BooleanEdge bexpr);
+       void replaceBooleanWithFalse(BooleanEdge bexpr);
+       void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
        void autoTune(uint budget);
 
@@ -147,11 +147,11 @@ public:
        CMEMALLOC;
 
 private:
-       void handleIFFTrue(BooleanLogic *bexpr, Boolean *child);
-       void handleANDTrue(BooleanLogic *bexpr, Boolean *child);
+       void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
+       void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
 
        /** This is a vector of constraints that must be satisfied. */
-       HashsetBoolean constraints;
+       HashsetBooleanEdge constraints;
 
        /** This is a vector of all boolean structs that we have allocated. */
        Vector<Boolean *> allBooleans;
@@ -176,8 +176,8 @@ private:
        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;
 
-       Boolean *boolTrue;
-       Boolean *boolFalse;
+       BooleanEdge boolTrue;
+       BooleanEdge boolFalse;
 
        /** These two tables are used for deduplicating entries. */
        BooleanMatchMap boolMap;