From 0306eff6928cbb2bdb9983a80e105abd35d78a85 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 6 Aug 2024 18:25:31 -1000
Subject: [PATCH] port look for 0 witness
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/nlsat/nlsat_interval_set.cpp | 70 ++++++++++++++++++++++----------
src/nlsat/nlsat_interval_set.h | 5 ++-
src/nlsat/nlsat_params.pyg | 6 ++-
src/nlsat/nlsat_solver.cpp | 4 +-
4 files changed, 58 insertions(+), 27 deletions(-)
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<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;
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";);