Fixin some bugs ..

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 48565e8383b10e262f42c52de7396005d8ea50a4..67b32a3e147f9d65f3bb5aed947a23d375be4c02 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -20,11 +20,11 @@ VectorImpl(Int, uint64_t, 4);
 VectorImpl(OrderNode, OrderNode *, 4);
 VectorImpl(OrderGraph, OrderGraph *, 4);
 
-inline unsigned int Ptr_hash_function(void *hash) {
+static inline unsigned int Ptr_hash_function(void *hash) {
        return (unsigned int)((int64)hash >> 4);
 }
 
-inline bool Ptr_equals(void *key1, void *key2) {
+static inline bool Ptr_equals(void *key1, void *key2) {
        return key1 == key2;
 }
 

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index a9ab298447387532e7368f54e819bc400c49e81c..c47a16f7d5c74529c90d35e3d4b5a93b4cb4b2e7 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -8,6 +8,7 @@
 OrderGraph *allocOrderGraph(Order *order) {
        OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
        This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
        This->order = order;
        return This;
 }

diff --git a/src/csolver.c b/src/csolver.c
index 036729b1d9e235c4da20c0ab71516ad1fc4aaa62..fbc86914af04d8f6439ced323c4e0769811da14e 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -10,6 +10,8 @@
 #include "satencoder.h"
 #include "sattranslator.h"
 #include "tunable.h"
+#include "orderencoder.h"
+#include "polarityassignment.h"
 
 CSolver *allocCSolver() {
        CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
@@ -200,6 +202,8 @@ Boolean *orderConstraint(CSolver *This, Order *order, uint64_t first, uint64_t s
 int startEncoding(CSolver *This) {
        naiveEncodingDecision(This);
        SATEncoder *satEncoder = This->satEncoder;
+       computePolarities(This);
+       orderAnalysis(This);
        encodeAllSATEncoder(This, satEncoder);
        int result = solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);