diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-02 20:57:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 20:57:58 -0500 |
commit | bbfb310eba34ae078ee2601c7e5ea2b56dbe1252 (patch) | |
tree | 665707ebb7d940357317594ebf8ca01ff92ba60c /src/theory/quantifiers/quantifiers_rewriter.h | |
parent | 6dd4efeea9fa0d9975fcffecd5af03bc081b68e7 (diff) |
Use prenex normal form when using cegqi-nested-qe (#4522)
Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.
This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2a3180e78..c8995ef4e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -234,8 +234,27 @@ class QuantifiersRewriter : public TheoryRewriter static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); + /** + * This function removes top-level quantifiers from subformulas of body + * appearing with overall polarity pol. It adds quantified variables that + * appear in positive polarity positions into args, and those at negative + * polarity positions in nargs. + * + * If prenexAgg is true, we ensure that all top-level quantifiers are + * eliminated from subformulas. This means that we must expand ITE and + * Boolean equalities to ensure that quantifiers are at fixed polarities. + * + * For example, calling this function on: + * (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z)))) + * would return: + * (or (P x z) (not (Q y z))) + * and add {x} to args, and {y} to nargs. + */ static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); - static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ); + /** + * Apply prenexing aggressively. Returns the prenex normal form of n. + */ + static Node computePrenexAgg(Node n, std::map<Node, Node>& visited); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); private: static Node computeOperation(Node f, |