t

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

src/nlsat/levelwise.cpp

@@ -93,7 +93,7 @@ namespace nlsat {
         anum_manager&                m_am;
         std::vector<property_queue>  m_Q; // the set of properties to prove
         std::vector<property>        m_to_refine; 
-        std::vector<symbolic_interval> m_I; // intervals per level (indexed by variable/level)
+        std::vector<root_function_interval> m_I; // intervals per level (indexed by variable/level)
         bool                         m_fail = false; 
         std::vector<root_function>   m_E; // the ordered root functions on a level
         assignment const & sample() const { return m_solver.sample();}
@@ -104,14 +104,10 @@ namespace nlsat {
         impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am)
             : m_solver(solver), m_P(ps),  m_n(max_x),  m_pm(pm), m_am(am) {
             TRACE(lws, tout  << "m_n:" << m_n << "\n";);
-            // m_I holds one symbolic_interval per level. symbolic_interval is not default
-            // constructible (it requires a polynomial::manager), so using resize() would
-            // attempt to default-construct elements and fail to compile. Instead we
-            // explicitly emplace objects initialized with the polynomial manager.
-            m_I.reserve(m_n);
+            m_I.reserve(m_n); // cannot just resize bcs of the absence of the default constructor of root_function_interval
             for (unsigned i = 0; i < m_n; ++i)
                 m_I.emplace_back(m_pm);
-            m_Q.resize(m_n+1);
+            m_Q.resize(m_n + 1);
         }
         // end constructor
 
@@ -237,11 +233,12 @@ namespace nlsat {
         }
 
         /*
+          See comment 7.1 Generating explanation for MCSAT.
           Return 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 root functions }.
         */
-        void seed_properties() {
+        void init_properties() {
             std::vector<poly*> ps_of_n_level;
             collect_level_properties(ps_of_n_level);
             std::vector<std::pair<scoped_anum, poly*>> root_vals;
@@ -251,10 +248,10 @@ namespace nlsat {
         }
         
 
-        // Compute symbolic interval from sorted roots. Assumes roots are sorted.
+        // Compute root function interval from sorted roots. Assumes roots are sorted.
         void compute_interval_from_sorted_roots( // works on m_level
                                                 std::vector<root_function>& roots,
-                                                symbolic_interval& I) {
+                                                root_function_interval& I) {
             // default: whole line sector (-inf, +inf)
             I.section = false;
             I.l = nullptr; I.u = nullptr; I.l_index = 0; I.u_index = 0;
@@ -401,12 +398,11 @@ namespace nlsat {
             SASSERT(invariant());
             return apply_property_rules(prop_enum::holds, true);
         }
-         // Extracted helper: handle ord_inv(discriminant_{x_{i+1}}(p)) for an_del pre-processing
+         // handle ord_inv(discriminant_{x_{i+1}}(p)) for an_del pre-processing
          void add_ord_inv_discriminant_for(const property& p) {
             polynomial::polynomial_ref disc(m_pm);
             disc = discriminant(p.poly, max_var(p.poly));
-            TRACE(lws, display(tout << "p:", p) << "\n";
-                  ::nlsat::display(tout << "discriminant: ", m_solver, disc) << "\n";);
+            TRACE(lws, display(tout << "p:", p) << "\n"; ::nlsat::display(tout << "discriminant by x" << max_var(p.poly)<< ": ", m_solver, disc) << "\n";);
             if (!is_const(disc)) {
                 for_each_distinct_factor(disc, [&](polynomial::polynomial_ref f) {
                     if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
@@ -420,7 +416,7 @@ namespace nlsat {
             }
          }
 
-        // Extracted helper: handle sgn_inv(leading_coefficient_{x_{i+1}}(p)) for an_del pre-processing
+        //  handle sgn_inv(leading_coefficient_{x_{i+1}}(p)) for an_del pre-processing
         void add_sgn_inv_leading_coeff_for(const property& p) {
             poly * pp = p.poly.get();
             unsigned lvl = max_var(p.poly);
@@ -431,12 +427,12 @@ namespace nlsat {
                 if (!is_const(lc)) {
                     for_each_distinct_factor(lc, [&](polynomial::polynomial_ref f) {
                         if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
-                            NOT_IMPLEMENTED_YET(); // leading coeff vanished as polynomial -- not handled yet
-                        }
-                        else {
-                            unsigned lvl = max_var(f);
-                            mk_prop(prop_enum::sgn_inv, f, lvl);
+                            m_fail = true;
+                            return;
                         }
+                        else
+                            mk_prop(prop_enum::sgn_inv, f, max_var(f));
+                        
                     });
                 }
             }
@@ -664,7 +660,7 @@ or
             if (I.section) {
             /* Rule 4.8. Let i ∈ N>0 , R ⊆ Ri
                , s ∈ R_{i−1}
-               , p ∈ Q[x1, . . . , xi ], level(p) = i, and I be a symbolic interval
+               , p ∈ Q[x1, . . . , xi ], level(p) = i, and I be a root function interval
                of level i. Assume that p is irreducible, and I = (section, b).
                Let Q := an_sub(i − 1)(R) ∧ connected(i − 1)(R) ∧ repr(I, s)(R) ∧ an_del(b.p)(R).
                Q, b.p= p ⊢ sgn_inv(p)(R)
@@ -683,14 +679,16 @@ or
             /*
               Rule 4.10. Let i ∈ N>0 , R ⊆ Ri
               , s ∈ Ri−1
-              , p ∈ Q[x1, . . . , xi ], level(p) = i, I be a symbolic interval of
+              , p ∈ Q[x1, . . . , xi ], level(p) = i, I be a root function interval of
               level i, ≼ be an indexed root ordering of level i, and ≼t be the reflexive and transitive closure of ≼.
               We choose l, u such that either I = (sector, l, u) or (I = (section, b) for b = l = u).
               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 ξ.
               sample(s)(R), repr(I, s)(R), ir_ord(≼, s)(R), an_del(p)(R) ⊢ sgn_inv(p)(R)
             */
-                NOT_IMPLEMENTED_YET();
+                mk_prop(sample_holds, m_level - 1); 
+                mk_prop(repr, m_level - 1);
+                mk_prop(an_del, p.poly, m_level);
             }
         }
 
@@ -768,23 +766,15 @@ or
         }
 
         // return an empty vector on failure, otherwise returns the cell representations with intervals
-        std::vector<symbolic_interval> single_cell() {
-            TRACE(lws,
-                   m_solver.display_assignment(tout << "sample()") << std::endl;
-                   tout << "m_P:\n";
-                   for (const auto & p: m_P) {
-                       ::nlsat::display(tout, m_solver, polynomial_ref(p, m_pm)) << std::endl;
-                       tout << "max_var:" << m_pm.max_var(p) << std::endl;
-                   }
-                 );
+        std::vector<root_function_interval> single_cell() {
+            TRACE(lws, m_solver.display_assignment(tout << "sample()") << std::endl; ::nlsat::display(tout << "m_P:\n", m_solver, m_P) << "\n";);
             m_level = m_n;
-            seed_properties(); // initializes m_Q as the set of properties on levels <= m_n            
+            init_properties(); // initializes m_Q as a queue of properties on levels <= m_n           
             apply_property_rules(prop_enum::_count, false); // reduce the level by one to be consumed by construct_interval
-            while (--m_level > 0) {
+            while (--m_level > 0) 
                 if (!construct_interval())
-                    return std::vector<symbolic_interval>(); // return empty
-            }
-            
+                    return std::vector<root_function_interval>(); // return empty
+                       
             return m_I; // the order of intervals is reversed
         }
         
@@ -812,8 +802,7 @@ or
             }
             return out;
         }
-        
-
+ 
         std::ostream& display(std::ostream& out, const property & pr) const {
             out << "{prop:" << prop_name(pr.prop_tag);
             if (pr.s_idx != -1) out   << ", s_idx:" << pr.s_idx;
@@ -827,8 +816,7 @@ or
             out << "}";
             return out;
         }
-
-        
+       
         std::ostream& display(std::ostream& out, const indexed_root_expr& ire ) const {
             out << "RootExpr: p=";
             ::nlsat::display(out, m_solver, ire.p);
@@ -836,11 +824,9 @@ or
             return out;
         }
 
-        std::ostream& display(std::ostream& out, const symbolic_interval& I) const {
+        std::ostream& display(std::ostream& out, const root_function_interval& I) const {
             return ::nlsat::display(out, m_solver, I);
         }
-
-
     };
 // constructor
     levelwise::levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var n, assignment const& s, pmanager& pm, anum_manager& am)
@@ -848,16 +834,15 @@ or
 
     levelwise::~levelwise() { delete m_impl; }
 
-    std::vector<levelwise::symbolic_interval> levelwise::single_cell() {
+    std::vector<levelwise::root_function_interval> levelwise::single_cell() {
         return m_impl->single_cell();
     }
 
     bool levelwise::failed() const { return m_impl->m_fail; }
-    
 } // namespace nlsat
 
 // Free pretty-printer for symbolic_interval
-std::ostream& nlsat::display(std::ostream& out, solver& s, levelwise::symbolic_interval const& I) {
+std::ostream& nlsat::display(std::ostream& out, solver& s, levelwise::root_function_interval const& I) {
     if (I.section) {
         out << "Section: ";
         if (I.l == nullptr)

src/nlsat/levelwise.h

@@ -11,7 +11,7 @@ namespace nlsat {
             poly* p;
             unsigned i;
         };
-        struct symbolic_interval {
+        struct root_function_interval {
             bool section = false;
             polynomial_ref l;
             unsigned l_index; // the low bound root index
@@ -25,12 +25,12 @@ namespace nlsat {
                 SASSERT(is_section());                
                 return l;
             }
-            symbolic_interval(polynomial::manager & pm):l(pm), u(pm) {}
+            root_function_interval(polynomial::manager & pm):l(pm), u(pm) {}
         };
         // Free pretty-printer declared here so external modules (e.g., nlsat_explain) can
         // display intervals without depending on levelwise internals.
         // Implemented in levelwise.cpp
-        friend std::ostream& display(std::ostream& out, solver& s, symbolic_interval const& I);
+        friend std::ostream& display(std::ostream& out, solver& s, root_function_interval const& I);
             
     private:
 
@@ -44,12 +44,12 @@ namespace nlsat {
 
         levelwise(levelwise const&) = delete;
         levelwise& operator=(levelwise const&) = delete;
-        std::vector<symbolic_interval> single_cell();
+        std::vector<root_function_interval> single_cell();
         bool failed() const;
     };
 
     //
     // Free pretty-printer (non-member) for levelwise::symbolic_interval
-    std::ostream& display(std::ostream& out, solver& s, levelwise::symbolic_interval const& I);
+    std::ostream& display(std::ostream& out, solver& s, levelwise::root_function_interval const& I);
 
 } // namespace nlsat

src/nlsat/nlsat_explain.cpp

@@ -392,6 +392,7 @@ namespace nlsat {
            Remark: root atoms are not normalized
         */
         literal normalize(literal l, var max) {
+            TRACE(nlsat_explain, display(tout << "l:", m_solver, l) << '\n';);
             bool_var b = l.var();
             if (b == true_bool_var)
                 return l;
@@ -481,6 +482,7 @@ namespace nlsat {
            stages) from (arithmetic) literals,
         */
         void normalize(scoped_literal_vector & C, var max) {
+            TRACE(nlsat_explain, display(tout << "C:\n", m_solver, C) << '\n';);
             unsigned sz = C.size();
             unsigned j  = 0;
             for (unsigned i = 0; i < sz; i++) {
@@ -1213,8 +1215,11 @@ namespace nlsat {
          * https://arxiv.org/abs/2003.00409 
          */
         void project_cdcac(polynomial_ref_vector & ps, var max_x) {
-            if (ps.empty())
+            TRACE(nlsat_explain, tout << "max_x:" << max_x << std::endl;);
+            if (ps.empty()) {
+                TRACE(nlsat_explain, tout << "ps.empty\n";);
                 return;
+            }
 
             m_todo.reset();
             for (unsigned i = 0; i < ps.size(); i++) {
@@ -1229,6 +1234,7 @@ 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))
                 return;
 
@@ -1618,8 +1624,10 @@ namespace nlsat {
            \brief Main procedure. The explain the given unsat core, and store the result in m_result
         */
         void main(unsigned num, literal const * ls) {
-            if (num == 0)
+            if (num == 0) {
+                TRACE(nlsat_explain, tout << "num:" << num << "\n";);
                 return;
+            }
             collect_polys(num, ls, m_ps);
             var max_x = max_var(m_ps);
             TRACE(nlsat_explain, tout << "polynomials in the conflict:\n"; display(tout, m_solver, m_ps); tout << "\n";);
@@ -1631,6 +1639,7 @@ namespace nlsat {
 
         void process2(unsigned num, literal const * ls) {
             if (m_simplify_cores) {
+                TRACE(nlsat_explain, tout << "m_simplify_cores is true\n";);
                 m_core2.reset();
                 m_core2.append(num, ls);
                 var max = max_var(num, ls);
@@ -1718,12 +1727,14 @@ namespace nlsat {
 
         void process(unsigned num, literal const * ls) {
             if (m_minimize_cores && num > 1) {
+                TRACE(nlsat_explain, tout << "m_minimize_cores:" << m_minimize_cores << ", num:" << num;);
                 m_core1.reset();
                 minimize(num, ls, m_core1);
                 process2(m_core1.size(), m_core1.data());
                 m_core1.reset();
             }
             else {
+                TRACE(nlsat_explain, tout << "directly to process2\n";);
                 process2(num, ls);
             }
         }
@@ -1741,7 +1752,7 @@ namespace nlsat {
             process(num, ls);
             reset_already_added();
             m_result = nullptr;
-            TRACE(nlsat_explain, display(tout << "[explain] result\n", m_solver, result) << "\n";);
+            TRACE(nlsat_explain, display(tout << "result\n", m_solver, result) << "\n";);
             CASSERT("nlsat", check_already_added());
         }
 

src/nlsat/nlsat_solver.cpp

@@ -2427,6 +2427,7 @@ namespace nlsat {
                                 resolve_clause(b, *(jst.get_clause()));
                                 break;
                             case justification::LAZY:
+                                m_apply_lws = m_stats.m_conflicts == 2;
                                 resolve_lazy_justification(b, *(jst.get_lazy()));
                                 break;
                             case justification::DECISION: