add parameter to suppress/enable levelwise

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

src/nlsat/levelwise.cpp

@@ -155,12 +155,9 @@ namespace nlsat {
           - For factors with level == m_n: add an_del(p) and isolate their indexed roots over the sample;
           sort those roots and for each adjacent pair coming from distinct polynomials add
           ord_inv(resultant(p_j, p_{j+1})) to Q.
-          - If any constructed polynomial (resultant, discriminant, etc.) is nullified on the sample,
+          - If any constructed polynomial is nullified on the sample, that is all coefficients are zeroes, then fail.
-          fail immediately.
 
-          Result: Q = { sgn_inv(p) | level(p) < m_n }
+          Result: Q = { sgn_inv(p) | level(p) < m_n } ∪ { an_del(p)  | level(p) == m_n } ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
-          ∪ { an_del(p)  | level(p) == m_n }
-          ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
         */
         // Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
         void collect_level_properties(std::vector<poly*> & ps_of_n_level) {
@@ -342,8 +339,6 @@ namespace nlsat {
              }
 
              collect_E(p_non_null);
-             // Ensure m_I can hold interval for this level
-             SASSERT(m_I.size() > m_level);
              std::sort(m_E.begin(), m_E.end(), [&](root_function const& a, root_function const& b){
                  return m_am.lt(a.val, b.val);
              });

src/nlsat/nlsat_explain.cpp

@@ -1229,28 +1229,29 @@ namespace nlsat {
             
             var x = m_todo.extract_max_polys(ps);
 
-            if (!levelwise_single_cell(ps, max_x)) { // on levelwise_single_cell failure continue with cdcac
+            if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x))
-                polynomial_ref_vector samples(m_pm);
+                return;
+
+            polynomial_ref_vector samples(m_pm);
             
-                if (x < max_x)
+            if (x < max_x)
-                    cac_add_cell_lits(ps, x);
+                cac_add_cell_lits(ps, x);
             
-                while (true) {
+            while (true) {
-                    if (all_univ(ps, x) && m_todo.empty()) {
+                if (all_univ(ps, x) && m_todo.empty()) {
-                        m_todo.reset();
+                    m_todo.reset();
-                        break;
+                    break;
-                    }
-                    TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x); tout << "\npolynomials\n";
-                          display(tout, m_solver, ps); tout << "\n";);
-                    add_lcs(ps, x);
-                    psc_discriminant(ps, x);
-                    psc_resultant(ps, x);
-                
-                    if (m_todo.empty())
-                        break;
-                    x = m_todo.extract_max_polys(ps);
-                    cac_add_cell_lits(ps, x);
                 }
+                TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x); tout << "\npolynomials\n";
+                      display(tout, m_solver, ps); tout << "\n";);
+                add_lcs(ps, x);
+                psc_discriminant(ps, x);
+                psc_resultant(ps, x);
+                
+                if (m_todo.empty())
+                    break;
+                x = m_todo.extract_max_polys(ps);
+                cac_add_cell_lits(ps, x);
             }
         }
 
@@ -1731,9 +1732,10 @@ namespace nlsat {
             SASSERT(check_already_added());
             SASSERT(num > 0);
             TRACE(nlsat_explain, 
-                  tout << "[explain] set of literals is infeasible in the current interpretation\n"; 
+                  tout << "the infeasible clause:\n"; 
                   display(tout, m_solver, num, ls) << "\n";
-                  m_solver.display_assignment(tout);
+                  
+                  m_solver.display_assignment(tout << "assignment:\n");
                   );
             m_result = &result;
             process(num, ls);

src/nlsat/nlsat_params.pyg

@@ -19,5 +19,6 @@ def_module_params('nlsat',
                           ('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."),
-                          ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only")
+                          ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
+                          ('apply_levelwise', BOOL, True, "apply levelwise.")
                           ))         

src/nlsat/nlsat_solver.cpp

@@ -242,7 +242,7 @@ namespace nlsat {
         // statistics
         stats                  m_stats;
         std::string m_debug_known_solution_file_name;
-
+        bool m_apply_lws;
         imp(solver& s, ctx& c):
             m_ctx(c),
             m_solver(s),
@@ -300,6 +300,7 @@ namespace nlsat {
             m_check_lemmas   = p.check_lemmas();
             m_variable_ordering_strategy = p.variable_ordering_strategy();
             m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
+            m_apply_lws = p.apply_levelwise();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
             m_cell_sample = p.cell_sample();
   
@@ -4397,6 +4398,7 @@ namespace nlsat {
     assumption solver::join(assumption a, assumption b) {
         return (m_imp->m_asm.mk_join(static_cast<imp::_assumption_set>(a), static_cast<imp::_assumption_set>(b)));
     }
-    
+
+    bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
         
 };

src/nlsat/nlsat_solver.h

@@ -246,7 +246,7 @@ namespace nlsat {
         static void collect_param_descrs(param_descrs & d);
         const assignment& sample() const;
         assignment& sample(); 
-
+        bool apply_levelwise() const;
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();