Try to fix encapsulation

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 62f6bff6fc7c9e4c133aa10ce2f0abb04480761e..6ec11935080b208c4202238ed614109266a6c2cc 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -40,7 +40,6 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a
        Boolean(LOGICOP),
        op(_op),
        inputs(array, asize) {
-       solver->allBooleans.push(this);
 }
 
 BooleanPredicate::~BooleanPredicate() {

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index f659b4e994cf34fbcc121546981e9bc2709dcf8b..e8e9c847eb6aaec678ee46c0923ff99590ad65f3 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -2,9 +2,9 @@
 #include "boolean.h"
 #include "csolver.h"
 
-void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) {
-       if (This->constraints.contains(bexpr)) {
-               This->constraints.remove(bexpr);
+void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
+       if (constraints.contains(bexpr)) {
+               constraints.remove(bexpr);
        }
 
        uint size = bexpr->parents.getSize();
@@ -13,28 +13,28 @@ void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) {
                BooleanLogic *logicop = (BooleanLogic *) parent;
                switch (logicop->op) {
                case L_AND:
-                       handleANDTrue(This, logicop, bexpr);
+                       handleANDTrue(logicop, bexpr);
                        break;
                case L_OR:
-                       replaceBooleanWithTrue(This, parent);
+                       replaceBooleanWithTrue(parent);
                        break;
                case L_NOT:
-                       replaceBooleanWithFalse(This, parent);
+                       replaceBooleanWithFalse(parent);
                        break;
                case L_XOR:
                        handleXORTrue(logicop, bexpr);
                        break;
                case L_IMPLIES:
-                       handleIMPLIESTrue(This, logicop, bexpr);
+                       handleIMPLIESTrue(logicop, bexpr);
                        break;
                }
        }
 }
 
-void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) {
-       if (This->constraints.contains(oldb)) {
-               This->constraints.remove(oldb);
-               This->constraints.add(newb);
+void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
+       if (constraints.contains(oldb)) {
+               constraints.remove(oldb);
+               constraints.add(newb);
        }
 
        uint size = oldb->parents.getSize();
@@ -62,31 +62,31 @@ void handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
        bexpr->op = L_NOT;
 }
 
-void handleXORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
        Boolean *b = bexpr->inputs.get(0);
        uint otherindex = (b == child) ? 1 : 0;
-       replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(otherindex));
+       replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
 }
 
-void handleIMPLIESTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
        Boolean *b = bexpr->inputs.get(0);
        if (b == child) {
                //Replace with other term
-               replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(1));
+               replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
        } else {
                //Statement is true...
-               replaceBooleanWithTrue(This, (Boolean *)bexpr);
+               replaceBooleanWithTrue(bexpr);
        }
 }
 
-void handleIMPLIESFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
        Boolean *b = bexpr->inputs.get(0);
        if (b == child) {
                //Statement is true...
-               replaceBooleanWithTrue(This, (Boolean *)bexpr);
+               replaceBooleanWithTrue(bexpr);
        } else {
                //Make into negation of first term
                bexpr->inputs.get(1);
@@ -94,11 +94,11 @@ void handleIMPLIESFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
        }
 }
 
-void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
 
        if (size == 1) {
-               replaceBooleanWithTrue(This, (Boolean *)bexpr);
+               replaceBooleanWithTrue(bexpr);
                return;
        }
 
@@ -110,15 +110,15 @@ void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
        }
 
        if (size == 2) {
-               replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(0));
+               replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
        }
 }
 
-void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
 
        if (size == 1) {
-               replaceBooleanWithFalse(This, (Boolean *) bexpr);
+               replaceBooleanWithFalse(bexpr);
        }
 
        for (uint i = 0; i < size; i++) {
@@ -129,14 +129,14 @@ void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
        }
 
        if (size == 2) {
-               replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(0));
+               replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
        }
 }
 
