diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 0788510efb1..fe4c1a29a19 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1855,6 +1855,7 @@ bool core::is_linear(const svector& 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 explain_dep) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index a6bc6b3b4a1..b2bb6b34889 100644 --- a/src/math/lp/nla_core.h +++ b/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& 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& vars, lpvar non_fixed, const rational& k); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index ab9f56c9641..fca7fcacf8e 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/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'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 7f3f1ca23ce..9bc830dd17c 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/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(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); } diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 526cb6f0907..f7808630044 100644 --- a/src/smt/params/theory_arith_params.h +++ b/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()) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7a267fdeca1..f9560cb01cd 100644 --- a/src/smt/smt_context.h +++ b/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 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; } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index fe86c68113c..3925a4e2151 100644 --- a/src/smt/smt_context_pp.cpp +++ b/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; } diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index f44516cad0f..ae0af89ec55 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -902,6 +902,8 @@ bool theory_arith::propagate_linear_monomial(theory_var v) { */ template bool theory_arith::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::gb_result theory_arith::compute_grobner(svector */ template bool theory_arith::max_min_nl_vars() { + if (!m_params.m_nl_arith_optimize_bounds) + return true; var_set already_found; svector vars; for (theory_var v : m_nl_monomials) { @@ -2360,7 +2364,7 @@ final_check_status theory_arith::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: diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index c7ff5b2561c..4e1dde11aae 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/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; - 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; - 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; - 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); */ }