Merge branch 'master' into brian

[satune.git] / src / csolver.c

diff --git a/src/csolver.c b/src/csolver.c
index 60240990e484371648b6e1b613d5cc8054284aca..d90304431634c30faf0d4fbfad73dd81f6af2743 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -171,12 +171,13 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
        return constraint;
 }
 
-void encode(CSolver* solver){
+void startEncoding(CSolver* solver){
        naiveEncodingDecision(solver);
        SATEncoder* satEncoder = allocSATEncoder();
-       initializeConstraintVars(solver, satEncoder);
        encodeAllSATEncoder(solver, satEncoder);
+       int result= solveCNF(satEncoder->cnf);
+       model_print("sat_solver's result:%d\n", result);
        //For now, let's just delete it, and in future for doing queries 
        //we may need it.
        deleteSATEncoder(satEncoder);
-}
\ No newline at end of file
+}