diff options
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 610023b70..b2857216d 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/minisat.h" #include "prop/options.h" #include "util/output.h" +#include "util/periodic_statistics.h" #include "expr/command.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" @@ -478,6 +479,13 @@ Lit Solver::pickBranchLit() { Lit nextLit; + // Every so-many-decisions print the total time + if(options::periodicStatsInterval() && decisions % options::periodicStatsInterval() == 0) { + PeriodicStatistic::print("sat::decisions", decisions); + PeriodicStatistic::print("sat::conflicts", conflicts); + PeriodicStatistic::print("sat::propagations", propagations); + } + #ifdef CVC4_REPLAY nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision()); |