diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-30 17:29:34 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-30 17:29:45 -0500 |
commit | 3b016602db8b9beb1f28f144979ab98beb119a59 (patch) | |
tree | d3536cca03b92a96f3e1b54d14d944fbeb93f871 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 32f19d4e68e90cbae021321d4444be3f868783e5 (diff) |
do simple ite rewriting within quantifiers
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index bf6a025f8..35ab3e647 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -273,6 +273,43 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } } +Node QuantifiersRewriter::computeSimpleIteLift( Node body ) { + if( body.getKind()==EQUAL ){ + for( size_t i=0; i<2; i++ ){ + if( body[i].getKind()==ITE ){ + Node no = i==0 ? body[1] : body[0]; + bool doRewrite = false; + std::vector< Node > children; + children.push_back( body[i][0] ); + for( size_t j=1; j<=2; j++ ){ + //check if it rewrites to a constant + Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); + nn = Rewriter::rewrite( nn ); + children.push_back( nn ); + if( nn.isConst() ){ + doRewrite = true; + } + } + if( doRewrite ){ + return NodeManager::currentNM()->mkNode( ITE, children ); + } + } + } + }else if( body.getKind()!=APPLY_UF && body.getType()==NodeManager::currentNM()->booleanType() ){ + bool changed = false; + std::vector< Node > children; + for( size_t i=0; i<body.getNumChildren(); i++ ){ + Node nn = computeSimpleIteLift( body[i] ); + children.push_back( nn ); + changed = changed || nn!=body[i]; + } + if( changed ){ + return NodeManager::currentNM()->mkNode( body.getKind(), children ); + } + } + return body; +} + Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ Trace("var-elim-quant") << "Compute var elimination for " << body << std::endl; QuantPhaseReq qpr( body ); @@ -521,6 +558,8 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) ); }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); + }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ + n = computeSimpleIteLift( n ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -771,6 +810,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption return options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) + }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ + return true; }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ |