Debug (#4415)

* fix it explanation.h

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

* fix explanation.h

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

* add options to run bound propagation on monomials etc.

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

src/math/lp/explanation.h

@@ -65,7 +65,7 @@ public:
     public:
         cimpq(constraint_index var, const optional<mpq> & val) : m_var(var), m_coeff(val) { }
         constraint_index ci() const { return m_var; }
-        mpq coeff() const { return m_coeff.undef()? one_of_type<mpq>(): *m_coeff; }
+        mpq coeff() const { return m_coeff.initialized()? *m_coeff: one_of_type<mpq>(); }
     };
     class iterator {
         u_map<optional<mpq>>::iterator m_it; 

src/math/lp/nla_core.cpp

@@ -1396,15 +1396,13 @@ lbool core::check(vector<lemma>& l_vec) {
 
     set_use_nra_model(false);    
 
-    if (false && l_vec.empty() && !done()) 
+    if (l_vec.empty() && !done() && m_nla_settings.propagate_bounds()) 
         m_monomial_bounds();
     
-    if (l_vec.empty() && !done() && need_to_call_algebraic_methods()) 
+    if (l_vec.empty() && !done() && need_run_horner()) 
         m_horner.horner_lemmas();
 
-    if (l_vec.empty() && !done() && m_nla_settings.run_grobner()) {
+    if (l_vec.empty() && !done() && need_run_grobner()) {
-        clear_and_resize_active_var_set(); 
-        find_nl_cluster();
         run_grobner();                
     }
 
@@ -1492,6 +1490,9 @@ void core::run_grobner() {
     if (quota == 1) {
         return;
     }
+    clear_and_resize_active_var_set(); 
+    find_nl_cluster();
+
     lp_settings().stats().m_grobner_calls++;
     configure_grobner();
     m_pdd_grobner.saturate();

src/math/lp/nla_core.h

@@ -229,8 +229,12 @@ public:
     lpvar var(const factor& f) const { return f.var(); }
 
     // returns true if the combination of the Horner's schema and Grobner Basis should be called
-    bool need_to_call_algebraic_methods() const { 
+    bool need_run_horner() const { 
-	    return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; 
+        return m_nla_settings.run_horner() && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; 
+    }
+
+    bool need_run_grobner() const { 
+        return m_nla_settings.run_grobner() && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; 
     }
     
     void incremental_linearization(bool);

src/math/lp/nla_settings.h

@@ -28,7 +28,10 @@ class nla_settings {
     unsigned m_grobner_max_simplified;
     unsigned m_grobner_number_of_conflicts_to_report;
     unsigned m_grobner_quota;
+    unsigned m_grobner_frequency;
     bool     m_run_nra;
+    // propagate bounds
+    bool     m_bp;
 public:
     nla_settings() : m_run_order(true),
                      m_run_tangents(true),
@@ -40,8 +43,12 @@ public:
                      m_grobner_row_length_limit(50),
                      m_grobner_subs_fixed(false),
                      m_grobner_quota(0),
-                     m_run_nra(false)
+                     m_grobner_frequency(4),
+                     m_run_nra(false),
+                     m_bp(false)
     {}
+    bool propagate_bounds() const { return m_bp; }
+    bool& propagate_bounds() { return m_bp; }
     unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;}
     unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;}
     bool run_order() const { return m_run_order; }
@@ -62,6 +69,8 @@ public:
 
     bool run_grobner() const { return m_run_grobner; }
     bool& run_grobner() { return m_run_grobner; }
+    unsigned grobner_frequency() const { return m_grobner_frequency; }
+    unsigned& grobner_frequency() { return m_grobner_frequency; }
 
     bool run_nra() const { return m_run_nra; }
     bool& run_nra() { return m_run_nra; }    

src/smt/params/smt_params_helper.pyg

@@ -48,11 +48,13 @@ def_module_params(module_name='smt',
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'),
                           ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),
                           ('arith.nl.order', BOOL, True, 'run order lemmas'),
+                          ('arith.nl.bp', BOOL, False, 'propagate bounds on monomials'),
                           ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
                           ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
                           ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
                           ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),
                           ('arith.nl.horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
+                          ('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'),
                           ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'),
                           ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
                           ('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'),

src/smt/theory_lra.cpp

@@ -412,6 +412,8 @@ class theory_lra::imp {
             m_nla->settings().grobner_max_simplified() =      prms.arith_nl_grobner_max_simplified();
             m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
             m_nla->settings().grobner_quota() =               prms.arith_nl_gr_q();
+            m_nla->settings().grobner_frequency() =           prms.arith_nl_grobner_frequency();
+            m_nla->settings().propagate_bounds()  =           prms.arith_nl_bp();
         }
     }