diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-27 14:41:47 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-27 14:41:47 -0400 |
| commit | 9006b759cfa01c6006196e0716c2d67c760556a6 (patch) | |
| tree | 6870500d18b75d7464b4b5c910ff2edf186a8db0 /src/prop | |
| parent | a891d1259fb3d250910186bbdf3083b55eb23f26 (diff) | |
timespec printing bug
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()); |