enable optional failure in levelwise

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/nlsat/levelwise.cpp

@@ -32,6 +32,8 @@ static void vec_setx(std_vector<T>& v, unsigned idx, T val, T def) {
 
 namespace nlsat {
 
+    struct nullified_poly_exception {};
+
     // The three projection modes for a level:
     // 1. section_biggest_cell: Sample is on a root. All disc/lc added.
     // 2. sector_biggest_cell:  Sample between roots. noLdcf optimization only.
@@ -55,6 +57,8 @@ namespace nlsat {
 
         unsigned               m_level = 0;      // current level being processed
         unsigned               m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree
+        bool                   m_null_fail = false;
+        bool                   m_fail = false;
         unsigned               m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc
         unsigned               m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case
 
@@ -260,6 +264,7 @@ namespace nlsat {
                 m_I.emplace_back(m_pm);
 
             m_spanning_tree_threshold = m_solver.lws_spt_threshold();
+            m_null_fail = m_solver.lws_null_fail();
         }
 
         // Handle a polynomial whose every coefficient evaluates to zero at the sample.
@@ -267,6 +272,8 @@ namespace nlsat {
         // request_factorized each of them and continue to the next level.
         // When a non-vanishing derivative is found, request_factorized it and stop.
         void handle_nullified_poly(polynomial_ref const& p) {
+            if (m_null_fail)
+                throw nullified_poly_exception();
             // Add all coefficients of p (w.r.t. m_level) to m_todo.
             unsigned deg = m_pm.degree(p, m_level);
             for (unsigned j = 0; j <= deg; ++j) {
@@ -1295,7 +1302,7 @@ namespace nlsat {
             }
         }
 
-        std_vector<root_function_interval> single_cell() {
+        std_vector<root_function_interval> single_cell_work() {
             TRACE(lws,             
                   tout << "Input polynomials (" << m_P.size() << "):\n";
                   for (unsigned i = 0; i < m_P.size(); ++i)
@@ -1342,6 +1349,16 @@ namespace nlsat {
 
             return m_I;
         }
+
+        std_vector<root_function_interval> single_cell() {
+            try {
+                return single_cell_work();
+            }
+            catch (nullified_poly_exception&) {
+                m_fail = true;
+                return m_I;
+            }
+        }
     };
 
     levelwise::levelwise(
@@ -1360,6 +1377,7 @@ namespace nlsat {
         return m_impl->single_cell();
     }
 
+    bool levelwise::failed() const { return m_impl->m_fail; }
 
 } // namespace nlsat
 

src/nlsat/levelwise.h

@@ -46,6 +46,7 @@ namespace nlsat {
         levelwise(levelwise const&) = delete;
         levelwise& operator=(levelwise const&) = delete;
         std_vector<root_function_interval> single_cell();
+        bool failed() const;
     };
 
     //

src/nlsat/nlsat_explain.cpp

@@ -1048,6 +1048,8 @@ namespace nlsat {
             
             levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
             auto cell = lws.single_cell();
+            if (lws.failed())
+                return false;
             TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
                                  display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
             // Enumerate all intervals in the computed cell and add literals for each non-trivial interval.

src/nlsat/nlsat_params.pyg

@@ -24,5 +24,6 @@ def_module_params('nlsat',
                           ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
                           ('lws', BOOL, True, "apply levelwise."),
                           ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"),
+                          ('lws_null_fail', BOOL, False, "fail levelwise projection on nullified polynomials and fall back to standard projection."),
                           ('canonicalize', BOOL, True, "canonicalize polynomials.")
                           ))                  

src/nlsat/nlsat_solver.cpp

@@ -251,6 +251,7 @@ namespace nlsat {
         bool m_apply_lws;
         bool m_last_conflict_used_lws = false;  // Track if last conflict explanation used levelwise
         unsigned m_lws_spt_threshold = 3;
+        bool m_lws_null_fail = false;
         imp(solver& s, ctx& c):
             m_ctx(c),
             m_solver(s),
@@ -312,6 +313,7 @@ namespace nlsat {
             m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
             m_apply_lws = p.lws();
             m_lws_spt_threshold = p.lws_spt_threshold();  // 0 disables spanning tree
+            m_lws_null_fail = p.lws_null_fail();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
   
             m_ism.set_seed(m_random_seed);
@@ -4719,5 +4721,7 @@ namespace nlsat {
     bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
     
     unsigned solver::lws_spt_threshold() const { return m_imp->m_lws_spt_threshold; }
-    
+
+    bool solver::lws_null_fail() const { return m_imp->m_lws_null_fail; }
+
 };

src/nlsat/nlsat_solver.h

@@ -249,6 +249,7 @@ namespace nlsat {
         assignment& sample(); 
         bool apply_levelwise() const;
         unsigned lws_spt_threshold() const;
+        bool lws_null_fail() const;
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();