mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

make der selective to configuration. For F*, quantifiers are hand or machine generated in specific formats and the tool depends on e-matching to use precisely the format of the quantifiers that have been entered. For other cases of quantifiers, destructive equality resolution (der) can be expected to offer simplifications

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-06 16:15:04 -07:00
parent 81068981aa
commit 68f43ac7a4
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/th_rewriter.cpp
View file

@ -74,6 +74,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bool m_push_ite_bv = true;
bool m_ignore_patterns_on_ground_qbody = true;
bool m_rewrite_patterns = true;
bool m_enable_der = true;
ast_manager & m() const { return m_b_rw.m(); }
@ -89,6 +90,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_push_ite_bv = p.push_ite_bv();
m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
m_rewrite_patterns = p.rewrite_patterns();
m_enable_der = p.enable_der();
}
void updt_params(params_ref const & p) {
@ -827,11 +829,17 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr_ref r(m());
bool der_change = false;
if (is_quantifier(result) && to_quantifier(result)->get_num_patterns() == 0) {
if (m_enable_der && is_quantifier(result) && to_quantifier(result)->get_num_patterns() == 0) {
m_der(to_quantifier(result), r, p2);
der_change = result.get() != r.get();
if (m().proofs_enabled() && der_change)
result_pr = m().mk_transitivity(result_pr, p2);
result_pr = m().mk_transitivity(result_pr, p2);
if (der_change) {
verbose_stream() << result << "\n";
verbose_stream() << "==>\n";
verbose_stream() << r << "\n";
}
result = r;
}

1
src/params/rewriter_params.pyg
View file

@ -8,6 +8,7 @@ def_module_params('rewriter',
("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
("cache_all", BOOL, False, "cache all intermediate results."),
("enable_der", BOOL, True, "enable destructive equality resolution to quantifiers."),
("rewrite_patterns", BOOL, False, "rewrite patterns."),
("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))