Found bug... Don't update parent's list until we know we aren't going to be freed

[satune.git] / src / Backend / satorderencoder.cc

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 57447364cfd537b0c999a0845d1772a09a7da886..b977efa782c4ea963f03a4a3da6bbeac80b8da01 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -6,26 +6,27 @@
 #include "orderpair.h"
 #include "set.h"
 #include "tunable.h"
-#include "orderencoder.h"
+#include "orderanalysis.h"
 #include "ordergraph.h"
 #include "orderedge.h"
 #include "element.h"
 #include "predicate.h"
 #include "orderelement.h"
+#include "orderpairresolver.h"
 
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
        switch ( constraint->order->type) {
-       case PARTIAL:
-               return encodePartialOrderSATEncoder(This, constraint);
-       case TOTAL:
-               return encodeTotalOrderSATEncoder(This, constraint);
+       case SATC_PARTIAL:
+               return encodePartialOrderSATEncoder(constraint);
+       case SATC_TOTAL:
+               return encodeTotalOrderSATEncoder(constraint);
        default:
                ASSERT(0);
        }
        return E_BOGUS;
 }
 
-Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
+Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
        if (order->graph != NULL) {
                OrderGraph *graph = order->graph;
                OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
@@ -50,12 +51,12 @@ Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _seco
        return E_NULL;
 }
 
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
        Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
        if (!edgeIsNull(gvalue))
                return gvalue;
 
-       HashTableOrderPair *table = order->orderPairTable;
+       HashtableOrderPair *table = order->orderPairTable;
        bool negate = false;
        OrderPair flipped;
        if (pair->first < pair->second) {
@@ -66,7 +67,7 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
        }
        Edge constraint;
        if (!(table->contains(pair))) {
-               constraint = getNewVarSATEncoder(This);
+               constraint = getNewVarSATEncoder();
                OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
                table->put(paircopy, paircopy);
        } else
@@ -75,49 +76,51 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
        return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
-       ASSERT(boolOrder->order->type == TOTAL);
+Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
+       ASSERT(boolOrder->order->type == SATC_TOTAL);
        if (boolOrder->order->orderPairTable == NULL) {
-               boolOrder->order->initializeOrderHashTable();
-               bool doOptOrderStructure = GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+               //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) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
-                       reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+                       reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
-               createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+               createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
        }
        OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
-       Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
+       Edge constraint = getPairConstraint(boolOrder->order, &pair);
        return constraint;
 }
 
 
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
-#ifdef TRACE_DEBUG
+void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
+#ifdef CONFIG_DEBUG
        model_print("in total order ...\n");
 #endif
-       ASSERT(order->type == TOTAL);
-       Vector<uint64_t> *mems = order->set->members;
-       uint size = mems->getSize();
+       ASSERT(order->type == SATC_TOTAL);
+       Set *set = order->set;
+       uint size = order->set->getSize();
        for (uint i = 0; i < size; i++) {
-               uint64_t valueI = mems->get(i);
+               uint64_t valueI = set->getMemberAt(i);
                for (uint j = i + 1; j < size; j++) {
-                       uint64_t valueJ = mems->get(j);
+                       uint64_t valueJ = set->getMemberAt(j);
                        OrderPair pairIJ(valueI, valueJ, E_NULL);
-                       Edge constIJ = getPairConstraint(This, order, &pairIJ);
+                       Edge constIJ = getPairConstraint(order, &pairIJ);
                        for (uint k = j + 1; k < size; k++) {
-                               uint64_t valueK = mems->get(k);
+                               uint64_t valueK = set->getMemberAt(k);
                                OrderPair pairJK(valueJ, valueK, E_NULL);
                                OrderPair pairIK(valueI, valueK, E_NULL);
-                               Edge constIK = getPairConstraint(This, order, &pairIK);
-                               Edge constJK = getPairConstraint(This, order, &pairJK);
-                               addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+                               Edge constIK = getPairConstraint(order, &pairIK);
+                               Edge constJK = getPairConstraint(order, &pairJK);
+                               addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
                        }
                }
        }
 }
 
-Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
+Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
        ASSERT(pair->first != pair->second);
        bool negate = false;
        OrderPair flipped;
@@ -135,15 +138,15 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
        return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
+Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
        Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
-       Edge loop1 = constraintOR(This->cnf, 3, carray);
+       Edge loop1 = constraintOR(cnf, 3, carray);
        Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
-       Edge loop2 = constraintOR(This->cnf, 3, carray2 );
-       return constraintAND2(This->cnf, loop1, loop2);
+       Edge loop2 = constraintOR(cnf, 3, carray2 );
+       return constraintAND2(cnf, loop1, loop2);
 }
 
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
-       ASSERT(constraint->order->type == PARTIAL);
+Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
+       ASSERT(constraint->order->type == SATC_PARTIAL);
        return E_BOGUS;
 }