Tons of bugs
authorbdemsky <bdemsky@uci.edu>
Tue, 5 Sep 2017 06:15:20 +0000 (23:15 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 5 Sep 2017 06:15:20 +0000 (23:15 -0700)
src/AST/boolean.cc
src/AST/rewriter.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/integerencoding.cc
src/Backend/satorderencoder.cc

index 5d8865e..4ca9c40 100644 (file)
@@ -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) {
index cdb2fb4..937a8b7 100644 (file)
@@ -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);
        }
 }
 
index 359a3a3..3791b10 100644 (file)
@@ -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
index b52ccf8..25ef990 100644 (file)
@@ -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);
 }
 
index 514bad9..b977efa 100644 (file)
@@ -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) {