mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

add logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-18 12:30:40 -08:00
parent 5bec982cc5
commit 924c296704
2 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/nlsat/nlsat_solver.cpp
View file

@ -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;

8
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -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)));
}