From efba7cfdb7c83f193689663a79873df81effabe4 Mon Sep 17 00:00:00 2001 From: Hamed Date: Sun, 27 Aug 2017 15:14:51 -0700 Subject: [PATCH] Adding Transform object ... applying Brian's comments --- src/AST/order.cc | 8 +--- src/AST/order.h | 1 - src/ASTTransform/integerencoding.cc | 40 -------------------- src/ASTTransform/integerencoding.h | 24 ------------ src/ASTTransform/integerencodingrecord.cc | 33 +++++++++++++++++ src/ASTTransform/integerencodingrecord.h | 27 ++++++++++++++ src/ASTTransform/orderdecompose.cc | 23 ++++++------ src/ASTTransform/transform.cc | 45 +++++++++++++++++++++++ src/ASTTransform/transform.h | 26 +++++++++++++ src/Collections/structs.cc | 8 ++++ src/Collections/structs.h | 5 ++- src/classlist.h | 2 + 12 files changed, 158 insertions(+), 84 deletions(-) delete mode 100644 src/ASTTransform/integerencoding.cc delete mode 100644 src/ASTTransform/integerencoding.h create mode 100644 src/ASTTransform/integerencodingrecord.cc create mode 100644 src/ASTTransform/integerencodingrecord.h create mode 100644 src/ASTTransform/transform.cc create mode 100644 src/ASTTransform/transform.h diff --git a/src/AST/order.cc b/src/AST/order.cc index debd37c..bf2e566 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -8,7 +8,6 @@ Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTable(NULL), - elementTable(NULL), graph(NULL), order(this) { @@ -18,9 +17,6 @@ void Order::initializeOrderHashTable() { orderPairTable = new HashTableOrderPair(); } -void Order::initializeOrderElementsHashTable() { - elementTable = new HashSetOrderElement(); -} void Order::addOrderConstraint(BooleanOrder *constraint) { constraints.push(constraint); @@ -35,9 +31,7 @@ Order::~Order() { orderPairTable->resetanddelete(); delete orderPairTable; } - if (elementTable != NULL) { - delete elementTable; - } + if (graph != NULL) { delete graph; } diff --git a/src/AST/order.h b/src/AST/order.h index 8d21240..d60208e 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -15,7 +15,6 @@ public: OrderType type; Set *set; HashTableOrderPair *orderPairTable; - HashSetOrderElement *elementTable; OrderGraph *graph; Vector constraints; OrderEncoding order; diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc deleted file mode 100644 index 0a415b9..0000000 --- a/src/ASTTransform/integerencoding.cc +++ /dev/null @@ -1,40 +0,0 @@ -#include "integerencoding.h" -#include "orderelement.h" -#include "order.h" -#include "satencoder.h" -#include "csolver.h" -#include "predicate.h" -#include "element.h" -#include "rewriter.h" -#include "set.h" - - -void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { - Order *order = boolOrder->order; - if (order->elementTable == NULL) { - order->initializeOrderElementsHashTable(); - } - //getting two elements and using LT predicate ... - ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->first); - ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->second); - Set *sarray[] = {elem1->set, elem2->set}; - Predicate *predicate = This->solver->createPredicateOperator(LT, sarray, 2); - Element *parray[] = {elem1, elem2}; - Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2); - This->solver->addConstraint(boolean); - This->solver->replaceBooleanWithBoolean(boolOrder, boolean); -} - - -Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) { - HashSetOrderElement *eset = order->elementTable; - OrderElement oelement(item, NULL); - if ( !eset->contains(&oelement)) { - Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize()); - Element *elem = This->solver->getElementVar(set); - eset->add(new OrderElement(item, elem)); - return elem; - } else - return eset->get(&oelement)->elem; -} - diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h deleted file mode 100644 index 15fbdd7..0000000 --- a/src/ASTTransform/integerencoding.h +++ /dev/null @@ -1,24 +0,0 @@ -/* - * To change this license header, choose License Headers in Project Properties. - * To change this template file, choose Tools | Templates - * and open the template in the editor. - */ - -/* - * File: integerencoding.h - * Author: hamed - * - * Created on August 24, 2017, 5:31 PM - */ - -#ifndef INTEGERENCODING_H -#define INTEGERENCODING_H -#include "classlist.h" -#include "structs.h" - -Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item); -void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder); - - -#endif/* INTEGERENCODING_H */ - diff --git a/src/ASTTransform/integerencodingrecord.cc b/src/ASTTransform/integerencodingrecord.cc new file mode 100644 index 0000000..ee3a427 --- /dev/null +++ b/src/ASTTransform/integerencodingrecord.cc @@ -0,0 +1,33 @@ +/* + * File: integerencodingrecord.cpp + * Author: hamed + * + * Created on August 26, 2017, 6:19 PM + */ + +#include "integerencodingrecord.h" +#include "csolver.h" +#include "orderelement.h" + +IntegerEncodingRecord::IntegerEncodingRecord(Set* _set): + set(_set) +{ + elementTable = new HashSetOrderElement(); +} + +IntegerEncodingRecord::~IntegerEncodingRecord(){ + if (elementTable != NULL) { + delete elementTable; + } +} + +Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item) { + OrderElement oelement(item, NULL); + if ( !elementTable->contains(&oelement)) { + Element *elem = This->getElementVar(set); + elementTable->add(new OrderElement(item, elem)); + return elem; + } else + return elementTable->get(&oelement)->elem; +} + diff --git a/src/ASTTransform/integerencodingrecord.h b/src/ASTTransform/integerencodingrecord.h new file mode 100644 index 0000000..3069da5 --- /dev/null +++ b/src/ASTTransform/integerencodingrecord.h @@ -0,0 +1,27 @@ +/* + * File: integerencodingrecord.h + * Author: hamed + * + * Created on August 26, 2017, 6:19 PM + */ + +#ifndef INTEGERENCODINGRECORD_H +#define INTEGERENCODINGRECORD_H +#include "classlist.h" +#include "structs.h" +#include "mymemory.h" + +class IntegerEncodingRecord { +public: + Set* set; + IntegerEncodingRecord(Set* set); + ~IntegerEncodingRecord(); + Element* getOrderIntegerElement(CSolver *This, uint64_t item); + MEMALLOC; + +private: + HashSetOrderElement *elementTable; +}; + +#endif /* INTEGERENCODINGRECORD_H */ + diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc index 18602cc..ccac62b 100644 --- a/src/ASTTransform/orderdecompose.cc +++ b/src/ASTTransform/orderdecompose.cc @@ -11,9 +11,11 @@ #include "csolver.h" #include "orderencoder.h" #include "tunable.h" -#include "integerencoding.h" +#include "transform.h" +#include "element.h" void orderAnalysis(CSolver *This) { + Transform* transform = new Transform(); Vector *orders = This->getOrders(); uint size = orders->getSize(); for (uint i = 0; i < size; i++) { @@ -57,18 +59,17 @@ void orderAnalysis(CSolver *This) { decomposeOrder(This, order, graph); delete graph; - /* - OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need... - - bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon ); - if(!doIntegerEncoding) - continue; - uint size = order->constraints.getSize(); - for(uint i=0; isatEncoder, order->constraints.get(i)); - }*/ + + bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon ); + if(!doIntegerEncoding) + continue; + uint size = order->constraints.getSize(); + for(uint i=0; iorderIntegerEncodingSATEncoder(This, order->constraints.get(i)); + } } + delete transform; } void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { diff --git a/src/ASTTransform/transform.cc b/src/ASTTransform/transform.cc new file mode 100644 index 0000000..312b450 --- /dev/null +++ b/src/ASTTransform/transform.cc @@ -0,0 +1,45 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: transform.cc + * Author: hamed + * + * Created on August 26, 2017, 5:14 PM + */ + +#include "transform.h" +#include "set.h" +#include "order.h" +#include "satencoder.h" +#include "csolver.h" +#include "integerencodingrecord.h" + +Transform::Transform() { + orderIntegerEncoding = new HashTableOrderIntegerEncoding; +} + +void Transform:: orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder) { + Order *order = boolOrder->order; + if (!orderIntegerEncoding->contains(order)) { + orderIntegerEncoding->put(order, new IntegerEncodingRecord( + This->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1))); + } + IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order); + //getting two elements and using LT predicate ... + Element *elem1 = ierec->getOrderIntegerElement(This, boolOrder->first); + Element *elem2 = ierec->getOrderIntegerElement(This, boolOrder->second); + Set *sarray[] = {ierec->set, ierec->set}; + Predicate *predicate = This->createPredicateOperator(LT, sarray, 2); + Element *parray[] = {elem1, elem2}; + Boolean *boolean = This->applyPredicate(predicate, parray, 2); + This->addConstraint(boolean); + This->replaceBooleanWithBoolean(boolOrder, boolean); +} + +Transform::~Transform(){ + delete orderIntegerEncoding; +} diff --git a/src/ASTTransform/transform.h b/src/ASTTransform/transform.h new file mode 100644 index 0000000..44b431a --- /dev/null +++ b/src/ASTTransform/transform.h @@ -0,0 +1,26 @@ +/* + * File: transform.h + * Author: hamed + * + * Created on August 26, 2017, 5:13 PM + */ + +#ifndef TRANSFORM_H +#define TRANSFORM_H + +#include "classlist.h" +#include "mymemory.h" +#include "structs.h" + +class Transform { +public: + Transform(); + ~Transform(); + void orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder); + MEMALLOC; +private: + HashTableOrderIntegerEncoding* orderIntegerEncoding; +}; + +#endif /* TRANSFORM_H */ + diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc index 7239a7e..660005c 100644 --- a/src/Collections/structs.cc +++ b/src/Collections/structs.cc @@ -57,3 +57,11 @@ bool order_pair_equals(OrderPair *key1, OrderPair *key2) { return key1->first == key2->first && key1->second == key2->second; } +unsigned int order_hash_function(Order *This) { + return (uint) This; +} + +bool order_pair_equals(Order *key1, Order *key2) { + return key1==key2; +} + diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 28d290f..ef3beb5 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -16,6 +16,9 @@ unsigned int order_element_hash_function(OrderElement *This); bool order_element_equals(OrderElement *key1, OrderElement *key2); unsigned int order_pair_hash_function(OrderPair *This); bool order_pair_equals(OrderPair *key1, OrderPair *key2); +unsigned int order_hash_function(Order *This); +bool order_pair_equals(Order *key1, Order *key2); + typedef HashSet HashSetBoolean; typedef HashSet HashSetTableEntry; @@ -24,7 +27,7 @@ typedef HashSet HashSetOrderElement; typedef HashTable HashTableNodeToNodeSet; typedef HashTable HashTableOrderPair; - +typedef HashTable HashTableOrderIntegerEncoding; typedef HSIterator HSIteratorTableEntry; typedef HSIterator HSIteratorBoolean; typedef HSIterator HSIteratorOrderEdge; diff --git a/src/classlist.h b/src/classlist.h index cef1e1f..4b19649 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -43,6 +43,8 @@ class Order; class OrderPair; class OrderElement; +class IntegerEncodingRecord; +class Transform; class ElementEncoding; class FunctionEncoding; -- 2.34.1