mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
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.
This commit is contained in:
parent
eb1caee18a
commit
3517361a73
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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"),
|
||||
|
|
|
@ -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<arith_pattern_inference_kind>(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);
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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'),
|
||||
|
|
Loading…
Reference in a new issue