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

port look for 0 witness

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-08-06 18:25:31 -10:00 committed by Lev Nachmanson
parent a09e412cf0
commit 0306eff692
4 changed files with 58 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
src/nlsat/nlsat_interval_set.cpp
View file

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

5
src/nlsat/nlsat_interval_set.h
View file

@ -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<char> 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, interval_set_manager> interval_set_ref;

6
src/nlsat/nlsat_params.pyg
View file

@ -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.")
))

4
src/nlsat/nlsat_solver.cpp
View file

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