Fixin some bugs ..

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 48565e8..67b32a3 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 a9ab298..c47a16f 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 036729b..fbc8691 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);