#include "csolver.h"
-DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver, Order* _order)
- :Transform(_solver),
- order(_order)
+DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver)
+ :Transform(_solver)
{
}
}
bool DecomposeOrderTransform::canExecuteTransform(){
- return canExecutePass(solver, order->type, DECOMPOSEORDER, &onoff);
+ return canExecutePass(solver, currOrder->type, DECOMPOSEORDER, &onoff);
}
void DecomposeOrderTransform::doTransform(){
Vector<Order *> ordervec;
Vector<Order *> partialcandidatevec;
- uint size = order->constraints.getSize();
+ uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
- BooleanOrder *orderconstraint = order->constraints.get(i);
- OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
- OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
+ BooleanOrder *orderconstraint = currOrder->constraints.get(i);
+ OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
+ OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
if (from->sccNum != to->sccNum) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polPos) {
solver->replaceBooleanWithTrue(orderconstraint);
} else if (edge->polNeg) {
if (ordervec.getSize() > from->sccNum)
neworder = ordervec.get(from->sccNum);
if (neworder == NULL) {
- MutableSet *set = solver->createMutableSet(order->set->getType());
- neworder = solver->createOrder(order->type, set);
+ MutableSet *set = solver->createMutableSet(currOrder->set->getType());
+ neworder = solver->createOrder(currOrder->type, set);
ordervec.setExpand(from->sccNum, neworder);
- if (order->type == SATC_PARTIAL)
+ if (currOrder->type == SATC_PARTIAL)
partialcandidatevec.setExpand(from->sccNum, neworder);
else
partialcandidatevec.setExpand(from->sccNum, NULL);
to->status = SATC_ADDEDTOSET;
((MutableSet *)neworder->set)->addElementMSet(to->id);
}
- if (order->type == SATC_PARTIAL) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ if (currOrder->type == SATC_PARTIAL) {
+ OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polNeg)
partialcandidatevec.setExpand(from->sccNum, NULL);
}
Transformer::Transformer(CSolver *_solver):
integerEncoding(new IntegerEncodingTransform(_solver)),
+ decomposeOrder(new DecomposeOrderTransform(_solver)),
solver(_solver)
{
}
Transformer::~Transformer(){
delete integerEncoding;
+ delete decomposeOrder;
}
void Transformer::orderAnalysis() {
uint size = orders->getSize();
for (uint i = 0; i < size; i++) {
Order *order = orders->get(i);
- DecomposeOrderTransform* decompose = new DecomposeOrderTransform(solver, order);
- if (!decompose->canExecuteTransform()){
- delete decompose;
+ decomposeOrder->setCurrentOrder(order);
+ if (!decomposeOrder->canExecuteTransform()){
continue;
}
//This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
- decompose->setOrderGraph(graph);
- decompose->doTransform();
- delete decompose;
+ decomposeOrder->setOrderGraph(graph);
+ decomposeOrder->doTransform();
delete graph;
integerEncoding->setCurrentOrder(order);