Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 29a99118eda43b1e26b6553afb11164d9ca2ea08..d0aa32ea175c04b0381df87ee41ed9e20f4135bd 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,7 +11,7 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "analyzer.h"
+#include "transformer.h"
 #include "autotuner.h"
 #include "astops.h"
 #include "structs.h"
@@ -24,6 +24,7 @@ CSolver::CSolver() :
        elapsedTime(0)
 {
        satEncoder = new SATEncoder(this);
+       transformer = new Transformer(this);
 }
 
 /** This function tears down the solver and the entire AST */
@@ -67,6 +68,7 @@ CSolver::~CSolver() {
        delete boolTrue;
        delete boolFalse;
        delete satEncoder;
+       delete transformer;
 }
 
 CSolver *CSolver::clone() {
@@ -375,7 +377,7 @@ int CSolver::solve() {
                
        long long startTime = getTimeNano();
        computePolarities(this);
-       orderAnalysis(this);
+       transformer->orderAnalysis();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();