remove option look_for_0_witness

Signed-off-by: Lev Nachmanson <[email protected]>
Z3Prover · Aug 11, 2024 · 839594a · 839594a
1 parent 0306eff
commit 839594a
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 23 deletions.
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
@@ -703,32 +703,32 @@ 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);
             return;
         }
         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
@@ -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, interval_set_manager> interval_set_ref;

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