From: Andrew Reynolds Date: Sat, 30 Mar 2013 22:29:34 +0000 (-0500) Subject: do simple ite rewriting within quantifiers X-Git-Tag: cvc5-1.0.0~7359 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b016602db8b9beb1f28f144979ab98beb119a59;p=cvc5.git do simple ite rewriting within quantifiers --- 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; imkNode( 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 ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 75b392e15..73f5d391f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -46,6 +46,7 @@ private: static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); static Node computeNNF( Node body ); + static Node computeSimpleIteLift( Node body ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); @@ -54,6 +55,7 @@ private: COMPUTE_MINISCOPING = 0, COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, + COMPUTE_SIMPLE_ITE_LIFT, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF,