removing true nodes from the OrderGraph

[satune.git] / src / csolver.c

diff --git a/src/csolver.c b/src/csolver.c
index 036729b1d9e235c4da20c0ab71516ad1fc4aaa62..e9c9526e14d9861273c9793fda12f2d3e26a5756 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));
@@ -22,8 +24,8 @@ CSolver *allocCSolver() {
        This->allTables = allocDefVectorTable();
        This->allOrders = allocDefVectorOrder();
        This->allFunctions = allocDefVectorFunction();
-       This->satEncoder = allocSATEncoder();
        This->tuner = allocTuner();
+       This->satEncoder = allocSATEncoder(This);
        return This;
 }
 
@@ -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);