diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f23579521..e821e26bd 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1307,6 +1307,10 @@ lbool core::check() { if (no_effect()) m_monomial_bounds.propagate(); + + if (no_effect() && refine_pseudo_linear()) + return l_false; + { std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; @@ -1519,6 +1523,54 @@ void core::simplify() { } +bool core::is_pseudo_linear(monic const& m) const { + bool has_unbounded = false; + for (auto v : m.vars()) { + if (lra.column_is_bounded(v) && lra.var_is_int(v)) { + auto lb = lra.get_lower_bound(v); + auto ub = lra.get_upper_bound(v); + if (ub - lb <= rational(4)) + continue; + } + if (has_unbounded) + return false; + has_unbounded = true; + } + return true; +} + +bool core::refine_pseudo_linear() { + if (!params().arith_nl_reduce_pseudo_linear()) + return false; + for (lpvar j : m_to_refine) { + if (is_pseudo_linear(m_emons[j])) { + refine_pseudo_linear(m_emons[j]); + return true; + } + } + return false; +} + +void core::refine_pseudo_linear(monic const& m) { + lemma_builder lemma(*this, "nla-pseudo-linear"); + lpvar nlvar = null_lpvar; + rational prod(1); + for (auto v : m.vars()) { + if (lra.column_is_bounded(v) && lra.var_is_int(v)) { + auto lb = lra.get_lower_bound(v); + auto ub = lra.get_upper_bound(v); + if (ub - lb <= rational(4)) { + lemma |= ineq(v, llc::NE, val(v)); + prod *= val(v); + continue; + } + } + SASSERT(nlvar == null_lpvar); + nlvar = v; + } + lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0)); + // lemma.display(verbose_stream() << "pseudo-linear lemma\n"); +} diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 0291ed673..fa5da5a81 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -111,7 +111,9 @@ class core { void check_weighted(unsigned sz, std::pair>* checks); void add_bounds(); - + bool refine_pseudo_linear(); + bool is_pseudo_linear(monic const& m) const; + void refine_pseudo_linear(monic const& m); public: // constructor diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 5f24f6119..f16d61815 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -841,22 +841,6 @@ namespace nla { m_solver.add(p, dep); } - bool grobner::is_pseudo_linear(unsigned_vector const& vars) const { - bool has_unbounded = false; - for (auto v : vars) { - if (c().lra.column_is_bounded(v) && c().lra.var_is_int(v)) { - auto lb = c().lra.get_lower_bound(v); - auto ub = c().lra.get_upper_bound(v); - if (ub - lb <= rational(4)) - continue; - } - if (has_unbounded) - return false; - has_unbounded = true; - } - return true; - } - void grobner::add_fixed_monic(unsigned j) { u_dependency* dep = nullptr; dd::pdd r = m_pdd_manager.mk_val(rational(1)); @@ -882,8 +866,7 @@ namespace nla { TRACE(grobner, for (lpvar j : c().m_to_refine) print_monic(c().emons()[j], tout) << "\n";); for (lpvar j : c().m_to_refine) - if (!is_pseudo_linear(c().emons()[j].vars())) - q.push_back(j); + q.push_back(j); while (!q.empty()) { lpvar j = q.back(); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 40e09305d..19f0e3687 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -79,7 +79,7 @@ namespace nla { void add_fixed_monic(unsigned j); bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r); void add_eq(dd::pdd& p, u_dependency* dep); - bool is_pseudo_linear(unsigned_vector const& vars) const; + bool is_pseudo_linear(monic const& m) const; const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep); dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep); dd::pdd pdd_expr(lp::lar_term const& t, u_dependency*& dep); diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index df84d6515..1ae97d72e 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -83,13 +83,14 @@ def_module_params(module_name='smt', ('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.grobner_expand_terms', BOOL, False, 'expand terms before computing grobner basis'), - ('arith.nl.delay', UINT, 10, '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.nl.log', BOOL, False, 'Log lemmas sent to nra solver'), + ('arith.nl.reduce_pseudo_linear', BOOL, False, 'create incremental linearization axioms for pseudo-linear monomials'), + ('arith.nl.delay', UINT, 10, '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.nl.log', BOOL, False, 'Log lemmas sent to nra solver'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), - ('arith.epsilon', DOUBLE, 1.0, 'initial value of epsilon used for model generation of infinitesimals'), + ('arith.epsilon', DOUBLE, 1.0, 'initial value of epsilon used for model generation of infinitesimals'), ('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'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), @@ -102,7 +103,7 @@ def_module_params(module_name='smt', ('arith.rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info'), ('arith.min', BOOL, False, 'minimize cost'), ('arith.print_stats', BOOL, False, 'print statistic'), - ('arith.validate', BOOL, False, 'validate lemmas generated by arithmetic solver'), + ('arith.validate', BOOL, False, 'validate lemmas generated by arithmetic solver'), ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'), ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'), ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),