Run tabbing pass

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index e2bb4bc278f189c5dcd3f1cb9365ed3701873109..d825df5e4c2a8d12192ec1fb5da68fe60eac06cc 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -10,11 +10,11 @@
 #include "satencoder.h"
 #include "sattranslator.h"
 #include "tunable.h"
-#include "orderencoder.h"
 #include "polarityassignment.h"
+#include "orderdecompose.h"
 
 CSolver::CSolver() : unsat(false) {
-       tuner = allocTuner();
+       tuner = new Tuner();
        satEncoder = allocSATEncoder(this);
 }
 
@@ -57,7 +57,7 @@ CSolver::~CSolver() {
        }
 
        deleteSATEncoder(satEncoder);
-       deleteTuner(tuner);
+       delete tuner;
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -155,13 +155,15 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu
 }
 
 Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
-       Boolean *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
+       BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
        allBooleans.push(boolean);
        return boolean;
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
-       return new BooleanLogic(this, op, array, asize);
+       Boolean *boolean = new BooleanLogic(this, op, array, asize);
+       allBooleans.push(boolean);
+       return boolean;
 }
 
 void CSolver::addConstraint(Boolean *constraint) {
@@ -181,9 +183,9 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second)
 }
 
 int CSolver::startEncoding() {
-       naiveEncodingDecision(this);
        computePolarities(this);
        orderAnalysis(this);
+       naiveEncodingDecision(this);
        encodeAllSATEncoder(this, satEncoder);
        int result = solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);