-void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr) {
-       if (This->constraints.contains(bexpr)) {
-               This->unsat=true;
-               This->constraints.remove(bexpr);
+void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
+       if (constraints.contains(bexpr)) {
+               setUnSAT();
+               constraints.remove(bexpr);
        }
        
        uint size = bexpr->parents.getSize();
@@ -145,19 +145,19 @@ void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr) {
                BooleanLogic *logicop = (BooleanLogic *) parent;
                switch (logicop->op) {
                case L_AND:
-                       replaceBooleanWithFalse(This, parent);
+                       replaceBooleanWithFalse(parent);
                        break;
                case L_OR:
-                       handleORFalse(This, logicop, bexpr);
+                       handleORFalse(logicop, bexpr);
                        break;
                case L_NOT:
-                       replaceBooleanWithTrue(This, parent);
+                       replaceBooleanWithTrue(parent);
                        break;
                case L_XOR:
-                       handleXORFalse(This, logicop, bexpr);
+                       handleXORFalse(logicop, bexpr);
                        break;
                case L_IMPLIES:
-                       handleIMPLIESFalse(This, logicop, bexpr);
+                       handleIMPLIESFalse(logicop, bexpr);
                        break;
                }
        }

diff --git a/src/AST/rewriter.h b/src/AST/rewriter.h
index 385c8fad609c716037f8180043fb488c70b1aa99..5387e4ef15ec0aa37c4a9d98a2be1c88a556bbac 100644 (file)
--- a/src/AST/rewriter.h
+++ b/src/AST/rewriter.h
@@ -2,14 +2,6 @@
 #define REWRITER_H
 #include "classlist.h"
 
-void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr);
-void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr);
-void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb);
 void handleXORTrue(BooleanLogic *bexpr, Boolean *child);
-void handleXORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleIMPLIESTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleIMPLIESFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child);
 
 #endif

diff --git a/src/ASTAnalyses/orderedge.h b/src/ASTAnalyses/orderedge.h
index bbe62004dfc3314cb29d7cc7f621070f17a7619e..7063f3486572a00d8c1559f2dc5a8e0bcfdf2cf7 100644 (file)
--- a/src/ASTAnalyses/orderedge.h
+++ b/src/ASTAnalyses/orderedge.h
@@ -21,6 +21,7 @@ class OrderEdge {
        unsigned int mustPos : 1;
        unsigned int mustNeg : 1;
        unsigned int pseudoPos : 1;
+       MEMALLOC;
 };
 
 #endif/* ORDEREDGE_H */

diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc
index 919fe1843f95e5ca9312d2fdfa01d27b3c5fc588..10adc819c91d44bb2998272129fa09d9e2f4bd0f 100644 (file)
--- a/src/ASTAnalyses/orderencoder.cc
+++ b/src/ASTAnalyses/orderencoder.cc
@@ -10,7 +10,7 @@
 #include "tunable.h"
 
 void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       HSIteratorOrderNode *iterator = graph->nodes->iterator();
+       HSIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
                if (node->status == NOTVISITED) {
@@ -65,7 +65,7 @@ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReve
 }
 
 void resetNodeInfoStatusSCC(OrderGraph *graph) {
-       HSIteratorOrderNode *iterator = graph->nodes->iterator();
+       HSIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
                iterator->next()->status = NOTVISITED;
        }
@@ -114,7 +114,7 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
                        newEdge->mustPos = true;
                        newEdge->polPos = true;
                        if (newEdge->mustNeg)
-                               This->unsat = true;
+                               This->setUnSAT();
                        srcNode->outEdges.add(newEdge);
                        sinkNode->inEdges.add(newEdge);
                }
@@ -124,7 +124,7 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
 }
 
 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
-       HSIteratorOrderNode* iterator = graph->nodes->iterator();
+       HSIteratorOrderNode* iterator = graph->getNodes();
        while(iterator->hasNext()) {
                OrderNode* node = iterator->next();
                if(isMustBeTrueNode(node)){
@@ -211,7 +211,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
 }
 
 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       HSIteratorOrderNode *iterator = graph->nodes->iterator();
+       HSIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
                if (node->status == NOTVISITED) {
@@ -256,7 +256,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                newedge->mustPos = true;
                                newedge->polPos = true;
                                if (newedge->mustNeg)
-                                       solver->unsat = true;
+                                       solver->setUnSAT();
                                srcnode->outEdges.add(newedge);
                                node->inEdges.add(newedge);
                        }
@@ -272,7 +272,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                        edge->mustPos = true;
                                        edge->polPos = true;
                                        if (edge->mustNeg)
-                                               solver->unsat = true;
+                                               solver->setUnSAT();
                                }
                        }
                        delete iterator;
@@ -287,7 +287,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                        edge->mustNeg = true;
                                        edge->polNeg = true;
                                        if (edge->mustPos)
-                                               solver->unsat = true;
+                                               solver->setUnSAT();
                                }
                        }
                        delete iterator;
@@ -318,7 +318,7 @@ void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransiti
    had one). */
 
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
-       HSIteratorOrderEdge *iterator = graph->edges->iterator();
+       HSIteratorOrderEdge *iterator = graph->getEdges();
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
                if (edge->mustPos) {
@@ -327,7 +327,7 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;
                                } else {
-                                       solver->unsat = true;
+                                       solver->setUnSAT();
                                }
                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
