add stats to track levelwise calls

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

src/nlsat/levelwise.cpp

@@ -214,19 +214,8 @@ namespace nlsat {
             return out;
         }
 
-        bool is_irreducible(poly* p) {
+        bool is_square_free(poly* p) {
-            polynomial_ref_vector factors(m_pm);
+            return m_pm.is_square_free(p);            
-            polynomial_ref pref(p, m_pm);
-            ::nlsat::factor(pref, m_cache, factors);
-            unsigned num_factors = factors.size();
-            CTRACE(lws, num_factors != 1, ::nlsat::display(tout, m_solver, p) << std::endl;
-                   tout << "{";
-                   tout << "num_factors:" << num_factors << "\n";
-                   ::nlsat::display(tout, m_solver, factors);
-                   tout << "}\n";
-                );
-            
-            return factors.size() == 1;            
         }
         
         /*
@@ -533,7 +522,7 @@ namespace nlsat {
          // add a property to m_Q if an equivalent one is not already present.
          // Equivalence: same m_prop_tag and same level; polynomials checked for equality
          // (polynomials are already in primitive form, so constant multipliers are normalized away).
-        void add_to_Q_if_new(const property & pr, unsigned level) {
+        void add_to_Q_if_new(const property & pr, unsigned level) {            
              SASSERT(pr.m_prop_tag != ord_inv || (pr.m_poly && !m_pm.is_zero(pr.m_poly)));
              for (auto const & q : m_Q[level]) {
                  if (q.m_prop_tag != pr.m_prop_tag) continue;
@@ -542,7 +531,7 @@ namespace nlsat {
                  TRACE(lws, display(tout << "matched q:", q) << std::endl;);
                  return;
              }
-             SASSERT(!pr.m_poly || is_irreducible(pr.m_poly));
+             SASSERT(!pr.m_poly || is_square_free(pr.m_poly));
              m_Q[level].push(pr);
          }
         
@@ -829,7 +818,7 @@ or
         }
 
         void apply_pre_sgn_inv(const property& p) {
-            SASSERT(is_irreducible(p.m_poly));
+            SASSERT(is_square_free(p.m_poly));
             scoped_anum_vector roots(m_am);
             SASSERT(max_var(p.m_poly) == m_level);
             m_am.isolate_roots(p.m_poly, undef_var_assignment(sample(), m_level), roots);
@@ -893,7 +882,7 @@ or
         /*Assume that p is irreducible, irExpr(p, s) ̸= ∅, ξ.p is irreducible for all ξ ∈ dom(≼), ≼ matches s,
               and for all ξ ∈ irExpr(p, s) it holds either ξ ≼t l or u ≼t ξ.*/
         bool precondition_on_sign_inv(const property &p) {
-            SASSERT(is_irreducible(p.m_poly));
+            SASSERT(is_square_free(p.m_poly));
             SASSERT(max_var(p.m_poly) == m_level);
 
             return true;
@@ -908,7 +897,7 @@ or
           p(s)= 0, sample(s)(R), an_sub(i− 1)(R), connected(i)(R), sgn_inv(p)(R), an_del(p)(R) ⊢ ord_inv(p)(R)
         */
         void apply_pre_ord_inv(const property& p) {
-            SASSERT(p.m_prop_tag == prop_enum::ord_inv && is_irreducible(p.m_poly));
+            SASSERT(p.m_prop_tag == prop_enum::ord_inv && is_square_free(p.m_poly));
             unsigned level = max_var(p.m_poly);
             auto sign_on_sample = sign(p.m_poly, sample(), m_am);
             mk_prop(sample_holds, level_t(level));

src/nlsat/nlsat_explain.cpp

@@ -1144,11 +1144,13 @@ namespace nlsat {
             var x = m_todo.extract_max_polys(ps);
 
             TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";);
-            if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x, m_cache)) {
+            if (m_solver.apply_levelwise()) {
-                std::cout << "s";
+                bool levelwise_ok = levelwise_single_cell(ps, max_x, m_cache);
-                return;
+                m_solver.record_levelwise_result(levelwise_ok);
+                if (levelwise_ok)
+                    return;
+
             }
-            std::cout << "f";
             polynomial_ref_vector samples(m_pm);
             
             if (x < max_x)

src/nlsat/nlsat_solver.cpp

@@ -239,6 +239,8 @@ namespace nlsat {
             unsigned               m_decisions;
             unsigned               m_stages;
             unsigned               m_irrational_assignments; // number of irrational witnesses
+            unsigned               m_levelwise_calls;
+            unsigned               m_levelwise_successes;
             void reset() { memset(this, 0, sizeof(*this)); }
             stats() { reset(); }
         };
@@ -2750,6 +2752,8 @@ namespace nlsat {
             st.update("nlsat stages", m_stats.m_stages);
             st.update("nlsat simplifications", m_stats.m_simplifications);
             st.update("nlsat irrational assignments", m_stats.m_irrational_assignments);
+            st.update("levelwise calls", m_stats.m_levelwise_calls);
+            st.update("levelwise successes", m_stats.m_levelwise_successes);
         }
 
         void reset_statistics() {
@@ -4613,6 +4617,12 @@ namespace nlsat {
         m_imp->m_stats.m_simplifications++;
     }
 
+    void solver::record_levelwise_result(bool success) {
+        m_imp->m_stats.m_levelwise_calls++;
+        if (success)
+            m_imp->m_stats.m_levelwise_successes++;
+    }
+
     bool solver::has_root_atom(clause const& c) const {
         return m_imp->has_root_atom(c);
     }

src/nlsat/nlsat_solver.h

@@ -194,6 +194,7 @@ namespace nlsat {
         assumption join(assumption a, assumption b);
 
         void inc_simplify();
+        void record_levelwise_result(bool success);
         void add_bound(bound_constraint const& c);
 
         /**
@@ -300,4 +301,3 @@ namespace nlsat {
     };
 
 };
-