mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

remove option look_for_0_witness

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-08-07 09:01:49 -10:00 committed by Lev Nachmanson
parent 0306eff692
commit 839594ac12
4 changed files with 19 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/nlsat/nlsat_interval_set.cpp
View file

@ -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)); SASSERT(!is_full(s));
if (s == nullptr) { if (s == nullptr) {
m_am.set(w, 0); m_am.set(w, 0);
@ -711,24 +711,24 @@ namespace nlsat {
} }
unsigned n = 0; unsigned n = 0;
unsigned num = num_intervals(s); unsigned num = num_intervals(s);
if (look_for_zero) { // try to assign w to zero first to simplify the polynomials
scoped_anum zero(m_am); scoped_anum zero(m_am);
m_am.set(zero, 0); m_am.set(zero, 0);
bool available = true; bool available = true;
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
int sgn = compare_interval_with_zero(s->m_intervals[i], zero, m_am); int sgn = compare_interval_with_zero(s->m_intervals[i], zero, m_am);
if (sgn == 0) { if (sgn == 0) {
available = false; available = false;
break; break;
}
if (sgn > 0)
break;
}
if (available) {
m_am.set(w, 0);
return ;
} }
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) { if (!s->m_intervals[num-1].m_upper_inf) {
// upper is not oo // upper is not oo
n++; n++;

2
src/nlsat/nlsat_interval_set.h
View file

@ -108,7 +108,7 @@ namespace nlsat {
\pre !is_full(s) \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, interval_set_manager> interval_set_ref; typedef obj_ref<interval_set, interval_set_manager> interval_set_ref;

2
src/nlsat/nlsat_params.pyg
View file

@ -4,8 +4,6 @@ def_module_params('nlsat',
export=True, export=True,
params=(max_memory_param(), params=(max_memory_param(),
('cell_sample', BOOL, True, "cell sample projection"), ('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."), ('lazy', UINT, 0, "how lazy the solver is."),
('reorder', BOOL, True, "reorder variables."), ('reorder', BOOL, True, "reorder variables."),
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"), ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),

4
src/nlsat/nlsat_solver.cpp
View file

@ -218,7 +218,6 @@ namespace nlsat {
bool m_inline_vars; bool m_inline_vars;
bool m_log_lemmas; bool m_log_lemmas;
bool m_check_lemmas; bool m_check_lemmas;
bool m_look_for_0_witness;
unsigned m_max_conflicts; unsigned m_max_conflicts;
unsigned m_lemma_count; unsigned m_lemma_count;
@ -290,7 +289,6 @@ namespace nlsat {
m_inline_vars = p.inline_vars(); m_inline_vars = p.inline_vars();
m_log_lemmas = p.log_lemmas(); m_log_lemmas = p.log_lemmas();
m_check_lemmas = p.check_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_ism.set_seed(m_random_seed);
m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_simplify_cores(m_simplify_cores);
m_explain.set_minimize_cores(min_cores); m_explain.set_minimize_cores(min_cores);
@ -1520,7 +1518,7 @@ namespace nlsat {
void select_witness() { void select_witness() {
scoped_anum w(m_am); scoped_anum w(m_am);
SASSERT(!m_ism.is_full(m_infeasible[m_xk])); 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", TRACE("nlsat",
tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n"; 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";); tout << "assigning "; m_display_var(tout, m_xk) << "(x" << m_xk << ") -> " << w << "\n";);