diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 35 |
1 files changed, 14 insertions, 21 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fcd8d1829..2b7e19c48 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -55,7 +55,6 @@ bool QuantifiersRewriter::isLiteral( Node n ){ case IMPLIES: case XOR: case ITE: - case IFF: return false; break; case EQUAL: @@ -251,7 +250,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { k = OR; negCh1 = true; }else if( ok==XOR ){ - k = IFF; + k = EQUAL; negCh1 = true; }else if( ok==NOT ){ if( body[0].getKind()==NOT ){ @@ -265,9 +264,9 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { k = OR; negAllCh = true; body = body[0]; - }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){ - k = IFF; - negCh1 = ( body[0].getKind()==IFF ); + }else if( body[0].getKind()==XOR || ( body[0].getKind()==EQUAL && body[0][0].getType().isBoolean() ) ){ + k = EQUAL; + negCh1 = ( body[0].getKind()==EQUAL ); body = body[0]; }else if( body[0].getKind()==ITE ){ k = body[0].getKind(); @@ -277,7 +276,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { }else{ return body; } - }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){ + }else if( ( ok!=EQUAL || !body[0].getType().isBoolean() ) && ok!=ITE && ok!=AND && ok!=OR ){ //a literal return body; } @@ -410,8 +409,8 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ }else if( res==-1 ){ return getEntailedCond( n[2], currCond ); } - }else if( n.getKind()==IFF || n.getKind()==ITE ){ - unsigned start = n.getKind()==IFF ? 0 : 1; + }else if( ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) || n.getKind()==ITE ){ + unsigned start = n.getKind()==EQUAL ? 0 : 1; int res1 = 0; for( unsigned j=start; j<=(start+1); j++ ){ int res = getEntailedCond( n[j], currCond ); @@ -423,7 +422,7 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ Assert( res!=0 ); if( n.getKind()==ITE ){ return res1==res ? res : 0; - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==EQUAL ){ return res1==res ? 1 : -1; } } @@ -512,7 +511,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Assert( !body.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( h.getType().isBoolean() ? IFF : EQUAL, h, r ) ); + return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) ); }else{ return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); } @@ -773,7 +772,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ } } if( options::condVarSplitQuant() ){ - if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){ + if( body.getKind()==ITE || ( body.getKind()==EQUAL && body[0].getType().isBoolean() && options::condVarSplitQuantAgg() ) ){ Assert( !qa.isFunDef() ); Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl; bool do_split = false; @@ -1100,7 +1099,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); return computePrenex( nn, args, nargs, pol, prenexAgg ); - }else if( prenexAgg && body.getKind()==kind::IFF ){ + }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){ Node nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); @@ -1631,11 +1630,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { case kind::RR_REWRITE: // Equality pattern.push_back( head ); - if( head.getType().isBoolean() ){ - body = head.iffNode(body); - }else{ - body = head.eqNode(body); - } + body = head.eqNode(body); break; case kind::RR_REDUCTION: case kind::RR_DEDUCTION: @@ -1780,7 +1775,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v //check if it contains a quantifier as a subterm //if so, we will write this node if( containsQuantifiers( n ) ){ - if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){ + if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ if( options::preSkolemQuantAgg() ){ Node nn; //must remove structure @@ -1788,12 +1783,10 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + }else if( n.getKind()==kind::EQUAL ){ nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); } return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); } |