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

add some comments to elim_predicates

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-19 19:45:25 +07:00
parent 251d49d133
commit c3c45f495a
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/simplifiers/eliminate_predicates.cpp
View file

@ -18,9 +18,17 @@ The simplifier
and we can obbtain {a, C}, {b, C} {~a, ~b, D } similar to propositional case. and we can obbtain {a, C}, {b, C} {~a, ~b, D } similar to propositional case.
Instead the case is handled by predicate elimination when p only occurs positively Instead the case is handled by predicate elimination when p only occurs positively
outside of {~p, a} {~p, b} {p, ~a, ~b} outside of {~p, a} {~p, b} {p, ~a, ~b}
The SAT based definition detection scheme creates clauses
{a}, {b}, {~a,~b}, C, D and checks for an unsat core.
The core {a}, {b}, {~a, ~b} maps back to a definition for p
Then {p, C}, {~p, D} clauses are replaced based on the definition.
(a task for a "Kitten"?)
- Handle various permutations of variables that are arguments to p?
- other SMT-based macro detection could be made here as well. - other SMT-based macro detection could be made here as well.
The (legacy) macro finder is not very flexible and could be replaced The (legacy) macro finder is not very flexible and could be replaced
by a module building on this one. by a module building on this one.
- eliminates predicates p(x) that occur at most once in each clause and the - eliminates predicates p(x) that occur at most once in each clause and the
number of occurrences is small. number of occurrences is small.
@ -76,6 +84,7 @@ struct eliminate_predicates::macro_expander_cfg : public default_rewriter_cfg {
/** /**
* adapted from macro_manager.cpp * adapted from macro_manager.cpp
* Perhaps hoist and combine?
*/ */
bool reduce_quantifier(quantifier* old_q, bool reduce_quantifier(quantifier* old_q,
expr* new_body, expr* new_body,
@ -131,6 +140,7 @@ struct eliminate_predicates::macro_expander_cfg : public default_rewriter_cfg {
r = rr; r = rr;
m_trail.push_back(rr); m_trail.push_back(rr);
m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, dep); m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, dep);
// skip proof terms for simplifiers
return true; return true;
} }