removing true nodes from the OrderGraph

[satune.git] / src / csolver.c

diff --git a/src/csolver.c b/src/csolver.c
index 2295e7bd923b487fd86f50f65f258d6bcd730535..e9c9526e14d9861273c9793fda12f2d3e26a5756 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -9,6 +9,9 @@
 #include "function.h"
 #include "satencoder.h"
 #include "sattranslator.h"
+#include "tunable.h"
+#include "orderencoder.h"
+#include "polarityassignment.h"
 
 CSolver *allocCSolver() {
        CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
@@ -21,7 +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;
 }
 
@@ -72,6 +76,7 @@ void deleteSolver(CSolver *This) {
        }
        deleteVectorFunction(This->allFunctions);
        deleteSATEncoder(This->satEncoder);
+       deleteTuner(This->tuner);
        ourfree(This);
 }
 
@@ -197,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);