mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

add logging for first conflict

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-01 20:50:52 -07:00
parent 2f02278227
commit 8f4ffc7caf
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_solver.cpp
View file

@ -1574,7 +1574,7 @@ namespace nlsat {
} }
void gc() { void gc() {
if (m_learned.size() <= 2*m_clauses.size()) if (m_learned.size() <= 4*m_clauses.size())
return; return;
reset_watches(); reset_watches();
reinit_cache(); reinit_cache();
@ -1595,7 +1595,7 @@ namespace nlsat {
unsigned m_next_conflict = 100; unsigned m_next_conflict = 100;
void log() { void log() {
if (m_conflicts < m_next_conflict) if (m_conflicts != 1 && m_conflicts < m_next_conflict)
return; return;
m_next_conflict += 100; 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"); IF_VERBOSE(2, verbose_stream() << "(nlsat :conflicts " << m_conflicts << " :decisions " << m_decisions << " :propagations " << m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n");
@ -1605,7 +1605,7 @@ namespace nlsat {
lbool search_check() { lbool search_check() {
lbool r = l_undef; lbool r = l_undef;
m_conflicts = 0; m_conflicts = 0;
m_next_conflict = 100; m_next_conflict = 0;
while (true) { while (true) {
r = search(); r = search();
if (r != l_true) break; if (r != l_true) break;
@ -3015,7 +3015,7 @@ namespace nlsat {
if (apply_fm_equality(x, clauses, lo, hi)) if (apply_fm_equality(x, clauses, lo, hi))
return true; return true;
return false; // return false;
if (!all_solved) if (!all_solved)
return false; return false;