From 3517361a736a96f342e53a0cbd089b297332ca55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 20 Jun 2023 16:10:37 -0700 Subject: [PATCH] Adding some options in support of F* (#6774) * patterns: add option for pattern decomposition (pi.decompose_patterns) True by default, retaining current behavior. * rewriter: add option for sorting of disjunctions (rewriter.sort_disjunctions) True by default, retaining current behavior. --- src/ast/pattern/pattern_inference.cpp | 4 ++++ src/ast/pattern/pattern_inference.h | 1 + src/ast/rewriter/bool_rewriter.cpp | 5 +++-- src/ast/rewriter/bool_rewriter.h | 1 + src/params/bool_rewriter_params.pyg | 1 + src/params/pattern_inference_params.cpp | 2 ++ src/params/pattern_inference_params.h | 1 + src/params/pattern_inference_params_helper.pyg | 1 + 8 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 2fd2b4c82..4391d8bf8 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -109,6 +109,7 @@ pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_ m_le(), m_nested_arith_only(true), m_block_loop_patterns(params.m_pi_block_loop_patterns), + m_decompose_patterns(params.m_pi_decompose_patterns), m_candidates(m), m_pattern_weight_lt(m_candidates_info), m_collect(m, *this), @@ -407,6 +408,9 @@ bool pattern_inference_cfg::pattern_weight_lt::operator()(expr * n1, expr * n2) app* pattern_inference_cfg::mk_pattern(app* candidate) { + if (!m_decompose_patterns) + return m.mk_pattern(candidate); + auto has_var_arg = [&](expr* e) { if (!is_app(e)) return false; diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index c5c8e2e74..8d179ba33 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -70,6 +70,7 @@ class pattern_inference_cfg : public default_rewriter_cfg { expr * const * m_no_patterns; bool m_nested_arith_only; bool m_block_loop_patterns; + bool m_decompose_patterns; struct info { uint_set m_free_vars; diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 95c0950d8..16ecf6473 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -26,6 +26,7 @@ Notes: void bool_rewriter::updt_params(params_ref const & _p) { bool_rewriter_params p(_p); m_flat_and_or = p.flat_and_or(); + m_sort_disjunctions = p.sort_disjunctions(); m_elim_and = p.elim_and(); m_elim_ite = p.elim_ite(); m_local_ctx = p.local_ctx(); @@ -291,7 +292,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args if (st != BR_FAILED) return st; #endif - if (s) { + if (m_sort_disjunctions && s) { ast_lt lt; std::sort(buffer.begin(), buffer.end(), lt); result = m().mk_or(sz, buffer.data()); @@ -329,7 +330,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args, } } if (mk_nflat_or_core(flat_args.size(), flat_args.data(), result) == BR_FAILED) { - if (!ordered) { + if (m_sort_disjunctions && !ordered) { ast_lt lt; std::sort(flat_args.begin(), flat_args.end(), lt); } diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 0693e94ba..1c1e7c60e 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -53,6 +53,7 @@ class bool_rewriter { ast_manager & m_manager; hoist_rewriter m_hoist; bool m_flat_and_or = false; + bool m_sort_disjunctions = true; bool m_local_ctx = false; bool m_elim_and = false; bool m_blast_distinct = false; diff --git a/src/params/bool_rewriter_params.pyg b/src/params/bool_rewriter_params.pyg index c8d7ddbb7..87578470e 100644 --- a/src/params/bool_rewriter_params.pyg +++ b/src/params/bool_rewriter_params.pyg @@ -4,6 +4,7 @@ def_module_params(module_name='rewriter', params=(("ite_extra_rules", BOOL, True, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"), ("flat", BOOL, True, "create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor"), ("flat_and_or", BOOL, True, "create nary applications for and,or"), + ("sort_disjunctions", BOOL, True, "sort subterms in disjunctions"), ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), ('elim_ite', BOOL, True, "eliminate ite in favor of and/or"), ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp index 26f606b63..aac574c6e 100644 --- a/src/params/pattern_inference_params.cpp +++ b/src/params/pattern_inference_params.cpp @@ -23,6 +23,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) { pattern_inference_params_helper p(_p); 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(); m_pi_arith = static_cast(p.arith()); m_pi_use_database = p.use_database(); m_pi_arith_weight = p.arith_weight(); @@ -36,6 +37,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) { void pattern_inference_params::display(std::ostream & out) const { DISPLAY_PARAM(m_pi_max_multi_patterns); DISPLAY_PARAM(m_pi_block_loop_patterns); + DISPLAY_PARAM(m_pi_decompose_patterns); DISPLAY_PARAM(m_pi_arith); DISPLAY_PARAM(m_pi_use_database); DISPLAY_PARAM(m_pi_arith_weight); diff --git a/src/params/pattern_inference_params.h b/src/params/pattern_inference_params.h index d05100759..b037411ec 100644 --- a/src/params/pattern_inference_params.h +++ b/src/params/pattern_inference_params.h @@ -29,6 +29,7 @@ enum arith_pattern_inference_kind { struct pattern_inference_params { unsigned m_pi_max_multi_patterns; bool m_pi_block_loop_patterns; + bool m_pi_decompose_patterns; arith_pattern_inference_kind m_pi_arith; bool m_pi_use_database; unsigned m_pi_arith_weight; diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg index 52c6c653e..cb1f02877 100644 --- a/src/params/pattern_inference_params_helper.pyg +++ b/src/params/pattern_inference_params_helper.pyg @@ -4,6 +4,7 @@ def_module_params(class_name='pattern_inference_params_helper', export=True, params=(('max_multi_patterns', UINT, 0, 'when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern'), ('block_loop_patterns', BOOL, True, 'block looping patterns during pattern inference'), + ('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'), ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),