From 8d2b65b20bafa7cb016d44e9799047ecda4196fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 19:18:44 -0700 Subject: [PATCH] add options to allow testing the effect of non-linear hammers Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 5 ++++- src/smt/params/theory_arith_params.cpp | 6 ++++++ src/smt/params/theory_arith_params.h | 3 +++ src/smt/theory_arith_nl.h | 6 +++++- 4 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f059dccb8..9fcda7f64 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -78,7 +78,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 7f3f1ca23..9bc830dd1 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 526cb6f09..f78086300 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/theory_arith_nl.h b/src/smt/theory_arith_nl.h index f44516cad..ae0af89ec 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: