From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 22 Aug 2017 00:29:15 +0000 (-0700)
Subject: Fixin some bugs ..
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c67bebcc33b92c5809d9e2895e722c7875e3224f;p=satune.git

Fixin some bugs ..
---

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