Add a sharp throttle to lia2card tactic to control overhead in defaul…

…t 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

@@ -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"),

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<expr>*        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<generic_model_converter>     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<expr>)),
         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;

src/tactic/smtlogics/qflia_tactic.cpp

@@ -192,14 +192,19 @@ 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),
             mk_propagate_values_tactic(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;