diff options
| -rw-r--r-- | stp/AST/ToSAT.cpp | 19 | ||||
| -rw-r--r-- | stp/sat/Solver.cpp | 18 | ||||
| -rw-r--r-- | stp/sat/Solver.h | 3 |
3 files changed, 20 insertions, 20 deletions
diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp index 29635ec5..ed8f1761 100644 --- a/stp/AST/ToSAT.cpp +++ b/stp/AST/ToSAT.cpp @@ -121,15 +121,16 @@ namespace BEEV { return; double cpu_time = MINISAT::cpuTime(); MINISAT::int64 mem_used = MINISAT::memUsed(); - reportf("restarts : %"I64_fmt"\n", s.starts); - reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); - reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); - reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); - reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", - s.tot_literals, - (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); - if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); - reportf("CPU time : %g s\n", cpu_time); + printf("restarts : %"I64_fmt"\n", s.starts); + printf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); + printf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); + printf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); + printf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", + s.tot_literals, + (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); + if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used / 1048576.0); + printf("CPU time : %g s\n", cpu_time); + fflush(stdout); } // Prints Satisfying assignment directly, for debugging. diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp index 13a9ae08..9761c719 100644 --- a/stp/sat/Solver.cpp +++ b/stp/sat/Solver.cpp @@ -768,24 +768,26 @@ bool Solver::solve(const vec<Lit>& assumps) assumps.copyTo(assumptions); if (verbosity >= 1){ - reportf("==================================[MINISAT]====================================\n"); - reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); - reportf("===============================================================================\n"); + printf("==================================[MINISAT]====================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); + printf("===============================================================================\n"); } // Search: while (status == l_Undef){ if (verbosity >= 1) - //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); - reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + //printf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); status = search((int)nof_conflicts, (int)nof_learnts); nof_conflicts *= params.restart_inc; nof_learnts *= params.learntsize_inc; } - if (verbosity >= 1) - reportf("==============================================================================\n"); + if (verbosity >= 1) { + printf("==============================================================================\n"); + fflush(stdout); + } if (status == l_True){ // Copy model: diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h index 8826fac7..0a6dc87e 100644 --- a/stp/sat/Solver.h +++ b/stp/sat/Solver.h @@ -24,9 +24,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "VarOrder.h" namespace MINISAT { -// Redfine if you want output to go somewhere else: -#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) ) - //================================================================================================= // Solver -- the main class: |