diff options
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 34 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 46 |
2 files changed, 64 insertions, 16 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e2ee99ceb..ee2461c23 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -35,6 +35,24 @@ namespace CVC4 { namespace theory { namespace quantifiers { +std::ostream& operator<<(std::ostream& out, RewriteStep s) +{ + switch (s) + { + case COMPUTE_ELIM_SYMBOLS: out << "COMPUTE_ELIM_SYMBOLS"; break; + case COMPUTE_MINISCOPING: out << "COMPUTE_MINISCOPING"; break; + case COMPUTE_AGGRESSIVE_MINISCOPING: + out << "COMPUTE_AGGRESSIVE_MINISCOPING"; + break; + case COMPUTE_PROCESS_TERMS: out << "COMPUTE_PROCESS_TERMS"; break; + case COMPUTE_PRENEX: out << "COMPUTE_PRENEX"; break; + case COMPUTE_VAR_ELIMINATION: out << "COMPUTE_VAR_ELIMINATION"; break; + case COMPUTE_COND_SPLIT: out << "COMPUTE_COND_SPLIT"; break; + default: out << "UnknownRewriteStep"; break; + } + return out; +} + bool QuantifiersRewriter::isLiteral( Node n ){ switch( n.getKind() ){ case NOT: @@ -166,7 +184,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; RewriteStatus status = REWRITE_DONE; Node ret = in; - int rew_op = -1; + RewriteStep rew_op = COMPUTE_LAST; //get the body if( in.getKind()==EXISTS ){ std::vector< Node > children; @@ -185,7 +203,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { //compute attributes QAttributes qa; QuantAttributes::computeQuantAttributes( in, qa ); - for( int op=0; op<COMPUTE_LAST; op++ ){ + for (unsigned i = 0; i < COMPUTE_LAST; ++i) + { + RewriteStep op = static_cast<RewriteStep>(i); if( doOperation( in, op, qa ) ){ ret = computeOperation( in, op, qa ); if( ret!=in ){ @@ -1978,7 +1998,10 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg return mkForAll( args, body, qa ); } -bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){ +bool QuantifiersRewriter::doOperation(Node q, + RewriteStep computeOption, + QAttributes& qa) +{ bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant() == options::UserPatMode::TRUST; @@ -2021,7 +2044,10 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q } //general method for computing various rewrites -Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){ +Node QuantifiersRewriter::computeOperation(Node f, + RewriteStep computeOption, + QAttributes& qa) +{ Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl; std::vector< Node > args; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ 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: |