#include "orderedge.h"
#include "ordergraph.h"
-OrderEdge *allocOrderEdge(OrderNode *source, OrderNode *sink) {
- OrderEdge *This = (OrderEdge *) ourmalloc(sizeof(OrderEdge));
- This->source = source;
- This->sink = sink;
- This->polPos = false;
- This->polNeg = false;
- This->mustPos = false;
- This->mustNeg = false;
- This->pseudoPos = false;
- return This;
+OrderEdge::OrderEdge(OrderNode *_source, OrderNode *_sink) {
+ source = _source;
+ sink = _sink;
+ polPos = false;
+ polNeg = false;
+ mustPos = false;
+ mustNeg = false;
+ pseudoPos = false;
}
-
-void deleteOrderEdge(OrderEdge *This) {
- ourfree(This);
-}
-
#include "classlist.h"
#include "mymemory.h"
-struct OrderEdge {
+class OrderEdge {
+ public:
+ OrderEdge(OrderNode *begin, OrderNode *end);
+
OrderNode *source;
OrderNode *sink;
unsigned int polPos : 1;
unsigned int pseudoPos : 1;
};
-OrderEdge *allocOrderEdge(OrderNode *begin, OrderNode *end);
-void deleteOrderEdge(OrderEdge *This);
-void setPseudoPos(OrderGraph *graph, OrderEdge *edge);
-void setMustPos(OrderGraph *graph, OrderEdge *edge);
-void setMustNeg(OrderGraph *graph, OrderEdge *edge);
-void setPolPos(OrderGraph *graph, OrderEdge *edge);
-void setPolNeg(OrderGraph *graph, OrderEdge *edge);
-
#endif/* ORDEREDGE_H */
}
void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
- HSIteratorOrderEdge *iterator = isReverse ? node->inEdges->iterator() : node->outEdges->iterator();
+ HSIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
if (mustvisit) {
}
bool isMustBeTrueNode(OrderNode* node){
- HSIteratorOrderEdge* iterator = node->inEdges->iterator();
+ HSIteratorOrderEdge* iterator = node->inEdges.iterator();
while(iterator->hasNext()){
OrderEdge* edge = iterator->next();
if(!edge->mustPos)
return false;
}
delete iterator;
- iterator = node->outEdges->iterator();
+ iterator = node->outEdges.iterator();
while(iterator->hasNext()){
OrderEdge* edge = iterator->next();
if(!edge->mustPos)
}
void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
- HSIteratorOrderEdge* iterin = node->inEdges->iterator();
+ HSIteratorOrderEdge* iterin = node->inEdges.iterator();
while(iterin->hasNext()){
OrderEdge* inEdge = iterin->next();
OrderNode* srcNode = inEdge->source;
- srcNode->outEdges->remove(inEdge);
- HSIteratorOrderEdge* iterout = node->outEdges->iterator();
+ srcNode->outEdges.remove(inEdge);
+ HSIteratorOrderEdge* iterout = node->outEdges.iterator();
while(iterout->hasNext()){
OrderEdge* outEdge = iterout->next();
OrderNode* sinkNode = outEdge->sink;
- sinkNode->inEdges->remove(outEdge);
+ sinkNode->inEdges.remove(outEdge);
//Adding new edge to new sink and src nodes ...
OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
newEdge->mustPos = true;
newEdge->polPos = true;
if (newEdge->mustNeg)
This->unsat = true;
- srcNode->outEdges->add(newEdge);
- sinkNode->inEdges->add(newEdge);
+ srcNode->outEdges.add(newEdge);
+ sinkNode->inEdges.add(newEdge);
}
delete iterout;
}
for (uint j = 0; j < rSize; j++) {
OrderNode *rnode = sccNodes.get(j);
//Compute source sets
- HSIteratorOrderEdge *iterator = rnode->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = rnode->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
table->put(rnode, set);
//Use source sets to compute pseudoPos edges
- HSIteratorOrderEdge *iterator = node->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
{
//Compute source sets
- HSIteratorOrderEdge *iterator = node->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
newedge->polPos = true;
if (newedge->mustNeg)
solver->unsat = true;
- srcnode->outEdges->add(newedge);
- node->inEdges->add(newedge);
+ srcnode->outEdges.add(newedge);
+ node->inEdges.add(newedge);
}
delete srciterator;
}
{
//Use source sets to compute mustPos edges
- HSIteratorOrderEdge *iterator =node->inEdges->iterator();
+ HSIteratorOrderEdge *iterator =node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
}
{
//Use source sets to compute mustNeg for edges that would introduce cycle if true
- HSIteratorOrderEdge *iterator = node->outEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->outEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *child = edge->sink;
if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
_1to2->mustPos = true;
_1to2->polPos = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
if (constr->polarity == P_TRUE)
break;
}
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_2to1->mustPos = true;
_2to1->polPos = true;
- addNewOutgoingEdge(node2, _2to1);
- addNewIncomingEdge(node1, _2to1);
+ node2->addNewOutgoingEdge(_2to1);
+ node1->addNewIncomingEdge(_2to1);
} else {
OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_1to2->mustNeg = true;
_1to2->polNeg = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
}
break;
}
OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
_1to2->mustPos = true;
_1to2->polPos = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
if (constr->boolVal == BV_MUSTBETRUE)
break;
}
OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
_2to1->mustPos = true;
_2to1->polPos = true;
- addNewOutgoingEdge(node2, _2to1);
- addNewIncomingEdge(node1, _2to1);
+ node2->addNewOutgoingEdge(_2to1);
+ node1->addNewIncomingEdge(_2to1);
} else {
OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
_1to2->mustNeg = true;
_1to2->polNeg = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
}
break;
}
}
OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
- OrderNode *node = allocOrderNode(id);
+ OrderNode *node = new OrderNode(id);
OrderNode *tmp = graph->nodes->get(node);
if ( tmp != NULL) {
- deleteOrderNode(node);
+ delete node;
node = tmp;
} else {
graph->nodes->add(node);
}
OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
- OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
+ OrderNode node(id);
OrderNode *tmp = graph->nodes->get(&node);
return tmp;
}
OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
- OrderEdge *edge = allocOrderEdge(begin, end);
+ OrderEdge *edge = new OrderEdge(begin, end);
OrderEdge *tmp = graph->edges->get(edge);
if ( tmp != NULL ) {
- deleteOrderEdge(edge);
+ delete edge;
edge = tmp;
} else {
graph->edges->add(edge);
}
OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
- OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
+ OrderEdge edge(begin, end);
OrderEdge *tmp = graph->edges->get(&edge);
return tmp;
}
OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
- OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
+ OrderEdge inverseedge(edge->sink, edge->source);
OrderEdge *tmp = graph->edges->get(&inverseedge);
return tmp;
}
HSIteratorOrderNode *iterator = graph->nodes->iterator();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
- deleteOrderNode(node);
+ delete node;
}
delete iterator;
HSIteratorOrderEdge *eiterator = graph->edges->iterator();
while (eiterator->hasNext()) {
OrderEdge *edge = eiterator->next();
- deleteOrderEdge(edge);
+ delete edge;
}
delete eiterator;
delete graph->nodes;
#include "ordernode.h"
#include "orderedge.h"
-OrderNode *allocOrderNode(uint64_t id) {
- OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode));
- This->id = id;
- This->inEdges = new HashSetOrderEdge();
- This->outEdges = new HashSetOrderEdge();
- This->status = NOTVISITED;
- This->sccNum = 0;
- return This;
+OrderNode::OrderNode(uint64_t _id) :
+ id(_id),
+ status(NOTVISITED),
+ sccNum(0),
+ inEdges(),
+ outEdges() {
}
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge) {
- node->inEdges->add(edge);
+void OrderNode::addNewIncomingEdge(OrderEdge *edge) {
+ inEdges.add(edge);
}
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge) {
- node->outEdges->add(edge);
-}
-
-void deleteOrderNode(OrderNode *node) {
- delete node->inEdges;
- delete node->outEdges;
- ourfree(node);
+void OrderNode::addNewOutgoingEdge(OrderEdge *edge) {
+ outEdges.add(edge);
}
enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
typedef enum NodeStatus NodeStatus;
-struct OrderNode {
+class OrderNode {
+ public:
+ OrderNode(uint64_t id);
+ void addNewIncomingEdge(OrderEdge *edge);
+ void addNewOutgoingEdge(OrderEdge *edge);
+
uint64_t id;
- HashSetOrderEdge * inEdges;
- HashSetOrderEdge * outEdges;
NodeStatus status;
uint sccNum;
+ HashSetOrderEdge inEdges;
+ HashSetOrderEdge outEdges;
};
-
-OrderNode *allocOrderNode(uint64_t id);
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge);
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge);
-void deleteOrderNode(OrderNode *node);
-
#endif/* ORDERNODE_H */
Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
HashSetOrderElement* eset = order->elementTable;
- OrderElement oelement ={item, NULL};
+ 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);
- eset->add(allocOrderElement(item, elem));
+ eset->add(new OrderElement(item, elem));
This->solver->allElements.push(elem);
This->solver->allSets.push(set);
return elem;
decomposeOrder(This, order, graph);
deleteOrderGraph(graph);
- bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
+ bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon );
if(!doIntegerEncoding)
continue;
uint size = order->constraints.getSize();
#include "orderelement.h"
-OrderElement *allocOrderElement(uint64_t item, Element* elem) {
- OrderElement *This = (OrderElement *) ourmalloc(sizeof(OrderElement));
- This->elem = elem;
- This->item = item;
- return This;
-}
-
-void deleteOrderElement(OrderElement *pair) {
- ourfree(pair);
+OrderElement::OrderElement(uint64_t _item, Element* _elem) {
+ elem = _elem;
+ item = _item;
}
#include "mymemory.h"
#include "constraint.h"
-struct OrderElement {
+class OrderElement {
+ public:
+ OrderElement(uint64_t item, Element* elem);
uint64_t item;
Element* elem;
+ MEMALLOC;
};
-OrderElement *allocOrderElement(uint64_t item, Element* elem);
-void deleteOrderElement(OrderElement *pair);
#endif/* ORDERELEMENT_H */
if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
index |= 1;
}
- model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, elemEnc->isinUseElement(index));
- ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
+ if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
+ model_print("WARNING: Element has undefined value!\n");
return elemEnc->encodingArray[index];
}
-struct OrderElement;
-typedef struct OrderElement OrderElement;
+class OrderElement;
class ElementEncoding;
class FunctionEncoding;
struct OrderGraph;
typedef struct OrderGraph OrderGraph;
-struct OrderNode;
-typedef struct OrderNode OrderNode;
-
-struct OrderEdge;
-typedef struct OrderEdge OrderEdge;
+class OrderNode;
+class OrderEdge;
struct OrderEncoder;
typedef struct OrderEncoder OrderEncoder;