@@ -343,21 +343,22 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
     polarity. */
 
 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
-       HSIteratorOrderEdge *iterator = graph->edges->iterator();
+       HSIteratorOrderEdge *iterator = graph->getEdges();
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
                if (edge->mustPos) {
                        if (!edge->mustNeg) {
                                edge->polNeg = false;
                        } else
-                               solver->unsat = true;
+                               solver->setUnSAT();
 
                        OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;
                                else
-                                       solver->unsat = true;
+                                       solver->setUnSAT();
+
                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
                        }

diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h
index eba6dbdeb615cd090828f53217d77b0cece45643..8dd2e659dd3a257e89d5f59b4a10a73f109140fa 100644 (file)
--- a/src/ASTAnalyses/ordergraph.h
+++ b/src/ASTAnalyses/ordergraph.h
@@ -24,6 +24,12 @@ class OrderGraph {
        void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
        void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
        OrderEdge *getInverseOrderEdge(OrderEdge *edge);
+       Order *getOrder() {return order;}
+       HSIteratorOrderNode * getNodes() {return nodes->iterator();}
+       HSIteratorOrderEdge * getEdges() {return edges->iterator();}
+       
+       MEMALLOC;
+ private:
        HashSetOrderNode *nodes;
        HashSetOrderEdge *edges;
        Order *order;

diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h
index 95862aea200b799a092ccda7eda4a614c634ca9a..a63dd7fddf11802aae638c69e32dc6ac9ae26069 100644 (file)
--- a/src/ASTAnalyses/ordernode.h
+++ b/src/ASTAnalyses/ordernode.h
@@ -28,6 +28,7 @@ class OrderNode {
        uint sccNum;
        HashSetOrderEdge inEdges;
        HashSetOrderEdge outEdges;
+       MEMALLOC;
 };
 #endif/* ORDERNODE_H */
 

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 3e4f4abd81630ac71ee086adf547bcafbaeedb6d..947f28e3d6c70aec3dd4d9a561128d5017ef248c 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -2,7 +2,7 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
-       HSIteratorBoolean *iterator=This->constraints.iterator();
+       HSIteratorBoolean *iterator=This->getConstraints();
        while(iterator->hasNext()) {
                Boolean *boolean = iterator->next();
                updatePolarity(boolean, P_TRUE);

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 343c93a7c02adbfeb2a846750a7f0255150afd4d..4fe381ae3e1d7fbae14f4bcfdd6ce9c45c719a84 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -18,15 +18,11 @@ void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
        ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first);
        ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second);
        Set * sarray[]={elem1->set, elem2->set};
-       Predicate *predicate =new PredicateOperator(LT, sarray, 2);
+       Predicate *predicate =This->solver->createPredicateOperator(LT, sarray, 2);
        Element * parray[]={elem1, elem2};
-       BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
-       {//Adding new elements and boolean/predicate to solver regarding memory management
-               This->solver->allBooleans.push(boolean);
-               This->solver->allPredicates.push(predicate);
-               This->solver->constraints.add(boolean);
-       }
-       replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
+       Boolean * boolean=This->solver->applyPredicate(predicate, parray, 2);
+       This->solver->addConstraint(boolean);
+       This->solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }
 
 
@@ -34,11 +30,9 @@ Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
        HashSetOrderElement* eset = order->elementTable;
        OrderElement oelement(item, NULL);
        if( !eset->contains(&oelement)){
-               Set* set = new Set(order->set->type, 1, (uint64_t) order->set->getSize());
-               Element* elem = new ElementSet(set);
+               Set* set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
+               Element* elem = This->solver->getElementVar(set);
                eset->add(new OrderElement(item, elem));
-               This->solver->allElements.push(elem);
-               This->solver->allSets.push(set);
                return elem;
        } else
                return eset->get(&oelement)->elem;

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 7c8e45c88655341f852fe4eadea131d09345fb2a..4962046a0e99685ce36b40480c1e0258add83a49 100644 (file)
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -14,10 +14,11 @@
 #include "integerencoding.h"
 
 void orderAnalysis(CSolver *This) {
-       uint size = This->allOrders.getSize();
+       Vector<Order *> * orders=This->getOrders();
+       uint size = orders->getSize();
        for (uint i = 0; i < size; i++) {
-               Order *order = This->allOrders.get(i);
-               bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
+               Order *order = orders->get(i);
+               bool doDecompose=GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
                if (!doDecompose)
                        continue;
                
@@ -30,12 +31,12 @@ void orderAnalysis(CSolver *This) {
                }
 
 
-               bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
+               bool mustReachGlobal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
 
                if (mustReachGlobal)
                        reachMustAnalysis(This, graph, false);
 
-               bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
+               bool mustReachLocal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
                
                if (mustReachLocal) {
                        //This pair of analysis is also optional
@@ -46,7 +47,7 @@ void orderAnalysis(CSolver *This) {
                        }
                }
 
-               bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
+               bool mustReachPrune=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
                
                if (mustReachPrune)
                        removeMustBeTrueNodes(This, graph);
@@ -56,13 +57,16 @@ void orderAnalysis(CSolver *This) {
                decomposeOrder(This, order, graph);
                delete graph;
                
-               bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon );
+               /*
+                       OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
+
+               bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
                if(!doIntegerEncoding)
                        continue;
                uint size = order->constraints.getSize();
                for(uint i=0; i<size; i++){
                        orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
-               }
+                       }*/
 
        }
 }
