From 682109617a66ee846aa596e9661363280e517d98 Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 6 Sep 2017 11:04:06 -0700 Subject: [PATCH] Moving OrderPairTable to the resolver + hide translation complexity in OrderPair (useful for partial order) --- src/AST/order.cc | 19 +++++++-------- src/AST/order.h | 3 +-- src/Backend/orderpair.cc | 23 ++++++++++++++++- src/Backend/orderpair.h | 12 +++++++-- src/Backend/satencoder.h | 1 - src/Backend/satorderencoder.cc | 38 +++++++---------------------- src/Translator/orderpairresolver.cc | 38 +++++++++++++++-------------- src/Translator/orderpairresolver.h | 5 +++- 8 files changed, 75 insertions(+), 64 deletions(-) diff --git a/src/AST/order.cc b/src/AST/order.cc index 35bca4a..609b469 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -4,21 +4,16 @@ #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); } @@ -36,12 +31,16 @@ Order *Order::clone(CSolver *solver, CloneMap *map) { return o; } -Order::~Order() { - if (orderPairTable != NULL) { - orderPairTable->resetanddelete(); - delete orderPairTable; +HashtableOrderPair* Order::getOrderPairTable(){ + ASSERT( encoding.resolver != NULL); + if (OrderPairResolver* t = dynamic_cast(encoding.resolver)){ + return t->getOrderPairTable(); + } else { + ASSERT(0); } +} +Order::~Order() { if (graph != NULL) { delete graph; } diff --git a/src/AST/order.h b/src/AST/order.h index cc8b45e..b1f0559 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -14,16 +14,15 @@ public: ~Order(); OrderType type; Set *set; - HashtableOrderPair *orderPairTable; OrderGraph *graph; Order *clone(CSolver *solver, CloneMap *map); Vector 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; }; diff --git a/src/Backend/orderpair.cc b/src/Backend/orderpair.cc index 89913bb..abe29cc 100644 --- a/src/Backend/orderpair.cc +++ b/src/Backend/orderpair.cc @@ -1,5 +1,7 @@ #include "orderpair.h" - +#include "constraint.h" +#include "csolver.h" +#include "satencoder.h" OrderPair::OrderPair(uint64_t _first, uint64_t _second, Edge _constraint) : first(_first), @@ -12,3 +14,22 @@ OrderPair::OrderPair() : 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)); +} diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h index aad68ff..f650648 100644 --- a/src/Backend/orderpair.h +++ b/src/Backend/orderpair.h @@ -14,12 +14,20 @@ 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 */ diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 7af3e55..ef3edc6 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -64,5 +64,4 @@ private: }; void allocElementConstraintVariables(ElementEncoding *ee, uint numVars); -Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair); #endif diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index b977efa..91e2d80 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -56,7 +56,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) { if (!edgeIsNull(gvalue)) return gvalue; - HashtableOrderPair *table = order->orderPairTable; + HashtableOrderPair *table = order->getOrderPairTable(); bool negate = false; OrderPair flipped; if (pair->first < pair->second) { @@ -65,23 +65,21 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) { 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); @@ -120,24 +118,6 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *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); diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc index f0cb98d..e32a757 100644 --- a/src/Translator/orderpairresolver.cc +++ b/src/Translator/orderpairresolver.cc @@ -16,11 +16,16 @@ 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) { @@ -42,24 +47,21 @@ 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); } diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h index bf7210c..dde7378 100644 --- a/src/Translator/orderpairresolver.h +++ b/src/Translator/orderpairresolver.h @@ -15,11 +15,14 @@ class OrderPairResolver : public OrderResolver { 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 */ -- 2.34.1