diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index f928fd5b6..0c15d580b 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -684,33 +684,50 @@ namespace nlsat { return new_set; } - void interval_set_manager::peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) { + int compare_interval_with_zero(const interval &now, const scoped_anum &zero, anum_manager & m) { + if (!now.m_upper_inf) { + int sgn = m.compare(now.m_upper, zero); + if (sgn < 0) + return -1; + if (sgn == 0 && now.m_upper_open) + return -1; + } + if (!now.m_lower_inf) { + int sgn = m.compare(now.m_lower, zero); + if (sgn > 0) + return 1; + if (sgn == 0 && now.m_lower_open) + return 1; + } + return 0; + } + + + void interval_set_manager::pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize, bool look_for_zero) { SASSERT(!is_full(s)); if (s == nullptr) { - if (randomize) { - int num = m_rand() % 2 == 0 ? 1 : -1; -#define MAX_RANDOM_DEN_K 4 - int den_k = (m_rand() % MAX_RANDOM_DEN_K); - int den = is_int ? 1 : (1 << den_k); - scoped_mpq _w(m_am.qm()); - m_am.qm().set(_w, num, den); - m_am.set(w, _w); - } - else { - m_am.set(w, 0); - } + m_am.set(w, 0); return; } - unsigned n = 0; - unsigned num = num_intervals(s); - if (!s->m_intervals[0].m_lower_inf) { - // lower is not -oo - n++; - m_am.int_lt(s->m_intervals[0].m_lower, w); - if (!randomize) - return; + 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 ; + } } if (!s->m_intervals[num-1].m_upper_inf) { // upper is not oo @@ -720,6 +737,16 @@ namespace nlsat { if (!randomize) return; } + + if (!s->m_intervals[0].m_lower_inf) { + // lower is not -oo + n++; + m_am.int_lt(s->m_intervals[0].m_lower, w); + if (!randomize) + return; + } + + // Try to find a gap that is not an unit. for (unsigned i = 1; i < num; i++) { @@ -770,5 +797,4 @@ namespace nlsat { out << "*"; return out; } - }; diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h index f1055118f..33b741ebd 100644 --- a/src/nlsat/nlsat_interval_set.h +++ b/src/nlsat/nlsat_interval_set.h @@ -21,7 +21,7 @@ Revision History: #include "nlsat/nlsat_types.h" namespace nlsat { - + class interval_set; class interval_set_manager { @@ -29,6 +29,7 @@ namespace nlsat { small_object_allocator & m_allocator; svector m_already_visited; random_gen m_rand; + void del(interval_set * s); public: interval_set_manager(anum_manager & m, small_object_allocator & a); @@ -107,7 +108,7 @@ namespace nlsat { \pre !is_full(s) */ - void peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize); + void pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize, bool look_for_zero); }; typedef obj_ref interval_set_ref; diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index dec3fac94..7a9aa864c 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -3,6 +3,9 @@ def_module_params('nlsat', description='nonlinear solver', 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"), @@ -14,7 +17,6 @@ def_module_params('nlsat', ('shuffle_vars', BOOL, False, "use a random variable order."), ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"), ('seed', UINT, 0, "random seed."), - ('factor', BOOL, True, "factor polynomials produced during conflict resolution."), - ('cell_sample', BOOL, True, "cell sample projection"), + ('factor', BOOL, True, "factor polynomials produced during conflict resolution.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 3d38d7a5e..1ce6435b9 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -218,6 +218,7 @@ 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; @@ -289,6 +290,7 @@ 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); @@ -1518,7 +1520,7 @@ namespace nlsat { void select_witness() { scoped_anum w(m_am); SASSERT(!m_ism.is_full(m_infeasible[m_xk])); - m_ism.peek_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize); + m_ism.pick_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize, m_look_for_0_witness); 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";);