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.cpp | |
| parent | 5c844f064cf6394030918c32f42d0764703b9786 (diff) | |
Use enum for quantifiers rewrite steps (#3840)
Makes trace messages easier to understand.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 34 |
1 files changed, 30 insertions, 4 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++ ){ |