From: bdemsky Date: Thu, 17 Aug 2017 23:09:07 +0000 (-0700) Subject: Move constraints to set X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=5238a70cb4f58d262d768ecdc2d9603cbc3386db;p=satune.git Move constraints to set --- diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index 9717886..f380fdd 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -28,15 +28,15 @@ void deleteSATEncoder(SATEncoder *This) { } void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) { - VectorBoolean *constraints = csolver->constraints; - uint size = getSizeVectorBoolean(constraints); - for (uint i = 0; i < size; i++) { + HSIteratorBoolean *iterator=iteratorBoolean(csolver->constraints); + while(hasNextBoolean(iterator)) { + Boolean *constraint = nextBoolean(iterator); model_print("Encoding All ...\n\n"); - Boolean *constraint = getVectorBoolean(constraints, i); Edge c = encodeConstraintSATEncoder(This, constraint); model_print("Returned Constraint in EncodingAll:\n"); addConstraintCNF(This->cnf, c); } + deleteIterBoolean(iterator); } Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index 9282de9..087046f 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -41,7 +41,8 @@ typedef struct HashSet ## Name HashSet ## Name; \ \ HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor); \ - void deleteHashSet ## Name(struct HashSet ## Name *set); \ + HashSet ## Name * allocDefHashSet ## Name (); \ + void deleteHashSet ## Name(struct HashSet ## Name *set); \ HashSet ## Name * copyHashSet ## Name(HashSet ## Name * set); \ void resetHashSet ## Name(HashSet ## Name * set); \ bool addHashSet ## Name(HashSet ## Name * set,_Key key); \ @@ -87,7 +88,11 @@ _Key k = hsit->last->key; \ removeHashSet ## Name(hsit->set, k); \ } \ - \ + \ + HashSet ## Name * allocDefHashSet ## Name () { \ + return allocHashSet ## Name(16, 0.25); \ + } \ + \ HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor) { \ HashSet ## Name * set = (HashSet ## Name *)ourmalloc(sizeof(struct HashSet ## Name)); \ set->table = allocHashTable ## Name ## Set(initialcapacity, factor); \ diff --git a/src/Collections/structs.c b/src/Collections/structs.c index 7be60b0..48565e8 100644 --- a/src/Collections/structs.c +++ b/src/Collections/structs.c @@ -28,7 +28,7 @@ inline bool Ptr_equals(void *key1, void *key2) { return key1 == key2; } -static inline unsigned int order_pair_hash_Function(OrderPair *This) { +static inline unsigned int order_pair_hash_function(OrderPair *This) { return (uint) (This->first << 2) ^ This->second; } @@ -36,7 +36,7 @@ static inline unsigned int order_pair_equals(OrderPair *key1, OrderPair *key2) { return key1->first == key2->first && key1->second == key2->second; } -static inline unsigned int table_entry_hash_Function(TableEntry *This) { +static inline unsigned int table_entry_hash_function(TableEntry *This) { unsigned int h = 0; for (uint i = 0; i < This->inputSize; i++) { h += This->inputs[i]; @@ -54,7 +54,7 @@ static inline bool table_entry_equals(TableEntry *key1, TableEntry *key2) { return true; } -static inline unsigned int order_node_hash_Function(OrderNode *This) { +static inline unsigned int order_node_hash_function(OrderNode *This) { return (uint) This->id; } @@ -63,7 +63,7 @@ static inline bool order_node_equals(OrderNode *key1, OrderNode *key2) { return key1->id == key2->id; } -static inline unsigned int order_edge_hash_Function(OrderEdge *This) { +static inline unsigned int order_edge_hash_function(OrderEdge *This) { return (uint) (((uintptr_t)This->sink) ^ ((uintptr_t)This->source << 4)); } @@ -71,10 +71,11 @@ 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); +HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_function, order_pair_equals, ourfree); -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(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); HashTableImpl(NodeToNodeSet, OrderNode *, HashSetOrderNode *, Ptr_hash_function, Ptr_equals, deleteHashSetOrderNode); diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 183a123..d787ada 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -27,7 +27,7 @@ VectorDef(OrderGraph, OrderGraph *); HashTableDef(Void, void *, void *); HashTableDef(OrderPair, OrderPair *, OrderPair *); -HashSetDef(Void, void *); +HashSetDef(Boolean, Boolean *); HashSetDef(TableEntry, TableEntry *); HashSetDef(OrderNode, OrderNode *); HashSetDef(OrderEdge, OrderEdge *); diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c index a7941a6..71dc582 100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@ -14,10 +14,12 @@ #include void naiveEncodingDecision(CSolver *This) { - for (uint i = 0; i < getSizeVectorBoolean(This->constraints); i++) { - Boolean *boolean = getVectorBoolean(This->constraints, i); + HSIteratorBoolean *iterator=iteratorBoolean(This->constraints); + while(hasNextBoolean(iterator)) { + Boolean *boolean = nextBoolean(iterator); naiveEncodingConstraint(boolean); } + deleteIterBoolean(iterator); } void naiveEncodingConstraint(Boolean *This) { diff --git a/src/Encoders/polarityassignment.c b/src/Encoders/polarityassignment.c index 416da2a..3e41380 100644 --- a/src/Encoders/polarityassignment.c +++ b/src/Encoders/polarityassignment.c @@ -2,12 +2,14 @@ #include "csolver.h" void computePolarities(CSolver *This) { - for (uint i = 0; i < getSizeVectorBoolean(This->constraints); i++) { - Boolean *boolean = getVectorBoolean(This->constraints, i); + HSIteratorBoolean *iterator=iteratorBoolean(This->constraints); + while(hasNextBoolean(iterator)) { + Boolean *boolean = nextBoolean(iterator); updatePolarity(boolean, P_TRUE); updateMustValue(boolean, BV_MUSTBETRUE); computePolarityAndBooleanValue(boolean); } + deleteIterBoolean(iterator); } void updatePolarity(Boolean *This, Polarity polarity) { diff --git a/src/csolver.c b/src/csolver.c index 683084b..8d66d7e 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -12,7 +12,7 @@ CSolver *allocCSolver() { CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver)); - This->constraints = allocDefVectorBoolean(); + This->constraints = allocDefHashSetBoolean(); This->allBooleans = allocDefVectorBoolean(); This->allSets = allocDefVectorSet(); This->allElements = allocDefVectorElement(); @@ -27,7 +27,7 @@ CSolver *allocCSolver() { /** This function tears down the solver and the entire AST */ void deleteSolver(CSolver *This) { - deleteVectorBoolean(This->constraints); + deleteHashSetBoolean(This->constraints); uint size = getSizeVectorBoolean(This->allBooleans); for (uint i = 0; i < size; i++) { @@ -178,7 +178,7 @@ Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint } void addConstraint(CSolver *This, Boolean *constraint) { - pushVectorBoolean(This->constraints, constraint); + addHashSetBoolean(This->constraints, constraint); } Order *createOrder(CSolver *This, OrderType type, Set *set) { diff --git a/src/csolver.h b/src/csolver.h index cde6c64..607bca6 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -7,7 +7,7 @@ struct CSolver { SATEncoder *satEncoder; /** This is a vector of constraints that must be satisfied. */ - VectorBoolean *constraints; + HashSetBoolean *constraints; /** This is a vector of all boolean structs that we have allocated. */ VectorBoolean *allBooleans;