removing true nodes from the OrderGraph

[satune.git] / src / csolver.c

diff --git a/src/csolver.c b/src/csolver.c
index 683084bef397bf1b49d5c4ed074419ae514d32a2..e9c9526e14d9861273c9793fda12f2d3e26a5756 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -9,10 +9,14 @@
 #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));
-       This->constraints = allocDefVectorBoolean();
+       This->unsat = false;
+       This->constraints = allocDefHashSetBoolean();
        This->allBooleans = allocDefVectorBoolean();
        This->allSets = allocDefVectorSet();
        This->allElements = allocDefVectorElement();
@@ -20,14 +24,15 @@ CSolver *allocCSolver() {
        This->allTables = allocDefVectorTable();
        This->allOrders = allocDefVectorOrder();
        This->allFunctions = allocDefVectorFunction();
-       This->satEncoder = allocSATEncoder();
+       This->tuner = allocTuner();
+       This->satEncoder = allocSATEncoder(This);
        return This;
 }
 
 /** This function tears down the solver and the entire AST */
 
 void deleteSolver(CSolver *This) {
-       deleteVectorBoolean(This->constraints);
+       deleteHashSetBoolean(This->constraints);
 
        uint size = getSizeVectorBoolean(This->allBooleans);
        for (uint i = 0; i < size; i++) {
@@ -71,6 +76,7 @@ void deleteSolver(CSolver *This) {
        }
        deleteVectorFunction(This->allFunctions);
        deleteSATEncoder(This->satEncoder);
+       deleteTuner(This->tuner);
        ourfree(This);
 }
 
@@ -178,7 +184,7 @@ Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint
 }
 
 void addConstraint(CSolver *This, Boolean *constraint) {
-       pushVectorBoolean(This->constraints, constraint);
+       addHashSetBoolean(This->constraints, constraint);
 }
 
 Order *createOrder(CSolver *This, OrderType type, Set *set) {
@@ -196,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);