Move constraints to set

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 9717886709374cc5a80a0e85bf46c1665d9a03b6..f380fdd3858a692ee0ae3cc27328e73709aa78a8 100644 (file)
--- 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 9282de97c359dd5f7cc2b9b1e38e27a25497e939..087046fd933bb8b3abdda9c2f5008f7ff4874961 100644 (file)
--- 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 7be60b0fa4dd1f69cd5eb5b46a370388ad0f65c3..48565e8383b10e262f42c52de7396005d8ea50a4 100644 (file)
--- 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 183a1230f90019e057146d58ba46d4879997a991..d787adac42fd249f40e084d533d49333eaba7293 100644 (file)
--- 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 a7941a6405812d8ff8f599ce10dd1926ba03f344..71dc582cba636090189f7f097894ed390cbbaa8b 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -14,10 +14,12 @@
 #include <strings.h>
 
 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 416da2a96f7efe5567b8013bef5e405dbac00359..3e4138092f38c0a21b8525e39d29e796232db8d3 100644 (file)
--- 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 683084bef397bf1b49d5c4ed074419ae514d32a2..8d66d7ea4dfb291065269e17b223c72f247aba35 100644 (file)
--- 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 cde6c64688b83ee6f670912338f6196a294c19b6..607bca675aa5900084f598afda2d5c54179eae66 100644 (file)
--- 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;