@@ -79,9 +83,9 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                if (from->sccNum != to->sccNum) {
                        OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);                  
                        if (edge->polPos) {
-                               replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
+                               This->replaceBooleanWithTrue(orderconstraint);
                        } else if (edge->polNeg) {
-                               replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
+                               This->replaceBooleanWithFalse(orderconstraint);
                        } else {
                                //This case should only be possible if constraint isn't in AST
                                ASSERT(0);
@@ -92,10 +96,8 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                        if (ordervec.getSize() > from->sccNum)
                                neworder = ordervec.get(from->sccNum);
                        if (neworder == NULL) {
-                               MutableSet *set = new MutableSet(order->set->type);
-                               This->allSets.push(set);
-                               neworder = new Order(order->type, set);
-                               This->allOrders.push(neworder);
+                               MutableSet *set = This->createMutableSet(order->set->type);
+                               neworder = This->createOrder(order->type, set);
                                ordervec.setExpand(from->sccNum, neworder);
                                if (order->type == PARTIAL)
                                        partialcandidatevec.setExpand(from->sccNum, neworder);

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 0a93045073d30146195362287413d620a2460e60..91e323d4d4842996076de9054f4a0c39c788fe0b 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,7 +29,7 @@ void deleteSATEncoder(SATEncoder *This) {
 }
 
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
-       HSIteratorBoolean *iterator=csolver->constraints.iterator();
+       HSIteratorBoolean *iterator=csolver->getConstraints();
        while(iterator->hasNext()) {
                Boolean *constraint = iterator->next();
                model_print("Encoding All ...\n\n");

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 3a3260e7bddb7f3d91bb92a7d8fc2ce976525d3a..640ac1abb094535d0b4ff495f108aa912e0cf4f4 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -79,7 +79,7 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
        ASSERT(boolOrder->order->type == TOTAL);
        if (boolOrder->order->orderPairTable == NULL) {
                boolOrder->order->initializeOrderHashTable();
-               bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+               bool doOptOrderStructure=GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(This->solver, boolOrder->order->graph, true);

diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc
index ff1317a2a992c897808bcf687b0fe92bfc6e4ca5..7b8eae0d8ff16b6b7fc0521aa3af9956eb7dc90a 100644 (file)
--- a/src/Backend/sattranslator.cc
+++ b/src/Backend/sattranslator.cc
@@ -10,7 +10,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding
        uint index = 0;
        for (int i = elemEnc->numVars - 1; i >= 0; i--) {
                index = index << 1;
-               if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
+               if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
        }
        if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
@@ -22,11 +22,11 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding
        uint64_t value = 0;
        for (int i = elemEnc->numVars - 1; i >= 0; i--) {
                value = value << 1;
-               if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
+               if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
        }
        if (elemEnc->isBinaryValSigned &&
-                       This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
+                       This->getSATEncoder()->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
                //Do sign extension of negative number
                uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
                value += highbits;
@@ -38,7 +38,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding
 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint index = 0;
        for (uint i = 0; i < elemEnc->numVars; i++) {
-               if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
+               if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
        ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
@@ -48,7 +48,7 @@ uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elem
 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint i;
        for (i = 0; i < elemEnc->numVars; i++) {
-               if (!getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+               if (!getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
                        break;
                }
        }
@@ -82,7 +82,7 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
 
 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
        int index = getEdgeVar( ((BooleanVar *) boolean)->var );
-       return getValueSolver(This->satEncoder->cnf->solver, index);
+       return getValueSolver(This->getSATEncoder()->cnf->solver, index);
 }
 
 HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
@@ -91,6 +91,6 @@ HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order,
        Edge var = getOrderConstraint(order->orderPairTable, &pair);
        if (edgeIsNull(var))
                return UNORDERED;
-       return getValueCNF(This->satEncoder->cnf, var) ? FIRST : SECOND;
+       return getValueCNF(This->getSATEncoder()->cnf, var) ? FIRST : SECOND;
 }
 

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 826ba8f7bb5ecbb07fd6e141cad1c655043ceeb6..35c62e8466fccc48c7521e708a233cf96d908b1b 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -14,7 +14,7 @@
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-       HSIteratorBoolean *iterator=This->constraints.iterator();
+       HSIteratorBoolean *iterator=This->getConstraints();
        while(iterator->hasNext()) {
                Boolean *boolean = iterator->next();
                naiveEncodingConstraint(boolean);

diff --git a/src/csolver.cc b/src/csolver.cc
index 4f26bde7a295d3292482ff4451f5f985414d23ae..d4d39c01ea5503d673dbfa0b3846ddf004329aa9 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -161,7 +161,9 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
-       return new BooleanLogic(this, op, array, asize);
+       Boolean * boolean=new BooleanLogic(this, op, array, asize);
+       allBooleans.push(boolean);
+       return boolean;
 }
 
 void CSolver::addConstraint(Boolean *constraint) {

diff --git a/src/csolver.h b/src/csolver.h
index d611e1d894faeab1947668350c710655ba1d3a90..aaf3b3064f744bd7b49c7441af83da9fe8b67984 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -9,36 +9,7 @@ class CSolver {
        CSolver();
        ~CSolver();
        
-       SATEncoder *satEncoder;
-       bool unsat;
-       Tuner *tuner;
-       
-       /** This is a vector of constraints that must be satisfied. */
-       HashSetBoolean constraints;
-
-       /** This is a vector of all boolean structs that we have allocated. */
-       Vector<Boolean *> allBooleans;
-
-       /** This is a vector of all set structs that we have allocated. */
-       Vector<Set *> allSets;
-
-       /** This is a vector of all element structs that we have allocated. */
-       Vector<Element *> allElements;
-
-       /** This is a vector of all predicate structs that we have allocated. */
-       Vector<Predicate *> allPredicates;
-
-       /** This is a vector of all table structs that we have allocated. */
-       Vector<Table *> allTables;
-
-       /** This is a vector of all order structs that we have allocated. */
-       Vector<Order *> allOrders;
-
-       /** This is a vector of all function structs that we have allocated. */
-       Vector<Function *> allFunctions;
-
        /** This function creates a set containing the elements passed in the array. */
-
        Set *createSet(VarType type, uint64_t *elements, uint num);
 
        /** This function creates a set from lowrange to highrange (inclusive). */
@@ -130,7 +101,58 @@ class CSolver {
 
        HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
+       void setUnSAT() { unsat = true; }
+
+       bool isUnSAT() { return unsat; }
+
+       Vector<Order *> * getOrders() { return & allOrders;}
+
+       Tuner * getTuner() { return tuner; }
+
+       HSIteratorBoolean * getConstraints() { return constraints.iterator(); }
+
+       SATEncoder * getSATEncoder() {return satEncoder;}
+
+       void replaceBooleanWithTrue(Boolean *bexpr);
+       void replaceBooleanWithFalse(Boolean *bexpr);
+       void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+
+       
        MEMALLOC;
-};
 
+ private:
+       void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
+       void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
+       void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
+       void handleANDTrue(BooleanLogic *bexpr, Boolean *child);
+       void handleORFalse(BooleanLogic *bexpr, Boolean *child);
+
+       /** This is a vector of constraints that must be satisfied. */
+       HashSetBoolean constraints;
+
+       /** This is a vector of all boolean structs that we have allocated. */
+       Vector<Boolean *> allBooleans;
+
+       /** This is a vector of all set structs that we have allocated. */
+       Vector<Set *> allSets;
+
+       /** This is a vector of all element structs that we have allocated. */
+       Vector<Element *> allElements;
+
+       /** This is a vector of all predicate structs that we have allocated. */
+       Vector<Predicate *> allPredicates;
+
+       /** This is a vector of all table structs that we have allocated. */
+       Vector<Table *> allTables;
+
+       /** This is a vector of all order structs that we have allocated. */
+       Vector<Order *> allOrders;
+
+       /** This is a vector of all function structs that we have allocated. */
+       Vector<Function *> allFunctions;
+
+       SATEncoder *satEncoder;
+       bool unsat;
+       Tuner *tuner;
+};
 #endif