#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) {
}
void resetNodeInfoStatusSCC(OrderGraph *graph) {
- HSIteratorOrderNode *iterator = graph->nodes->iterator();
+ HSIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
iterator->next()->status = NOTVISITED;
}
newEdge->mustPos = true;
newEdge->polPos = true;
if (newEdge->mustNeg)
- This->unsat = true;
+ This->setUnSAT();
srcNode->outEdges.add(newEdge);
sinkNode->inEdges.add(newEdge);
}
}
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)){
}
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) {
newedge->mustPos = true;
newedge->polPos = true;
if (newedge->mustNeg)
- solver->unsat = true;
+ solver->setUnSAT();
srcnode->outEdges.add(newedge);
node->inEdges.add(newedge);
}
edge->mustPos = true;
edge->polPos = true;
if (edge->mustNeg)
- solver->unsat = true;
+ solver->setUnSAT();
}
}
delete iterator;
edge->mustNeg = true;
edge->polNeg = true;
if (edge->mustPos)
- solver->unsat = true;
+ solver->setUnSAT();
}
}
delete iterator;
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) {
if (!invEdge->mustPos) {
invEdge->polPos = false;
} else {
- solver->unsat = true;
+ solver->setUnSAT();
}
invEdge->mustNeg = true;
invEdge->polNeg = true;
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;
}