From 99cbfa715c184b9ecfe1d2da2edd15951cac8623 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Feb 2025 13:58:51 -0800 Subject: [PATCH] Add a sharp throttle to lia2card tactic to control overhead in default tactic mode lia2card was added to qfuflia tactic based on a user scenario, but it overshot: lia2card is by default harmful. It is here tamed to only convert binary variables and throttle on nested ite terms --- src/params/tactic_params.pyg | 2 ++ src/tactic/arith/lia2card_tactic.cpp | 23 ++++++++++++++--------- src/tactic/smtlogics/qflia_tactic.cpp | 9 ++++++++- 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/src/params/tactic_params.pyg b/src/params/tactic_params.pyg index 3870e90ad4e..1614987ddfa 100644 --- a/src/params/tactic_params.pyg +++ b/src/params/tactic_params.pyg @@ -9,6 +9,8 @@ def_module_params('tactic', ('blast_term_ite.max_inflation', UINT, UINT_MAX, "multiplicative factor of initial term size."), ('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."), ('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."), + ('lia2card.max_range', UINT, 100, "maximal range of integers to compilation into Booleans"), + ('lia2card.max_ite_nesting', UINT, 4, "maximal nesting depth for ite expressions to be compiled into PB constraints"), ('default_tactic', SYMBOL, '', "overwrite default tactic in strategic solver"), # ('aig.per_assertion', BOOL, True, "process one assertion at a time"), diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index e298e30e31b..a5524d13a9c 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -25,6 +25,7 @@ Module Name: #include "ast/ast_util.h" #include "ast/ast_pp_util.h" #include "tactic/tactical.h" +#include "params/tactic_params.hpp" #include "ast/simplifiers/bound_manager.h" #include "ast/converters/generic_model_converter.h" @@ -116,7 +117,8 @@ class lia2card_tactic : public tactic { mutable ptr_vector* m_todo; bounds_map m_bounds; bool m_compile_equality; - unsigned m_max_ub; + unsigned m_max_range = 101; + unsigned m_max_ite_nesting = 1; ref m_mc; lia2card_tactic(ast_manager & _m, params_ref const & p): @@ -126,7 +128,7 @@ class lia2card_tactic : public tactic { m_pb(m), m_todo(alloc(ptr_vector)), m_compile_equality(true) { - m_max_ub = 100; + updt_params(p); } ~lia2card_tactic() override { @@ -137,7 +139,11 @@ class lia2card_tactic : public tactic { void updt_params(params_ref const & p) override { m_params.append(p); + tactic_params tp(p); + m_compile_equality = m_params.get_bool("compile_equality", true); + m_max_range = tp.lia2card_max_range(); + m_max_ite_nesting = tp.lia2card_max_ite_nesting(); } expr_ref mk_bounded(expr_ref_vector& axioms, app* x, unsigned lo, unsigned hi) { @@ -152,7 +158,6 @@ class lia2card_tactic : public tactic { if (lo > 0) { xs.push_back(a.mk_int(lo)); } - verbose_stream() << "bounded " << lo << " " << hi << "\n"; for (unsigned i = lo; i < hi; ++i) { checkpoint(); @@ -193,7 +198,7 @@ class lia2card_tactic : public tactic { if (a.is_int(x) && is_uninterp_const(x) && bounds.has_lower(x, lo, s1) && !s1 && lo.is_unsigned() && - bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() - lo.get_unsigned() <= m_max_ub) { + bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() - lo.get_unsigned() <= m_max_range) { expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned()); rep.insert(x, b); m_bounds.insert(x, bound(lo.get_unsigned(), hi.get_unsigned(), b)); @@ -288,11 +293,14 @@ class lia2card_tactic : public tactic { rational r, q; if (!is_app(x)) return false; - if (nesting > 8) + if (nesting > m_max_ite_nesting && !is_numeral(x, r)) return false; app* f = to_app(x); bool ok = true; - if (a.is_add(x)) { + if (is_numeral(x, r)) { + insert_arg(mul * r, conds, m.mk_true(), args, coeffs, coeff); + } + else if (a.is_add(x)) { for (unsigned i = 0; ok && i < f->get_num_args(); ++i) { ok = get_sum(nesting, f->get_arg(i), mul, conds, args, coeffs, coeff); } @@ -321,9 +329,6 @@ class lia2card_tactic : public tactic { ok &= get_sum(nesting + 1, u, mul, conds, args, coeffs, coeff); conds.pop_back(); } - else if (is_numeral(x, r)) { - insert_arg(mul*r, conds, m.mk_true(), args, coeffs, coeff); - } else { TRACE("pb", tout << "Can't handle " << mk_pp(x, m) << "\n";); ok = false; diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 981127faba0..e728a33ac29 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -192,6 +192,11 @@ tactic * mk_preamble_tactic(ast_manager& m) { ctx_simp_p.set_uint("max_depth", 30); ctx_simp_p.set_uint("max_steps", 5000000); + // only binary integer variables are converted to PB + params_ref lia2card_p; + lia2card_p.set_uint("lia2card.max_range", 1); + lia2card_p.set_uint("lia2card.max_ite_nesting", 1); + return and_then( mk_simplify_tactic(m), @@ -199,7 +204,7 @@ tactic * mk_preamble_tactic(ast_manager& m) { using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_simplify_tactic(m), pull_ite_p), mk_solve_eqs_tactic(m), - mk_lia2card_tactic(m), + mk_lia2card_tactic(m, lia2card_p), mk_elim_uncnstr_tactic(m)); } @@ -209,6 +214,8 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { main_p.set_bool("som", true); main_p.set_bool("blast_distinct", true); main_p.set_uint("blast_distinct_threshold", 128); + main_p.set_uint("lia2card.max_range", 1); + main_p.set_uint("lia2card.max_ite_nesting", 1); // main_p.set_bool("push_ite_arith", true); params_ref quasi_pb_p;