Adding support for Integer Encoding ...

diff --git a/src/AST/order.c b/src/AST/order.c
index b5840da5e3c9be6dd173bc5080ad5a1be4da3ac2..92bb55795004b90c97f0e2fd967e7ee9533494f0 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -11,6 +11,7 @@ Order *allocOrder(OrderType type, Set *set) {
        This->type = type;
        initOrderEncoding(&This->order, This);
        This->orderPairTable = NULL;
+       This->elementTable = NULL;
        This->graph = NULL;
        return This;
 }
@@ -19,6 +20,10 @@ void initializeOrderHashTable(Order *This) {
        This->orderPairTable = allocHashTableOrderPair(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
 }
 
+void initializeOrderElementsHashTable(Order *This){
+       This->elementTable = allocHashSetOrderElement(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+}
+
 void addOrderConstraint(Order *This, BooleanOrder *constraint) {
        pushVectorBooleanOrder( &This->constraints, constraint);
 }
@@ -34,6 +39,9 @@ void deleteOrder(Order *This) {
                resetAndDeleteHashTableOrderPair(This->orderPairTable);
                deleteHashTableOrderPair(This->orderPairTable);
        }
+       if(This->elementTable != NULL){
+               deleteHashSetOrderElement(This->elementTable);
+       }
        if (This->graph != NULL) {
                deleteOrderGraph(This->graph);
        }

diff --git a/src/AST/order.h b/src/AST/order.h
index c5a03a84f455b31e923867e23e1f8c4b70631cc5..a4a7621d96bb794a6e5a90f035ce2b674fe0a6d5 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -11,6 +11,7 @@ struct Order {
        OrderType type;
        Set *set;
        HashTableOrderPair *orderPairTable;
+       HashSetOrderElement* elementTable;
        OrderGraph *graph;
        VectorBooleanOrder constraints;
        OrderEncoding order;
@@ -18,6 +19,7 @@ struct Order {
 
 Order *allocOrder(OrderType type, Set *set);
 void initializeOrderHashTable(Order *This);
+void initializeOrderElementsHashTable(Order *This);
 void addOrderConstraint(Order *This, BooleanOrder *constraint);
 void setOrderEncodingType(Order *This, OrderEncodingType type);
 void deleteOrder(Order *This);

diff --git a/src/Backend/orderelement.c b/src/Backend/orderelement.c
new file mode 100644 (file)
index 0000000..1355011
--- /dev/null
+++ b/src/Backend/orderelement.c
@@ -0,0 +1,13 @@
+#include "orderelement.h"
+
+
+OrderElement *allocOrderElement(uint64_t item, Element* elem) {
+       OrderElement *This = (OrderElement *) ourmalloc(sizeof(OrderElement));
+       This->elem = elem;
+       This->item = item;
+       return This;
+}
+
+void deleteOrderElement(OrderElement *pair) {
+       ourfree(pair);
+}

diff --git a/src/Backend/orderelement.h b/src/Backend/orderelement.h
new file mode 100644 (file)
index 0000000..6bdcbc6
--- /dev/null
+++ b/src/Backend/orderelement.h
@@ -0,0 +1,24 @@
+/*
+ * File:   orderelement.h
+ * Author: hamed
+ *
+ * Created on July 1, 2017, 4:22 PM
+ */
+
+#ifndef ORDERELEMENT_H
+#define ORDERELEMENT_H
+
+#include "classlist.h"
+#include "mymemory.h"
+#include "constraint.h"
+
+struct OrderElement {
+       uint64_t item;
+       Element* elem;
+};
+
+OrderElement *allocOrderElement(uint64_t item, Element* elem);
+void deleteOrderElement(OrderElement *pair);
+
+#endif/* ORDERELEMENT_H */
+

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 7d123dd3c9dc96d39a7c7f825d311beeae35ae3e..bb076ec14ce1dea867fe142a493ab4027abe8b0c 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -9,8 +9,14 @@
 #include "orderencoder.h"
 #include "ordergraph.h"
 #include "orderedge.h"
+#include "element.h"
+#include "predicate.h"
+#include "orderelement.h"
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+       if(constraint->order->order.type == INTEGERENCODING){
+               return orderIntegerEncodingSATEncoder(This, constraint);
+       }
        switch ( constraint->order->type) {
        case PARTIAL:
                return encodePartialOrderSATEncoder(This, constraint);
@@ -22,11 +28,47 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
        return E_BOGUS;
 }
 
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
+       if(boolOrder->order->graph == NULL){
+               bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type,
+                       OPTIMIZEORDERSTRUCTURE, &onoff);
+               if (doOptOrderStructure ) {
+                       boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
+                       reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+               }
+       }
+       Order* order = boolOrder->order;
+       Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
+       if(!edgeIsNull(gvalue))
+               return gvalue;
+       
+       if (boolOrder->order->elementTable == NULL) {
+               initializeOrderElementsHashTable(boolOrder->order);
+       }
+       //getting two elements and using LT predicate ...
+       Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
+       ElementEncoding *encoding = getElementEncoding(elem1);
+       if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
+               setElementEncodingType(encoding, BINARYINDEX);
+               encodingArrayInitialization(encoding);
+       }
+       Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
+       encoding = getElementEncoding(elem2);
+       if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
+               setElementEncodingType(encoding, BINARYINDEX);
+               encodingArrayInitialization(encoding);
+       }
+       Predicate *predicate =allocPredicateOperator(LT, (Set*[]){order->set, order->set}, 2);
+       Boolean * boolean=allocBooleanPredicate(predicate, (Element *[]){elem1,elem2}, 2, NULL);
+       setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean), CIRCUIT);
+       return encodeConstraintSATEncoder(This, boolean);
+}
+
+Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
        if (order->graph != NULL) {
                OrderGraph *graph=order->graph;
-               OrderNode *first=lookupOrderNodeFromOrderGraph(graph, pair->first);
-               OrderNode *second=lookupOrderNodeFromOrderGraph(graph, pair->second);
+               OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
+               OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
                if ((first != NULL) && (second != NULL)) {
                        OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
                        if (edge != NULL) {
@@ -44,6 +86,28 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
                        }
                }
        }
