diff options
Diffstat (limited to 'src/sat/glucose/Glucose.cpp')
| -rw-r--r-- | src/sat/glucose/Glucose.cpp | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index b3df0c82..6301a0f8 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -92,8 +92,8 @@ Solver::Solver() : SolverType(0) , pCnfFunc(NULL) , nCallConfl(1000) - , verbEveryConflicts(10000) , terminate_search_early(false) + , verbEveryConflicts(10000) , pstop(NULL) , nRuntimeLimit(0) @@ -1188,16 +1188,16 @@ double Solver::progressEstimate() const void Solver::printIncrementalStats() { printf("c---------- Glucose Stats -------------------------\n"); - printf("c restarts : %lld\n", starts); - printf("c nb ReduceDB : %lld\n", nbReduceDB); - printf("c nb removed Clauses : %lld\n", nbRemovedClauses); - printf("c nb learnts DL2 : %lld\n", nbDL2); - printf("c nb learnts size 2 : %lld\n", nbBin); - printf("c nb learnts size 1 : %lld\n", nbUn); - - printf("c conflicts : %lld\n", conflicts); - printf("c decisions : %lld\n", decisions); - printf("c propagations : %lld\n", propagations); + printf("c restarts : %ld\n", starts); + printf("c nb ReduceDB : %ld\n", nbReduceDB); + printf("c nb removed Clauses : %ld\n", nbRemovedClauses); + printf("c nb learnts DL2 : %ld\n", nbDL2); + printf("c nb learnts size 2 : %ld\n", nbBin); + printf("c nb learnts size 1 : %ld\n", nbUn); + + printf("c conflicts : %ld\n", conflicts); + printf("c decisions : %ld\n", decisions); + printf("c propagations : %ld\n", propagations); printf("c SAT Calls : %d in %g seconds\n", nbSatCalls, totalTime4Sat); printf("c UNSAT Calls : %d in %g seconds\n", nbUnsatCalls, totalTime4Unsat); |