Fix memory bugs

diff --git a/src/AST/order.c b/src/AST/order.c
index 3e0f73e285bcab0d0c88a95de824c5b21d4430ab..b5840da5e3c9be6dd173bc5080ad5a1be4da3ac2 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -2,6 +2,7 @@
 #include "structs.h"
 #include "set.h"
 #include "boolean.h"
+#include "ordergraph.h"
 
 Order *allocOrder(OrderType type, Set *set) {
        Order *This = (Order *)ourmalloc(sizeof(Order));
@@ -33,5 +34,8 @@ void deleteOrder(Order *This) {
                resetAndDeleteHashTableOrderPair(This->orderPairTable);
                deleteHashTableOrderPair(This->orderPairTable);
        }
+       if (This->graph != NULL) {
+               deleteOrderGraph(This->graph);
+       }
        ourfree(This);
 }

diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h
index 15f69af6b330dc05090f1c31c0e6283fd6bcd3ac..59e7eced0334a6b93542e8723c977eaa85bcbc46 100644 (file)
--- a/src/Collections/hashtable.h
+++ b/src/Collections/hashtable.h
@@ -103,9 +103,9 @@
                        ourfree(tab->zero);                                               \
                        tab->zero = NULL;                                                   \
                }                                                                   \
-               tab->size = 0;                                                        \
-       }                                                                     \
-                                                                        \
+               tab->size = 0;                                                                                                                                                                                                                  \
+       }                                                                                                                                                                                                                                                                                       \
+                                                                                                                                                                                                                                                                                               \
        void reset ## Name(HashTable ## Name * tab) {                         \
                memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \
                if (tab->zero) {                                                    \

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index a43d39dfec00b974994d414ffb5650e1d5d1c690..00c64688678ab11aebde57b33f1d22ca10e2e5cd 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -160,6 +160,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
        }
 
        resetAndDeleteHashTableNodeToNodeSet(table);
+       deleteHashTableNodeToNodeSet(table);
        resetNodeInfoStatusSCC(graph);
        deleteVectorArrayOrderNode(&sccNodes);
        deleteVectorArrayOrderNode(&finishNodes);
@@ -250,6 +251,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode
        }
 
        resetAndDeleteHashTableNodeToNodeSet(table);
+       deleteHashTableNodeToNodeSet(table);
 }
 
 /* This function finds edges that would form a cycle with must edges

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index f92007650c5b0e5ee179e7ad84c5acacfa8cd022..32e13501c0fdceab9a1ba90dc7d7c3f295e52e65 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -83,7 +83,7 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo
                _1to2->polPos = true;
                addNewOutgoingEdge(node1, _1to2);
                addNewIncomingEdge(node2, _1to2);
-               if (constr->base.polarity == BV_MUSTBETRUE)
+               if (constr->base.boolVal == BV_MUSTBETRUE)
                        break;
        }
        case BV_MUSTBEFALSE: {
@@ -176,5 +176,7 @@ void deleteOrderGraph(OrderGraph *graph) {
                deleteOrderEdge(edge);
        }
        deleteIterOrderEdge(eiterator);
+       deleteHashSetOrderNode(graph->nodes);
+       deleteHashSetOrderEdge(graph->edges);
        ourfree(graph);
 }

diff --git a/src/Test/ordertest.c b/src/Test/ordertest.c
index 852df3456cfd0127bbe21a66ee05c48391b31600..eef8c3620f992324a6ae99e59d0633c53e833ae5 100644 (file)
--- a/src/Test/ordertest.c
+++ b/src/Test/ordertest.c
@@ -16,13 +16,8 @@ int main(int numargs, char **argv) {
        addConstraint(solver, b1);
        addConstraint(solver, b2);
        if (startEncoding(solver) == 1)
-               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n",
-                                        getOrderConstraintValue(solver, order, 5, 1),
-                                        getOrderConstraintValue(solver, order, 1, 4),
-                                        getOrderConstraintValue(solver, order, 5, 4),
-                                        getOrderConstraintValue(solver, order, 1, 5),
-                                        getOrderConstraintValue(solver, order, 1111, 5));
+               printf("SAT\n");
        else
                printf("UNSAT\n");
        deleteSolver(solver);
-}
\ No newline at end of file
+}