This->type = type;
initOrderEncoding(&This->order, This);
This->orderPairTable = NULL;
+ This->elementTable = NULL;
This->graph = NULL;
return 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);
}
resetAndDeleteHashTableOrderPair(This->orderPairTable);
deleteHashTableOrderPair(This->orderPairTable);
}
+ if(This->elementTable != NULL){
+ deleteHashSetOrderElement(This->elementTable);
+ }
if (This->graph != NULL) {
deleteOrderGraph(This->graph);
}
OrderType type;
Set *set;
HashTableOrderPair *orderPairTable;
+ HashSetOrderElement* elementTable;
OrderGraph *graph;
VectorBooleanOrder constraints;
OrderEncoding 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);
--- /dev/null
+#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);
+}
--- /dev/null
+/*
+ * 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 */
+
#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);
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) {
}
}
}
+ 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;
#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);
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);
#include "ordernode.h"
#include "orderedge.h"
#include "ordergraph.h"
+#include "orderelement.h"
VectorImpl(Table, Table *, 4);
VectorImpl(Set, Set *, 4);
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);
HashSetDef(TableEntry, TableEntry *);
HashSetDef(OrderNode, OrderNode *);
HashSetDef(OrderEdge, OrderEdge *);
+HashSetDef(OrderElement, OrderElement *);
HashTableDef(NodeToNodeSet, OrderNode *, HashSetOrderNode *);
#endif
#include "classlist.h"
enum OrderEncodingType {
- ORDER_UNASSIGNED, PAIRWISE
+ ORDER_UNASSIGNED, PAIRWISE, INTEGERENCODING
};
typedef enum OrderEncodingType OrderEncodingType;
struct OrderPair;
typedef struct OrderPair OrderPair;
+struct OrderElement;
+typedef struct OrderElement OrderElement;
+
struct ElementEncoding;
typedef struct ElementEncoding ElementEncoding;