diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 235 |
1 files changed, 189 insertions, 46 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0afdece82..6a95e243d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -340,64 +340,141 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } } + +void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, + std::vector< Node >& conj ){ + if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Node x = n[0][0]; + std::map< Node, Node >::iterator itp = pcons.find( x ); + if( itp!=pcons.end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl; + computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj ); + }else{ + Expr testerExpr = n[0].getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + std::map< int, Node >::iterator itn = ncons[x].find( index ); + if( itn!=ncons[x].end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl; + computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj ); + }else{ + for( unsigned i=0; i<2; i++ ){ + if( i==0 ){ + pcons[x] = n[0]; + }else{ + pcons.erase( x ); + ncons[x][index] = n[0].negate(); + } + computeDtTesterIteSplit( n[i+1], pcons, ncons, conj ); + } + ncons[x].erase( index ); + } + } + }else{ + Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl; + std::vector< Node > children; + children.push_back( n ); + std::vector< Node > vars; + //add all positive testers + for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){ + children.push_back( it->second.negate() ); + vars.push_back( it->first ); + } + //add all negative testers + for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){ + Node x = it->first; + //only if we haven't settled on a positive tester + if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ + //check if we have exhausted all options but one + const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype(); + std::vector< Node > nchildren; + int pos_cons = -1; + for( int i=0; i<(int)dt.getNumConstructors(); i++ ){ + std::map< int, Node >::iterator itt = it->second.find( i ); + if( itt==it->second.end() ){ + pos_cons = pos_cons==-1 ? i : -2; + }else{ + nchildren.push_back( itt->second.negate() ); + } + } + if( pos_cons>=0 ){ + const DatatypeConstructor& c = dt[pos_cons]; + Expr tester = c.getTester(); + children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() ); + }else{ + children.insert( children.end(), nchildren.begin(), nchildren.end() ); + } + } + } + //make condition/output pair + Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + conj.push_back( c ); + } +} + Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) { if( body.getType().isBoolean() ){ - if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){ + if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){ 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( no.getKind()!=ITE ){ + bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL; + 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 ); } - } - if( doRewrite ){ - return NodeManager::currentNM()->mkNode( ITE, children ); } } } - }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){ - for( unsigned r=0; r<2; r++ ){ - //check if there is a variable elimination - Node b = r==0 ? body[0] : body[0].negate(); - QuantPhaseReq qpr( b ); - std::vector< Node > vars; - std::vector< Node > subs; - Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl; - if( it->second ){ - if( it->first.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( it->first[i].getKind()==BOUND_VARIABLE ){ - unsigned j = i==0 ? 1 : 0; - if( !hasArg1( it->first[i], it->first[j] ) ){ - vars.push_back( it->first[i] ); - subs.push_back( it->first[j] ); - break; + }else if( body.getKind()==ITE && hasPol ){ + if( options::iteCondVarSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl; + for( unsigned r=0; r<2; r++ ){ + //check if there is a variable elimination + Node b = r==0 ? body[0] : body[0].negate(); + QuantPhaseReq qpr( b ); + std::vector< Node > vars; + std::vector< Node > subs; + Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl; + if( it->second ){ + if( it->first.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + if( it->first[i].getKind()==BOUND_VARIABLE ){ + unsigned j = i==0 ? 1 : 0; + if( !hasArg1( it->first[i], it->first[j] ) ){ + vars.push_back( it->first[i] ); + subs.push_back( it->first[j] ); + break; + } } } } } } - } - if( !vars.empty() ){ - //bool cpol = (r==1); - Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); - //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - //pos = Rewriter::rewrite( pos ); - Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); - //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl; - //Trace("ite-var-split-quant") << " " << pos << std::endl; - //Trace("ite-var-split-quant") << " " << neg << std::endl; - return NodeManager::currentNM()->mkNode( AND, pos, neg ); + if( !vars.empty() ){ + //bool cpol = (r==1); + Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //pos = Rewriter::rewrite( pos ); + Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); + Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl; + Trace("quantifiers-rewrite-ite") << " " << pos << std::endl; + Trace("quantifiers-rewrite-ite") << " " << neg << std::endl; + return NodeManager::currentNM()->mkNode( AND, pos, neg ); + } } } } @@ -420,6 +497,26 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) return body; } +Node QuantifiersRewriter::computeProcessIte2( Node body ){ + if( body.getKind()==ITE ){ + if( options::iteDtTesterSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; + std::map< Node, Node > pcons; + std::map< Node, std::map< int, Node > > ncons; + std::vector< Node > conj; + computeDtTesterIteSplit( body, pcons, ncons, conj ); + Assert( !conj.empty() ); + if( conj.size()>1 ){ + Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; + for( unsigned i=0; i<conj.size(); i++ ){ + Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl; + } + return NodeManager::currentNM()->mkNode( AND, conj ); + } + } + } + return body; +} Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ @@ -677,6 +774,30 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } +Node QuantifiersRewriter::computeElimTaut( Node body ) { + if( body.getKind()==OR ){ + std::vector< Node > children; + std::map< Node, bool > lit_pol; + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node lit = body[i].getKind()==NOT ? body[i][0] : body[i]; + bool pol = body[i].getKind()!=NOT; + std::map< Node, bool >::iterator it = lit_pol.find( lit ); + if( it==lit_pol.end() ){ + lit_pol[lit] = pol; + children.push_back( body[i] ); + }else{ + if( it->second!=pol ){ + return NodeManager::currentNM()->mkConst( true ); + } + } + } + if( children.size()!=body.getNumChildren() ){ + return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + } + } + return body; +} + Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) { if( body.getKind()==OR ){ size_t var_found_count = 0; @@ -784,7 +905,21 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; - computeArgVec2( args, activeArgs, body, ipl ); + //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables + if( options::ceGuidedInst() && !ipl.isNull() ){ + for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ + Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl; + if( ipl[i].getKind()==INST_ATTRIBUTE ){ + Node avar = ipl[i][0]; + if( avar.getAttribute(SygusAttribute()) ){ + activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); + } + } + } + } + if( activeArgs.empty() ){ + computeArgVec2( args, activeArgs, body, ipl ); + } if( activeArgs.empty() ){ return body; }else{ @@ -1002,9 +1137,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_NNF ){ return options::nnfQuant(); }else if( computeOption==COMPUTE_PROCESS_ITE ){ - return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant(); + return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + return options::iteDtTesterSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + return options::elimTautQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant() || options::dtVarExpandQuant(); }else if( computeOption==COMPUTE_CNF ){ @@ -1041,8 +1180,12 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_ITE ){ n = computeProcessIte( n, true, true ); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + n = computeProcessIte2( n ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + n = computeElimTaut( n ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ Node prev; do{ |