port look for 0 witness

Signed-off-by: Lev Nachmanson <[email protected]>

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

src/nlsat/nlsat_interval_set.h

@@ -21,14 +21,15 @@ Revision History:
 #include "nlsat/nlsat_types.h"
 
 namespace nlsat {
-
+      
     class interval_set;
 
     class interval_set_manager {
         anum_manager &           m_am;
         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;

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

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