Merge branch 'master' into brian
[satune.git] / src / csolver.c
index d63c266c804aa2bf587e76db54bda52d939cafcb..d90304431634c30faf0d4fbfad73dd81f6af2743 100644 (file)
@@ -174,9 +174,10 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
 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
+}