diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-28 13:35:09 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-28 13:35:09 -0600 |
commit | a975f3af51a3730f5b848d2b55f9c6d4027fe763 (patch) | |
tree | 4f316ccd61625375f7a8fd92811e6f8f76b49b18 /src/theory/quantifiers/quantifiers_rewriter.h | |
parent | 5c844f064cf6394030918c32f42d0764703b9786 (diff) |
Use enum for quantifiers rewrite steps (#3840)
Makes trace messages easier to understand.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 46 |
1 files changed, 34 insertions, 12 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 69e057c76..ac87f944c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -27,6 +27,34 @@ namespace quantifiers { struct QAttributes; +/** + * List of steps used by the quantifiers rewriter, details on these steps + * can be found in the class below. + */ +enum RewriteStep +{ + /** Eliminate symbols (e.g. implies, xor) */ + COMPUTE_ELIM_SYMBOLS = 0, + /** Miniscoping */ + COMPUTE_MINISCOPING, + /** Aggressive miniscoping */ + COMPUTE_AGGRESSIVE_MINISCOPING, + /** + * Term processing (e.g. simplifying terms based on ITE conditions, + * eliminating extended arithmetic symbols). + */ + COMPUTE_PROCESS_TERMS, + /** Prenexing */ + COMPUTE_PRENEX, + /** Variable elimination */ + COMPUTE_VAR_ELIMINATION, + /** Conditional splitting */ + COMPUTE_COND_SPLIT, + /** Placeholder for end of steps */ + COMPUTE_LAST +}; +std::ostream& operator<<(std::ostream& out, RewriteStep s); + class QuantifiersRewriter : public TheoryRewriter { public: @@ -183,24 +211,18 @@ class QuantifiersRewriter : public TheoryRewriter static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); private: - enum{ - COMPUTE_ELIM_SYMBOLS = 0, - COMPUTE_MINISCOPING, - COMPUTE_AGGRESSIVE_MINISCOPING, - COMPUTE_PROCESS_TERMS, - COMPUTE_PRENEX, - COMPUTE_VAR_ELIMINATION, - COMPUTE_COND_SPLIT, - COMPUTE_LAST - }; - static Node computeOperation( Node f, int computeOption, QAttributes& qa ); + static Node computeOperation(Node f, + RewriteStep computeOption, + QAttributes& qa); + public: RewriteResponse preRewrite(TNode in) override; RewriteResponse postRewrite(TNode in) override; private: /** options */ - static bool doOperation( Node f, int computeOption, QAttributes& qa ); + static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa); + private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: |