From 4d9af7848dcbb51293ba3002875b3e63c4c5733b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2023 15:27:37 -0700 Subject: [PATCH] add parameter to disable pattern inference #6884 Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/pattern_inference.cpp | 9 +++++---- src/params/pattern_inference_params.cpp | 2 ++ src/params/pattern_inference_params.h | 11 +++++------ src/params/pattern_inference_params_helper.pyg | 1 + 4 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 4391d8bf8..7c7576c84 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -624,9 +624,11 @@ bool pattern_inference_cfg::reduce_quantifier( proof_ref & result_pr) { TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";); - if (!is_forall(q)) { + if (!m_params.m_pi_enabled) + return false; + + if (!is_forall(q)) return false; - } int weight = q->get_weight(); @@ -653,9 +655,8 @@ bool pattern_inference_cfg::reduce_quantifier( } } - if (q->get_num_patterns() > 0) { + if (q->get_num_patterns() > 0) return false; - } if (m_params.m_pi_nopat_weight >= 0) weight = m_params.m_pi_nopat_weight; diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp index aac574c6e..0e548c896 100644 --- a/src/params/pattern_inference_params.cpp +++ b/src/params/pattern_inference_params.cpp @@ -21,6 +21,7 @@ Revision History: void pattern_inference_params::updt_params(params_ref const & _p) { pattern_inference_params_helper p(_p); + m_pi_enabled = p.enabled(); m_pi_max_multi_patterns = p.max_multi_patterns(); m_pi_block_loop_patterns = p.block_loop_patterns(); m_pi_decompose_patterns = p.decompose_patterns(); @@ -35,6 +36,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) { #define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void pattern_inference_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_pi_enabled); DISPLAY_PARAM(m_pi_max_multi_patterns); DISPLAY_PARAM(m_pi_block_loop_patterns); DISPLAY_PARAM(m_pi_decompose_patterns); diff --git a/src/params/pattern_inference_params.h b/src/params/pattern_inference_params.h index b037411ec..e558a6a7b 100644 --- a/src/params/pattern_inference_params.h +++ b/src/params/pattern_inference_params.h @@ -27,7 +27,8 @@ enum arith_pattern_inference_kind { }; struct pattern_inference_params { - unsigned m_pi_max_multi_patterns; + bool m_pi_enabled = true; + unsigned m_pi_max_multi_patterns = 1; bool m_pi_block_loop_patterns; bool m_pi_decompose_patterns; arith_pattern_inference_kind m_pi_arith; @@ -35,13 +36,11 @@ struct pattern_inference_params { unsigned m_pi_arith_weight; unsigned m_pi_non_nested_arith_weight; bool m_pi_pull_quantifiers; - int m_pi_nopat_weight; - bool m_pi_avoid_skolems; + int m_pi_nopat_weight = -1; + bool m_pi_avoid_skolems = true; bool m_pi_warnings; - pattern_inference_params(params_ref const & p = params_ref()): - m_pi_nopat_weight(-1), - m_pi_avoid_skolems(true) { + pattern_inference_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg index cb1f02877..80d36e3ec 100644 --- a/src/params/pattern_inference_params_helper.pyg +++ b/src/params/pattern_inference_params_helper.pyg @@ -7,6 +7,7 @@ def_module_params(class_name='pattern_inference_params_helper', ('decompose_patterns', BOOL, True, 'allow decomposition of patterns into multipatterns'), ('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'), ('use_database', BOOL, False, 'use pattern database'), + ('enabled', BOOL, True, 'enable a heuristic to infer patterns, when they are not provided'), ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'), ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'), ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),