From: Hamed Date: Tue, 22 Aug 2017 22:09:28 +0000 (-0700) Subject: Adding support for Integer Encoding ... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=72df0425fdbb8581b5ae2b17a8c1da9fbaf848ae Adding support for Integer Encoding ... --- diff --git a/src/AST/order.c b/src/AST/order.c index b5840da..92bb557 100644 --- 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 c5a03a8..a4a7621 100644 --- 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 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 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 7d123dd..bb076ec 100644 --- 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 e3342bf..8faa73d 100644 --- 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 ad204f3..be5c8c0 100644 --- 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 67b32a3..d6cdd16 100644 --- 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 d787ada..4ee5549 100644 --- 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 3b7b4f7..35ad564 100644 --- 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 ca192fa..7e904e8 100644 --- 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;