From 924c2967049711ec73d318b5d7edc8873fbd1093 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 18 Nov 2023 12:30:40 -0800
Subject: [PATCH] add logging
---
src/nlsat/nlsat_solver.cpp | 10 ++++++++++
src/tactic/smtlogics/qfnia_tactic.cpp | 8 +++-----
2 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 568a25a29..8993182a2 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1491,6 +1491,7 @@ namespace nlsat {
m_bk = 0;
m_xk = null_var;
m_conflicts = 0;
+ m_next_conflict = 100;
while (true) {
CASSERT("nlsat", check_satisfied());
@@ -1527,6 +1528,7 @@ namespace nlsat {
return l_false;
if (m_conflicts >= m_max_conflicts)
return l_undef;
+ log();
}
if (m_xk == null_var) {
@@ -1541,6 +1543,14 @@ namespace nlsat {
}
}
+ unsigned m_next_conflict = 100;
+ void log() {
+ if (m_conflicts < m_next_conflict)
+ return;
+ m_next_conflict += 100;
+ IF_VERBOSE(2, verbose_stream() << "(nlsat :conflicts " << m_conflicts << " :decisions " << m_decisions << " :propagations " << m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n");
+ }
+
lbool search_check() {
lbool r = l_undef;
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 3dd66606d..0dad56a19 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -117,10 +117,8 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
mk_report_verbose_tactic("(qfnia-tactic)", 10),
mk_qfnia_preamble(m, p),
or_else(mk_qfnia_sat_solver(m, p),
- try_for(mk_qfnia_smt_solver(m, p), 2000),
- mk_qfnia_nlsat_solver(m, p),
- mk_qfnia_smt_solver(m, p))
- )
- ;
+ try_for(mk_qfnia_smt_solver(m, p), 2000),
+ mk_qfnia_nlsat_solver(m, p),
+ mk_qfnia_smt_solver(m, p)));
}