From 839594ac12a05aa2038b34270f0cffc00460e286 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 7 Aug 2024 09:01:49 -1000 Subject: [PATCH] remove option look_for_0_witness Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_interval_set.cpp | 34 ++++++++++++++++---------------- src/nlsat/nlsat_interval_set.h | 2 +- src/nlsat/nlsat_params.pyg | 2 -- src/nlsat/nlsat_solver.cpp | 4 +--- 4 files changed, 19 insertions(+), 23 deletions(-) diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 0c15d580b..76a310f00 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -703,7 +703,7 @@ namespace nlsat { } - void interval_set_manager::pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize, bool look_for_zero) { + void interval_set_manager::pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) { SASSERT(!is_full(s)); if (s == nullptr) { m_am.set(w, 0); @@ -711,24 +711,24 @@ namespace nlsat { } unsigned n = 0; unsigned num = num_intervals(s); - if (look_for_zero) { - scoped_anum zero(m_am); - m_am.set(zero, 0); - bool available = true; - for (unsigned i = 0; i < num; ++i) { - int sgn = compare_interval_with_zero(s->m_intervals[i], zero, m_am); - if (sgn == 0) { - available = false; - break; - } - if (sgn > 0) - break; - } - if (available) { - m_am.set(w, 0); - return ; + // try to assign w to zero first to simplify the polynomials + scoped_anum zero(m_am); + m_am.set(zero, 0); + bool available = true; + for (unsigned i = 0; i < num; ++i) { + int sgn = compare_interval_with_zero(s->m_intervals[i], zero, m_am); + if (sgn == 0) { + available = false; + break; } + if (sgn > 0) + break; } + if (available) { + m_am.set(w, 0); + return ; + } + // cannot assign w to zero if (!s->m_intervals[num-1].m_upper_inf) { // upper is not oo n++; diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h index 33b741ebd..2e74f33c6 100644 --- a/src/nlsat/nlsat_interval_set.h +++ b/src/nlsat/nlsat_interval_set.h @@ -108,7 +108,7 @@ namespace nlsat { \pre !is_full(s) */ - void pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize, bool look_for_zero); + void pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize); }; typedef obj_ref interval_set_ref; diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 7a9aa864c..62101e777 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -4,8 +4,6 @@ def_module_params('nlsat', export=True, params=(max_memory_param(), ('cell_sample', BOOL, True, "cell sample projection"), - ('look_for_zero_witness', BOOL, True, "look for 0 witness"), - ('lazy', UINT, 0, "how lazy the solver is."), ('reorder', BOOL, True, "reorder variables."), ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"), diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 1ce6435b9..9f43b7a78 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -218,7 +218,6 @@ namespace nlsat { bool m_inline_vars; bool m_log_lemmas; bool m_check_lemmas; - bool m_look_for_0_witness; unsigned m_max_conflicts; unsigned m_lemma_count; @@ -290,7 +289,6 @@ namespace nlsat { m_inline_vars = p.inline_vars(); m_log_lemmas = p.log_lemmas(); m_check_lemmas = p.check_lemmas(); - m_look_for_0_witness = p.look_for_zero_witness(); m_ism.set_seed(m_random_seed); m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_minimize_cores(min_cores); @@ -1520,7 +1518,7 @@ namespace nlsat { void select_witness() { scoped_anum w(m_am); SASSERT(!m_ism.is_full(m_infeasible[m_xk])); - m_ism.pick_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize, m_look_for_0_witness); + m_ism.pick_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize); TRACE("nlsat", tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n"; tout << "assigning "; m_display_var(tout, m_xk) << "(x" << m_xk << ") -> " << w << "\n";);