add logging

Z3Prover · Nov 18, 2023 · 924c296 · 924c296
1 parent 5bec982
commit 924c296
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 5 deletions.
diff --git 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
@@ -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)));
 }