From 58e64ea8264b42feb5a9c824bd4f3944aed65616 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 22 Oct 2025 17:00:16 -0700 Subject: [PATCH] try exponential delay in grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.cpp | 17 +++++++++++++++-- src/params/smt_params_helper.pyg | 2 +- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 89396b41f..f0db19649 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -47,9 +47,22 @@ namespace nla { if (m_quota == 0) m_quota = c().params().arith_nl_gr_q(); + bool const use_exp_delay = c().params().arith_nl_grobner_exp_delay(); + if (m_quota == 1) { - m_delay_base++; - m_delay = m_delay_base; + if (use_exp_delay) { + constexpr unsigned delay_cap = 1000000; + if (m_delay_base == 0) + m_delay_base = 1; + else if (m_delay_base < delay_cap) { + m_delay_base *= 2; + if (m_delay_base > delay_cap) + m_delay_base = delay_cap; + } + m_delay = m_delay_base; + } + else + m_delay = ++m_delay_base; m_quota = c().params().arith_nl_gr_q(); } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 487772c81..e0d02c6d2 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -80,6 +80,7 @@ def_module_params(module_name='smt', ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'), ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'), + ('arith.nl.grobner_exp_delay', BOOL, False, 'use exponential delay between grobner basis attempts'), ('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, True, 'expand terms before computing grobner basis'), @@ -138,4 +139,3 @@ def_module_params(module_name='smt', ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'), ('qsat_use_qel', BOOL, True, 'Use QEL for lite quantifier elimination and model-based projection in QSAT') )) -