Merge branch 'master' into unit_prop_on_monomials

src/math/lp/nla_core.cpp

@@ -1855,6 +1855,7 @@ bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed)
         }
     }
     return n_of_non_fixed <= 1;
+
 }
 
 void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep) {

src/math/lp/nla_core.h

@@ -398,8 +398,6 @@ class core {
     void check_bounded_divisions();
 
     bool  no_lemmas_hold() const;
-
-    // void propagate();
 
     lbool  test_check();
     lpvar map_to_root(lpvar) const;
@@ -435,6 +433,7 @@ class core {
     void set_use_nra_model(bool m);
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
+
     bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed);
     void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var);
     void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);

src/smt/params/smt_params_helper.pyg

@@ -80,7 +80,10 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                           ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
                           ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),   
-	                  ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),                       
+	                  ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
+			  ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
+			  ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
+			  ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),

src/smt/params/theory_arith_params.cpp

@@ -36,6 +36,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
     m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
     m_arith_auto_config_simplex = p.arith_auto_config_simplex();
+    m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
+    m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
+    m_nl_arith_cross_nested = p.arith_nl_cross_nested();
 
     arith_rewriter_params ap(_p);
     m_arith_eq2ineq = ap.eq2ineq();
@@ -89,4 +92,7 @@ void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_nl_arith_max_degree);
     DISPLAY_PARAM(m_nl_arith_branching);
     DISPLAY_PARAM(m_nl_arith_rounds);
+    DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials);
+    DISPLAY_PARAM(m_nl_arith_optimize_bounds);
+    DISPLAY_PARAM(m_nl_arith_cross_nested);
 }

src/smt/params/theory_arith_params.h

@@ -105,6 +105,9 @@ struct theory_arith_params {
     unsigned                m_nl_arith_max_degree = 6;
     bool                    m_nl_arith_branching = true;
     unsigned                m_nl_arith_rounds = 1024;
+    bool                    m_nl_arith_propagate_linear_monomials = true;
+    bool                    m_nl_arith_optimize_bounds = true;
+    bool                    m_nl_arith_cross_nested = true;
 
 
     theory_arith_params(params_ref const & p = params_ref()) {

src/smt/smt_context.h

@@ -134,7 +134,6 @@ namespace smt {
             enode *                 m_lhs;
             enode *                 m_rhs;
             eq_justification        m_justification;
-            new_eq() {}
             new_eq(enode * lhs, enode * rhs, eq_justification const & js):
                 m_lhs(lhs), m_rhs(rhs), m_justification(js) {}
         };
@@ -143,7 +142,6 @@ namespace smt {
             theory_id  m_th_id;
             theory_var m_lhs;
             theory_var m_rhs;
-            new_th_eq():m_th_id(null_theory_id), m_lhs(null_theory_var), m_rhs(null_theory_var) {}
             new_th_eq(theory_id id, theory_var l, theory_var r):m_th_id(id), m_lhs(l), m_rhs(r) {}
         };
         svector<new_th_eq>          m_th_eq_propagation_queue;
@@ -215,7 +213,7 @@ namespace smt {
         // -----------------------------------
         proto_model_ref            m_proto_model;
         model_ref                  m_model;
-        std::string                m_unknown;
+        const char *               m_unknown;
         void                       mk_proto_model();
         void                       reset_model() { m_model = nullptr; m_proto_model = nullptr; }
 

src/smt/smt_context_pp.cpp

@@ -66,6 +66,7 @@ namespace smt {
     std::string context::last_failure_as_string() const {
         std::string r;
         switch(m_last_search_failure) {
+        case UNKNOWN:
         case OK: r = m_unknown; break;
         case MEMOUT: r = "memout"; break;
         case CANCELED: r = "canceled"; break;
@@ -82,7 +83,6 @@ namespace smt {
         case RESOURCE_LIMIT: r = "(resource limits reached)"; break;
         case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
         case LAMBDAS: r = "(incomplete lambdas)"; break;
-        case UNKNOWN: r = m_unknown; break;
         }
         return r;
     }

src/smt/theory_arith_nl.h

@@ -902,6 +902,8 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_linear_monomials() {
+    if (!m_params.m_nl_arith_propagate_linear_monomials)
+        return false;
     if (!reflection_enabled())
         return false;
     TRACE("non_linear", tout << "propagating linear monomials...\n";);
@@ -2278,6 +2280,8 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
 */
 template<typename Ext>
 bool theory_arith<Ext>::max_min_nl_vars() {
+    if (!m_params.m_nl_arith_optimize_bounds)
+        return true;
     var_set             already_found;
     svector<theory_var> vars;
     for (theory_var v : m_nl_monomials) {
@@ -2360,7 +2364,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
             }
             break;
         case 1:
-            if (!is_cross_nested_consistent(vars))
+            if (m_params.m_nl_arith_cross_nested && !is_cross_nested_consistent(vars))
                 progress = true;
             break;
         case 2:

src/test/lp/nla_solver_test.cpp

@@ -197,6 +197,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
     auto const& lemmas = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemmas.back(), std::cout);
 
+
     ineq i0(lp_ac, llc::NE, 1);
     lp::lar_term t1, t2;
     t1.add_var(lp_bde);
@@ -399,7 +400,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
 
     VERIFY(nla.get_core().test_check() == l_false);
     auto const& lemma = nla.get_core().lemmas();
-    
+
     nla.get_core().print_lemma(lemma.back(), std::cout);
 
     ineq i0(lp_a, llc::EQ, 0);
@@ -476,7 +477,6 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
     s_set_column_value_test(s, lp_d,  rational(3));
     VERIFY(nla.get_core().test_check() == l_false);
     auto const& lemma = nla.get_core().lemmas();
-
 
     nla.get_core().print_lemma(lemma.back(), std::cout);
     ineq i0(lp_d, llc::EQ, 1);
@@ -714,9 +714,9 @@ void test_order_lemma_params(bool var_equiv, int sign) {
         s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij)
                            + rational(1));
     }
-    vector<lemma> lemma;
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     // lp::lar_term t;
     // t.add_monomial(lp_bde);
     // t.add_monomial(lp_acd);
@@ -800,8 +800,8 @@ void test_monotone_lemma() {
     // set ef = ij while it has to be ef > ij
     s_set_column_value_test(s, lp_ef, s.get_column_value(lp_ij));
 
-    vector<lemma> lemma;
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemma.back(), std::cout);
     */
 }
@@ -859,8 +859,7 @@ void test_tangent_lemma_reg() {
     nla.add_monic(lp_ab, vec.size(), vec.begin());
 
     VERIFY(nla.get_core().test_check() == l_false);
-    auto const& lemma = nla.get_core().lemmas();
-    nla.get_core().print_lemma(lemma.back(), std::cout);
+    nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
 }
 
 void test_tangent_lemma_equiv() {
@@ -904,10 +903,9 @@ void test_tangent_lemma_equiv() {
     int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
     
     s_set_column_value_test(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
-    vector<lemma> lemma;
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
-    nla.get_core().print_lemma(lemma.back(), std::cout);
+    VERIFY(nla.get_core().test_check() == l_false);
+    nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
     */
 }