continue;
}
- DecomposeOrderResolver *dor=new DecomposeOrderResolver(order);
+ DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
order->setOrderResolver(dor);
-
+
OrderGraph *graph = buildOrderGraph(order);
if (order->type == SATC_PARTIAL) {
//Required to do SCC analysis for partial order graphs. It
dor->mustOrderEdge(from->getID(), to->getID());
solver->replaceBooleanWithTrue(orderconstraint);
} else if (edge->polNeg) {
- if (currOrder->type == SATC_TOTAL)
+ if (currOrder->type == SATC_TOTAL)
dor->mustOrderEdge(to->getID(), from->getID());
solver->replaceBooleanWithFalse(orderconstraint);
} else {
int main(int numargs, char **argv) {
CSolver *solver = new CSolver();
- uint64_t elements[]={0, 1};
- Set * s = solver->createSet(1, elements, 2);
- Element * e1=solver->getElementVar(s);
- Element * e2=solver->getElementVar(s);
- Set * sarray[]={s, s};
- Predicate *p=solver->createPredicateOperator(SATC_LT, sarray, 2);
- Element *earray[]={e1, e2};
- BooleanEdge be=solver->applyPredicate(p, earray, 2);
+ uint64_t elements[] = {0, 1};
+ Set *s = solver->createSet(1, elements, 2);
+ Element *e1 = solver->getElementVar(s);
+ Element *e2 = solver->getElementVar(s);
+ Set *sarray[] = {s, s};
+ Predicate *p = solver->createPredicateOperator(SATC_LT, sarray, 2);
+ Element *earray[] = {e1, e2};
+ BooleanEdge be = solver->applyPredicate(p, earray, 2);
solver->addConstraint(be);
if (solver->solve() == 1) {
#include "ordernode.h"
#include "ordergraph.h"
-DecomposeOrderResolver::DecomposeOrderResolver(Order * _order) :
+DecomposeOrderResolver::DecomposeOrderResolver(Order *_order) :
graph(NULL),
order(_order)
{
void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
DOREdge edge(first, second, 0, first, second);
if (!edges.contains(&edge)) {
- DOREdge *newedge=new DOREdge(first, second, 0, first, second);
+ DOREdge *newedge = new DOREdge(first, second, 0, first, second);
edges.add(newedge);
}
}
void DecomposeOrderResolver::remapEdge(uint64_t first, uint64_t second, uint64_t newfirst, uint64_t newsecond) {
DOREdge edge(first, second, 0, first, second);
- DOREdge *oldedge=edges.get(&edge);
+ DOREdge *oldedge = edges.get(&edge);
if (oldedge != NULL) {
edges.remove(oldedge);
- oldedge->newfirst=newfirst;
- oldedge->newsecond=newsecond;
+ oldedge->newfirst = newfirst;
+ oldedge->newsecond = newsecond;
edges.add(oldedge);
} else {
- DOREdge *newedge=new DOREdge(first, second, 0, newfirst, newsecond);
+ DOREdge *newedge = new DOREdge(first, second, 0, newfirst, newsecond);
edges.add(newedge);
}
}
void DecomposeOrderResolver::setEdgeOrder(uint64_t first, uint64_t second, uint sccNum) {
DOREdge edge(first, second, 0, first, second);
- DOREdge *oldedge=edges.get(&edge);
+ DOREdge *oldedge = edges.get(&edge);
if (oldedge != NULL) {
- oldedge->orderindex=sccNum;
+ oldedge->orderindex = sccNum;
} else {
- DOREdge *newedge=new DOREdge(first, second, sccNum, first, second);
+ DOREdge *newedge = new DOREdge(first, second, sccNum, first, second);
edges.add(newedge);
}
}
orders.setExpand(sccNum, neworder);
}
-Order * DecomposeOrderResolver::getOrder(uint sccNum) {
+Order *DecomposeOrderResolver::getOrder(uint sccNum) {
Order *neworder = NULL;
if (orders.getSize() > sccNum)
neworder = orders.get(sccNum);
void DecomposeOrderResolver::buildGraph() {
graph = new OrderGraph(order);
SetIteratorDOREdge *iterator = edges.iterator();
- while(iterator->hasNext()) {
- DOREdge * doredge = iterator->next();
+ while (iterator->hasNext()) {
+ DOREdge *doredge = iterator->next();
if (doredge->orderindex == 0) {
graph->addEdge(doredge->origfirst, doredge->origsecond);
} else {
- Order * suborder = orders.get(doredge->orderindex);
+ Order *suborder = orders.get(doredge->orderindex);
bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
if (isEdge)
graph->addEdge(doredge->origfirst, doredge->origsecond);
#include "orderresolver.h"
class DOREdge {
- public:
- DOREdge(uint64_t _origfirst, uint64_t _origsecond, uint _orderindex, uint64_t _newfirst, uint64_t _newsecond) :
- origfirst(_origfirst),
+public:
+ DOREdge(uint64_t _origfirst, uint64_t _origsecond, uint _orderindex, uint64_t _newfirst, uint64_t _newsecond) :
+ origfirst(_origfirst),
origsecond(_origsecond),
orderindex(_orderindex),
newfirst(_newfirst),
newsecond(_newsecond) {
- }
+ }
uint64_t origfirst;
uint64_t origsecond;
uint orderindex;
void remapEdge(uint64_t oldfirst, uint64_t oldsecond, uint64_t newfirst, uint64_t newsecond);
void setEdgeOrder(uint64_t first, uint64_t second, uint sccNum);
void setOrder(uint sccNum, Order *order);
- Order * getOrder(uint sccNum);
+ Order *getOrder(uint sccNum);
CMEMALLOC;
-
- private:
+
+private:
bool resolvePartialOrder(OrderNode *first, OrderNode *second);
void buildGraph();
OrderGraph *graph;