#include "boolean.h"
#include "ordergraph.h"
#include "csolver.h"
+#include "orderpairresolver.h"
Order::Order(OrderType _type, Set *_set) :
type(_type),
set(_set),
- orderPairTable(NULL),
graph(NULL),
encoding(this)
{
}
-void Order::initializeOrderHashtable() {
- orderPairTable = new HashtableOrderPair();
-}
-
-
void Order::addOrderConstraint(BooleanOrder *constraint) {
constraints.push(constraint);
}
return o;
}
-Order::~Order() {
- if (orderPairTable != NULL) {
- orderPairTable->resetanddelete();
- delete orderPairTable;
+HashtableOrderPair* Order::getOrderPairTable(){
+ ASSERT( encoding.resolver != NULL);
+ if (OrderPairResolver* t = dynamic_cast<OrderPairResolver*>(encoding.resolver)){
+ return t->getOrderPairTable();
+ } else {
+ ASSERT(0);
}
+}
+Order::~Order() {
if (graph != NULL) {
delete graph;
}
~Order();
OrderType type;
Set *set;
- HashtableOrderPair *orderPairTable;
OrderGraph *graph;
Order *clone(CSolver *solver, CloneMap *map);
Vector<BooleanOrder *> constraints;
OrderEncoding encoding;
void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
- void initializeOrderHashtable();
void initializeOrderElementsHashtable();
void addOrderConstraint(BooleanOrder *constraint);
void setOrderEncodingType(OrderEncodingType type);
+ HashtableOrderPair* getOrderPairTable();
CMEMALLOC;
};
#include "orderpair.h"
-
+#include "constraint.h"
+#include "csolver.h"
+#include "satencoder.h"
OrderPair::OrderPair(uint64_t _first, uint64_t _second, Edge _constraint) :
first(_first),
second(0),
constraint(E_NULL) {
}
+
+OrderPair::~OrderPair(){
+}
+
+Edge OrderPair::getConstraint(){
+ return constraint;
+}
+
+Edge OrderPair::getNegatedConstraint(){
+ return constraintNegate(constraint);
+}
+
+bool OrderPair::getConstraintValue(CSolver* solver){
+ return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
+}
+
+bool OrderPair::getNegatedConstraintValue(CSolver* solver){
+ return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
+}
class OrderPair {
public:
- OrderPair(uint64_t first, uint64_t second, Edge constraint);
+ OrderPair(uint64_t first, uint64_t second, Edge constraint = E_NULL);
OrderPair();
+ virtual ~OrderPair();
+ virtual Edge getConstraint();
+ virtual bool getConstraintValue(CSolver* solver);
+ //for the cases that we swap first and second ... For total order is straight forward.
+ // but for partial order it has some complexity which should be hidden ... -HG
+ virtual Edge getNegatedConstraint();
+ virtual bool getNegatedConstraintValue(CSolver* solver);
uint64_t first;
uint64_t second;
- Edge constraint;
CMEMALLOC;
+protected:
+ Edge constraint;
};
#endif/* ORDERPAIR_H */
};
void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
#endif
if (!edgeIsNull(gvalue))
return gvalue;
- HashtableOrderPair *table = order->orderPairTable;
+ HashtableOrderPair *table = order->getOrderPairTable();
bool negate = false;
OrderPair flipped;
if (pair->first < pair->second) {
flipped.second = pair->first;
pair = &flipped;
}
- Edge constraint;
+ OrderPair* tmp;
if (!(table->contains(pair))) {
- constraint = getNewVarSATEncoder();
- OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
- table->put(paircopy, paircopy);
- } else
- constraint = table->get(pair)->constraint;
-
- return negate ? constraintNegate(constraint) : constraint;
+ tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
+ table->put(tmp, tmp);
+ } else {
+ tmp = table->get(pair);
+ }
+ return negate ? tmp->getNegatedConstraint() : tmp->getConstraint();
}
Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
ASSERT(boolOrder->order->type == SATC_TOTAL);
- if (boolOrder->order->orderPairTable == NULL) {
+ if (boolOrder->order->encoding.resolver == NULL) {
//This is pairwised encoding ...
boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
- boolOrder->order->initializeOrderHashtable();
bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
if (doOptOrderStructure) {
boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
}
}
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
- ASSERT(pair->first != pair->second);
- bool negate = false;
- OrderPair flipped;
- if (pair->first < pair->second) {
- negate = true;
- flipped.first = pair->second;
- flipped.second = pair->first;
- pair = &flipped;
- }
- if (!table->contains(pair)) {
- return E_NULL;
- }
- Edge constraint = table->get(pair)->constraint;
- ASSERT(!edgeIsNull(constraint));
- return negate ? constraintNegate(constraint) : constraint;
-}
-
Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
Edge loop1 = constraintOR(cnf, 3, carray);
OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
solver(_solver),
- order(_order)
+ order(_order),
+ orderPairTable(new HashtableOrderPair())
{
}
OrderPairResolver::~OrderPairResolver() {
+ if (orderPairTable != NULL) {
+ orderPairTable->resetanddelete();
+ delete orderPairTable;
+ }
}
bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
}
//Couldn't infer from graph. Should call the SAT Solver ...
- switch ( order->type) {
- case SATC_TOTAL:
- resolveTotalOrder(first, second);
- case SATC_PARTIAL:
- //TODO: Support for partial order ...
- default:
- ASSERT(0);
- }
-
-
+ return getOrderConstraintValue(first, second);
}
-
-bool OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) {
- ASSERT(order->orderPairTable != NULL);
- OrderPair pair(first, second, E_NULL);
- Edge var = getOrderConstraint(order->orderPairTable, &pair);
- if (edgeIsNull(var))
+bool OrderPairResolver::getOrderConstraintValue(uint64_t first, uint64_t second) {
+ ASSERT(first != second);
+ bool negate = false;
+ OrderPair tmp(first, second);
+ if (first < second) {
+ negate = true;
+ tmp.first = second;
+ tmp.second = first;
+ }
+ if (!orderPairTable->contains(&tmp)) {
return false;
- return getValueCNF(solver->getSATEncoder()->getCNF(), var);
+ }
+ OrderPair *pair = orderPairTable->get(&tmp);
+ return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);
}
public:
OrderPairResolver(CSolver *_solver, Order *_order);
bool resolveOrder(uint64_t first, uint64_t second);
+ HashtableOrderPair* getOrderPairTable() { return orderPairTable;}
virtual ~OrderPairResolver();
private:
CSolver *solver;
Order *order;
- bool resolveTotalOrder(uint64_t first, uint64_t second);
+ HashtableOrderPair *orderPairTable;
+
+ bool getOrderConstraintValue(uint64_t first, uint64_t second);
};
#endif/* ORDERPAIRRESOLVER_H */