Tons of bugs

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 5d8865e466717f6625fba9242c5dc15c9b7355e2..4ca9c404522deb2e324fc617580e8243d2159b37 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -47,6 +47,9 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uin
        op(_op),
        replaced(false),
        inputs(array, asize) {
+       for (uint i = 0; i < asize; i++) {
+               array[i]->parents.push(this);
+       }
 }
 
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) {

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index cdb2fb4be1ba2c6e44ac1e8fa29f5509f21bf84c..937a8b74cb442f2f6a0738fa039da845a0558eb8 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -59,19 +59,20 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        for (uint i = 0; i < size; i++) {
                Boolean *parent = oldb->parents.get(i);
                BooleanLogic *logicop = (BooleanLogic *) parent;
-
+               boolMap.remove(parent); //could change parent's hash
+               
                uint parentsize = logicop->inputs.getSize();
-
                for (uint j = 0; j < parentsize; j++) {
-                       BooleanEdge b = logicop->inputs.get(i);
+                       BooleanEdge b = logicop->inputs.get(j);
                        if (b == oldb) {
-                               logicop->inputs.set(i, newb);
+                               logicop->inputs.set(j, newb);
                                newb->parents.push(parent);
                        } else if (b == oldbnegated) {
-                               logicop->inputs.set(i, newb.negate());
+                               logicop->inputs.set(j, newb.negate());
                                newb->parents.push(parent);
                        }
                }
+               boolMap.put(parent, parent);
        }
 }
 

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 359a3a3afa4e15899396df76c9399d38eae19e09..3791b100fe6358f0ee39b3e2cce90a4410408526 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -84,14 +84,33 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
                OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
                if (from->sccNum != to->sccNum) {
-                       OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
-                       if (edge->polPos) {
-                               solver->replaceBooleanWithTrue(orderconstraint);
-                       } else if (edge->polNeg) {
-                               solver->replaceBooleanWithFalse(orderconstraint);
+                       OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
+                       if (edge != NULL) {
+                               if (edge->polPos) {
+                                       solver->replaceBooleanWithTrue(orderconstraint);
+                               } else if (edge->polNeg) {
+                                       solver->replaceBooleanWithFalse(orderconstraint);
+                               } else {
+                                       //This case should only be possible if constraint isn't in AST
+                                       //This can happen, so don't do anything
+                                       ;
+                               }
                        } else {
-                               //This case should only be possible if constraint isn't in AST
-                               ASSERT(0);
+                               OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
+                               if (invedge != NULL) {
+                                       if (invedge->polPos) {
+                                               solver->replaceBooleanWithFalse(orderconstraint);
+                                       } else if (edge->polNeg) {
+                                               //This case shouldn't happen...  If we have a partial order,
+                                               //then we should have our own edge...If we have a total
+                                               //order, then this edge should be positive...
+                                               ASSERT(0);
+                                       } else {
+                                               //This case should only be possible if constraint isn't in AST
+                                               //This can happen, so don't do anything
+                                               ;
+                                       }
+                               }
                        }
                } else {
                        //Build new order and change constraint's order

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index b52ccf84921cb5cafe16d314cea7c7deed4bb002..25ef990ee38bca14e5f2aee152382b073eb58e30 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -48,7 +48,6 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *bool
        Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
        BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
-       solver->addConstraint(boolean);
        solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }
 

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 514bad902442f4dd0e496f1d0bd2256560c321e2..b977efa782c4ea963f03a4a3da6bbeac80b8da01 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -15,8 +15,6 @@
 #include "orderpairresolver.h"
 
 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
-       //This is pairwised encoding ...
-       constraint->order->setOrderResolver(new OrderPairResolver(solver, constraint->order));
        switch ( constraint->order->type) {
        case SATC_PARTIAL:
                return encodePartialOrderSATEncoder(constraint);
@@ -81,6 +79,8 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
        ASSERT(boolOrder->order->type == SATC_TOTAL);
        if (boolOrder->order->orderPairTable == NULL) {
+               //This is pairwised encoding ...
+               boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
                boolOrder->order->initializeOrderHashtable();
                bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {