diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-05 17:23:41 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-05 17:23:41 +0200 |
commit | 8b189c3f51d2272ecbda57e367d2bd1af34fb94d (patch) | |
tree | b78759e65d102a4cd01ab5a9ca6cfc13eb457795 /src/theory/quantifiers | |
parent | 7adf1f2ba37912da65d86d811dd1fd9d572fc747 (diff) |
Minor fix : do not drop instantiation patterns when merging quantifiers.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 4c01e927d..1a20693f9 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -159,7 +159,13 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { } Node body = in[1]; bool doRewrite = false; + std::vector< Node > ipl; while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){ + if( body.getNumChildren()==3 ){ + for( unsigned i=0; i<body[2].getNumChildren(); i++ ){ + ipl.push_back( body[2][i] ); + } + } for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ args.push_back( body[0][i] ); } @@ -171,7 +177,12 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) ); children.push_back( body ); if( in.getNumChildren()==3 ){ - children.push_back( in[2] ); + for( unsigned i=0; i<in[2].getNumChildren(); i++ ){ + ipl.push_back( in[2][i] ); + } + } + if( !ipl.empty() ){ + children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, ipl ) ); } Node n = NodeManager::currentNM()->mkNode( in.getKind(), children ); if( in!=n ){ |