From a0daa81a61273f51fdaad8a6d5aaf078387851bc Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 26 Aug 2017 18:06:04 -0700 Subject: [PATCH] Try to fix encapsulation --- src/AST/boolean.cc | 1 - src/AST/rewriter.cc | 66 ++++++++++----------- src/AST/rewriter.h | 8 --- src/ASTAnalyses/orderedge.h | 1 + src/ASTAnalyses/orderencoder.cc | 27 ++++----- src/ASTAnalyses/ordergraph.h | 6 ++ src/ASTAnalyses/ordernode.h | 1 + src/ASTAnalyses/polarityassignment.cc | 2 +- src/ASTTransform/integerencoding.cc | 18 ++---- src/ASTTransform/orderdecompose.cc | 30 +++++----- src/Backend/satencoder.cc | 2 +- src/Backend/satorderencoder.cc | 2 +- src/Backend/sattranslator.cc | 14 ++--- src/Encoders/naiveencoder.cc | 2 +- src/csolver.cc | 4 +- src/csolver.h | 82 +++++++++++++++++---------- 16 files changed, 143 insertions(+), 123 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 62f6bff..6ec1193 100644 --- 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 f659b4e..e8e9c84 100644 --- 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 385c8fa..5387e4e 100644 --- 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 bbe6200..7063f34 100644 --- 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 919fe18..10adc81 100644 --- a/src/ASTAnalyses/orderencoder.cc +++ b/src/ASTAnalyses/orderencoder.cc @@ -10,7 +10,7 @@ #include "tunable.h" void DFS(OrderGraph *graph, Vector *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 *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 *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, VectormustPos = 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, VectormustPos = true; edge->polPos = true; if (edge->mustNeg) - solver->unsat = true; + solver->setUnSAT(); } } delete iterator; @@ -287,7 +287,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectormustNeg = 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 eba6dbd..8dd2e65 100644 --- 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 95862ae..a63dd7f 100644 --- 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 3e4f4ab..947f28e 100644 --- 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 343c93a..4fe381a 100644 --- 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 7c8e45c..4962046 100644 --- 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 * 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; isatEncoder, 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 0a93045..91e323d 100644 --- 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 3a3260e..640ac1a 100644 --- 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 ff1317a..7b8eae0 100644 --- 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 826ba8f..35c62e8 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -14,7 +14,7 @@ #include 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 4f26bde..d4d39c0 100644 --- 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 d611e1d..aaf3b30 100644 --- 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 allBooleans; - - /** This is a vector of all set structs that we have allocated. */ - Vector allSets; - - /** This is a vector of all element structs that we have allocated. */ - Vector allElements; - - /** This is a vector of all predicate structs that we have allocated. */ - Vector allPredicates; - - /** This is a vector of all table structs that we have allocated. */ - Vector allTables; - - /** This is a vector of all order structs that we have allocated. */ - Vector allOrders; - - /** This is a vector of all function structs that we have allocated. */ - Vector 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 * 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 allBooleans; + + /** This is a vector of all set structs that we have allocated. */ + Vector allSets; + + /** This is a vector of all element structs that we have allocated. */ + Vector allElements; + + /** This is a vector of all predicate structs that we have allocated. */ + Vector allPredicates; + + /** This is a vector of all table structs that we have allocated. */ + Vector
allTables; + + /** This is a vector of all order structs that we have allocated. */ + Vector allOrders; + + /** This is a vector of all function structs that we have allocated. */ + Vector allFunctions; + + SATEncoder *satEncoder; + bool unsat; + Tuner *tuner; +}; #endif -- 2.34.1