Adding Transform object ... applying Brian's comments

diff --git a/src/AST/order.cc b/src/AST/order.cc
index debd37cf69defe4107d34c8091a69c1f9d214a16..bf2e5662fb67e907e5d46d9e73a532f3a8bccdff 100644 (file)
--- 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 8d2124073968ce7a8c4cea3c09df018671b1fd2f..d60208ebc14c1360473cdfaf42142c3071f1c55c 100644 (file)
--- 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<BooleanOrder *> constraints;
        OrderEncoding order;

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
deleted file mode 100644 (file)
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 (file)
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 (file)
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 (file)
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 18602cc864f3c177f925781d057ce760ee9929b8..ccac62b00238662c5a3c564f159faefcb2423e1a 100644 (file)
--- 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<Order *> *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; i<size; i++){
-                  orderIntegerEncodingSATEncoder(This->satEncoder, 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; i<size; i++){
+                       transform->orderIntegerEncodingSATEncoder(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 (file)
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 (file)
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 7239a7ea4757d87f630ce4f393754606478d789d..660005c787f58497e49de41d0bd0389aaf22a353 100644 (file)
--- 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 28d290f0303b9b460ec58fa9a94090ba490c632b..ef3beb55d0f1401ba2695e34b12f594bf858118b 100644 (file)
--- 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<Boolean *, uintptr_t, 4> HashSetBoolean;
 typedef HashSet<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashSetTableEntry;
@@ -24,7 +27,7 @@ typedef HashSet<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_
 typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
 typedef HashTable<OrderNode *, HashSetOrderNode *, uintptr_t, 4> HashTableNodeToNodeSet;
 typedef HashTable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashTableOrderPair;
-
+typedef HashTable<Order* , IntegerEncodingRecord*, uintptr_t, 4, order_hash_function, order_pair_equals> HashTableOrderIntegerEncoding; 
 typedef HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
 typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
 typedef HSIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HSIteratorOrderEdge;

diff --git a/src/classlist.h b/src/classlist.h
index cef1e1fe6bcc8fd4f46b50f73c71a0a9f945754a..4b1964997dc72bd62c22d1c0bdd0bf2653932847 100644 (file)
--- 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;