diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
commit | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (patch) | |
tree | 57cee5cddf68999e20553ee9746f4a83183e8b99 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 576d50ac7c13233a589771401537b587eb36361e (diff) |
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 79c300401..5aae4d640 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -244,17 +244,21 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { ret = ret.negate(); status = REWRITE_AGAIN_FULL; }else if( in.getKind()==FORALL ){ - //compute attributes - QAttributes qa; - TermDb::computeQuantAttributes( in, qa ); - if( !qa.isRewriteRule() ){ - for( int op=0; op<COMPUTE_LAST; op++ ){ - if( doOperation( in, op, qa ) ){ - ret = computeOperation( in, op, qa ); - if( ret!=in ){ - rew_op = op; - status = REWRITE_AGAIN_FULL; - break; + if( in[1].isConst() ){ + return RewriteResponse( status, in[1] ); + }else{ + //compute attributes + QAttributes qa; + TermDb::computeQuantAttributes( in, qa ); + if( !qa.isRewriteRule() ){ + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, op, qa ) ){ + ret = computeOperation( in, op, qa ); + if( ret!=in ){ + rew_op = op; + status = REWRITE_AGAIN_FULL; + break; + } } } } |