+       return E_NULL;
+}
+
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
+       HashSetOrderElement* eset = order->elementTable;
+       OrderElement oelement ={item, NULL};
+       if( !containsHashSetOrderElement(eset, &oelement)){
+               Element* elem = allocElementSet(order->set);
+               ElementEncoding* encoding = getElementEncoding(elem);
+               setElementEncodingType(encoding, BINARYINDEX);
+               encodingArrayInitialization(encoding);
+               encodeElementSATEncoder(This, elem);
+               addHashSetOrderElement(eset, allocOrderElement(item, elem));
+               return elem;
+       }else
+               return getHashSetOrderElement(eset, &oelement)->elem;
+}
+Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+       Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
+       if(!edgeIsNull(gvalue))
+               return gvalue;
+       
        HashTableOrderPair *table = order->orderPairTable;
        bool negate = false;
        OrderPair flipped;

diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h
index e3342bfcc3532b4fb0bf8e65aff3687e9c6dddf7..8faa73d074ab0f3c64fab6c39b3ac6ebdcab1a1e 100644 (file)
--- a/src/Backend/satorderencoder.h
+++ b/src/Backend/satorderencoder.h
@@ -2,6 +2,9 @@
 #define SATORDERENCODER_H
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
+Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
+Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second);
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);

diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h
index ad204f39832c4eabe2e4e7b0a8838315969c6c89..be5c8c0fdfd11082f6f1457b45f206573ef7722d 100644 (file)
--- a/src/Backend/sattranslator.h
+++ b/src/Backend/sattranslator.h
@@ -14,6 +14,9 @@
 
 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean);
 HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second);
+/**
+ * most significant bit is represented by variable index 0 
+ */
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc);
 uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc);
 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc);

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 67b32a3e147f9d65f3bb5aed947a23d375be4c02..d6cdd164ab1e6a42eb3db386c79c130bff2f6ef0 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -5,6 +5,7 @@
 #include "ordernode.h"
 #include "orderedge.h"
 #include "ordergraph.h"
+#include "orderelement.h"
 
 VectorImpl(Table, Table *, 4);
 VectorImpl(Set, Set *, 4);
@@ -71,11 +72,20 @@ static inline bool order_edge_equals(OrderEdge *key1, OrderEdge *key2) {
        return key1->sink == key2->sink && key1->source == key2->source;
 }
 
-HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_function, order_pair_equals, ourfree);
+static inline unsigned int order_element_hash_function(OrderElement* This) {
+       return (uint)This->item;
+}
+
+static inline bool order_element_equals(OrderElement* key1, OrderElement* key2) {
+       return key1->item == key2->item;
+}
+
 
 HashSetImpl(Boolean, Boolean *, Ptr_hash_function, Ptr_equals);
 HashSetImpl(TableEntry, TableEntry *, table_entry_hash_function, table_entry_equals);
 HashSetImpl(OrderNode, OrderNode *, order_node_hash_function, order_node_equals);
 HashSetImpl(OrderEdge, OrderEdge *, order_edge_hash_function, order_edge_equals);
+HashSetImpl(OrderElement, OrderElement *, order_element_hash_function, order_element_equals);
 
 HashTableImpl(NodeToNodeSet, OrderNode *, HashSetOrderNode *, Ptr_hash_function, Ptr_equals, deleteHashSetOrderNode);
+HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_function, order_pair_equals, ourfree);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index d787adac42fd249f40e084d533d49333eaba7293..4ee55494ff4247e4937577970de23f42a0e189fb 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -31,6 +31,7 @@ HashSetDef(Boolean, Boolean *);
 HashSetDef(TableEntry, TableEntry *);
 HashSetDef(OrderNode, OrderNode *);
 HashSetDef(OrderEdge, OrderEdge *);
+HashSetDef(OrderElement, OrderElement *);
 
 HashTableDef(NodeToNodeSet, OrderNode *, HashSetOrderNode *);
 #endif

diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h
index 3b7b4f7cf0eb7bf94abb081e267caf6dece66786..35ad5649afa8344a241a31a18f97b76bb07a6665 100644 (file)
--- a/src/Encoders/orderencoding.h
+++ b/src/Encoders/orderencoding.h
@@ -3,7 +3,7 @@
 #include "classlist.h"
 
 enum OrderEncodingType {
-       ORDER_UNASSIGNED, PAIRWISE
+       ORDER_UNASSIGNED, PAIRWISE, INTEGERENCODING
 };
 
 typedef enum OrderEncodingType OrderEncodingType;

diff --git a/src/classlist.h b/src/classlist.h
index ca192fa22d4ef9629ee8fad6198aac7b81ed5f75..7e904e88d638a6b4ef9907e1ea53e18bca34f0d0 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -70,6 +70,9 @@ typedef struct Order Order;
 struct OrderPair;
 typedef struct OrderPair OrderPair;
 
+struct OrderElement;
+typedef struct OrderElement OrderElement;
+
 struct ElementEncoding;
 typedef struct ElementEncoding ElementEncoding;