Fixing more bugs

diff --git a/src/AST/order.h b/src/AST/order.h
index d922235adf09f3e12f373127489e512a6335e5b0..cc8b45e4adc7774e6b3510ef66fa80309a82ebbd 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -19,7 +19,7 @@ public:
        Order *clone(CSolver *solver, CloneMap *map);
        Vector<BooleanOrder *> constraints;
        OrderEncoding encoding;
-       void setOrderResolver(OrderResolver *_resolver) { encoding.resolver = _resolver;};
+       void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
        void initializeOrderHashtable();
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);

diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
index fcc9eda132f0b3b1e0c56e5e8e409968a243f9e2..bb241de593463b4ca9c860ba13e8ffacea82258d 100644 (file)
--- a/src/ASTAnalyses/ordergraph.cc
+++ b/src/ASTAnalyses/ordergraph.cc
@@ -13,6 +13,7 @@ OrderGraph::OrderGraph(Order *_order) :
 
 OrderGraph *buildOrderGraph(Order *order) {
        OrderGraph *orderGraph = new OrderGraph(order);
+       order->graph = orderGraph;
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
                orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 7d276e2edaf21d6e4c4c7716e824d511ee679ff5..359a3a3afa4e15899396df76c9399d38eae19e09 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -60,17 +60,15 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
-               /*
+               
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
                if (mustReachPrune)
                        removeMustBeTrueNodes(solver, graph);
-               */
                
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(order, graph);
-               delete graph;
        }
        delete orderit;
        delete orders;

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index a4aacdf5a1f93d171d963e57c1eff127f8bdd430..ab88f2065be16dd226cceaf9bd9ae9d0eacc5fa2 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -35,6 +35,7 @@ void IntegerEncodingTransform::integerEncode(Order *currOrder) {
                encodingRecord = new IntegerEncodingRecord(
                        solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
                orderIntEncoding->put(currOrder, encodingRecord);
+               currOrder->setOrderEncodingType( INTEGERENCODING );
        } else {
                encodingRecord = orderIntEncoding->get(currOrder);
        }

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 466d839f625a882fe416676ccf5038bea7627fc0..2d77608772ba3d01351aa0a7b89e857b7c9d02ca 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -28,7 +28,8 @@ void naiveEncodingConstraint(Boolean *This) {
                return;
        }
        case ORDERCONST: {
-               ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
+               if(((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+                       ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
                return;
        }
        case LOGICOP: {

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 8633415044a9cc1c304363585feed09a6db315cb..d9ad852594103b727690c870deb75a8aa101a212 100755 (executable)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -15,9 +15,15 @@ int main(int numargs, char **argv) {
        BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
        solver->addConstraint(b1);
        solver->addConstraint(b2);
-       if (solver->solve() == 1)
+       if (solver->solve() == 1){
                printf("SAT\n");
-       else
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+                       solver->getOrderConstraintValue(order, 5, 1), 
+                       solver->getOrderConstraintValue(order, 1, 4),
+                       solver->getOrderConstraintValue(order, 5, 4),
+                       solver->getOrderConstraintValue(order, 1, 5));
+       } else {
                printf("UNSAT\n");
+       }
        delete solver;
 }

diff --git a/src/csolver.cc b/src/csolver.cc
index b353791e768e263c87799cd6c75435deb87b03d5..f52c4eb655a518a75d8fb843da27e7e7cf13846f 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -400,12 +400,11 @@ int CSolver::solve() {
        long long startTime = getTimeNano();
        computePolarities(this);
 
-       DecomposeOrderTransform dot(this);
-       dot.doTransform();
+//     DecomposeOrderTransform dot(this);
+//     dot.doTransform();
 
-       //This leaks like crazy
-       //      IntegerEncodingTransform iet(this);
-       //iet.doTransform();
+       IntegerEncodingTransform iet(this);
+       iet.doTransform();
 
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);