diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:25 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:37 +0100 |
commit | 81dca680f6c88d10b56a0ed065d470d907766e21 (patch) | |
tree | 4410fa473ecb6848f7976b2b6a00188ac5e44775 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 50c8533760bfd5b1f803d52bc4318c544521e6af (diff) |
Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 263 |
1 files changed, 201 insertions, 62 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 895408269..dcf58e692 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/trigger.h" using namespace std; using namespace CVC4; @@ -82,6 +83,16 @@ bool QuantifiersRewriter::isCube( Node n ){ } } +int QuantifiersRewriter::getPurifyId( Node n ){ + if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ + return 1; + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){ + return 0; + }else{ + return -1; + } +} + void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ if( n.getKind()==OR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ @@ -758,70 +769,106 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ return body; } +bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { + if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ + return false; + }else{ + if( !var_parent.empty() ){ + std::map< Node, std::vector< int > >::iterator it = var_parent.find( v ); + if( it!=var_parent.end() ){ + Assert( !it->second.empty() ); + int id = getPurifyId( s ); + return it->second.size()==1 && it->second[0]==id; + } + } + return true; + } +} -Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ - Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; - QuantPhaseReq qpr( body ); - std::vector< Node > vars; - std::vector< Node > subs; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; - if( it->first.getKind()==EQUAL ){ - if( it->second && options::varElimQuant() ){ - TypeNode types[2]; - for( int i=0; i<2; i++ ){ - types[i] = it->first[i].getType(); +bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vector< Node >& args, std::vector< Node >& vars, std::vector< Node >& subs, + std::map< Node, std::vector< int > >& var_parent ) { + if( lit.getKind()==EQUAL && pol ){ + for( unsigned i=0; i<2; i++ ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] ); + if( ita!=args.end() ){ + if( isVariableElim( lit[i], lit[1-i], var_parent ) ){ + vars.push_back( lit[i] ); + subs.push_back( lit[1-i] ); + args.erase( ita ); + return true; } - for( int i=0; i<2; i++ ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] ); + } + } + //for arithmetic, solve the equality + if( lit[0].getType().isReal() ){ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( lit, msum ) ){ + for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); if( ita!=args.end() ){ - if( !TermDb::containsTerm( it->first[1-i], it->first[i] ) && types[1-i].isSubtypeOf( types[i] ) ){ - vars.push_back( it->first[i] ); - subs.push_back( it->first[1-i] ); + Node veq_c; + Node val; + int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){ + vars.push_back( itm->first ); + subs.push_back( val ); args.erase( ita ); - break; + return true; } } } - if( !vars.empty() ){ - break; - } } - }else if( it->first.getKind()==APPLY_TESTER ){ - if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){ - Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl; - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] ); - if( ita!=args.end() ){ - vars.push_back( it->first[0] ); - Expr testerExpr = it->first.getOperator().toExpr(); - int index = Datatype::indexOf( testerExpr ); - const Datatype& dt = Datatype::datatypeOf(testerExpr); - const DatatypeConstructor& c = dt[index]; - std::vector< Node > newChildren; - newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); - std::vector< Node > newVars; - for( unsigned j=0; j<c.getNumArgs(); j++ ){ - TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); - tn = tn[1]; - Node v = NodeManager::currentNM()->mkBoundVar( tn ); - newChildren.push_back( v ); - newVars.push_back( v ); - } - subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) ); - Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; - args.erase( ita ); - args.insert( args.end(), newVars.begin(), newVars.end() ); - } - } - }else if( it->first.getKind()==BOUND_VARIABLE ){ - if( options::varElimQuant() ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first ); - if( ita!=args.end() ){ - Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl; - vars.push_back( it->first ); - subs.push_back( NodeManager::currentNM()->mkConst( it->second ) ); - args.erase( ita ); - } + } + }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE ){ + Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl; + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] ); + if( ita!=args.end() ){ + vars.push_back( lit[0] ); + Expr testerExpr = lit.getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + const Datatype& dt = Datatype::datatypeOf(testerExpr); + const DatatypeConstructor& c = dt[index]; + std::vector< Node > newChildren; + newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); + std::vector< Node > newVars; + for( unsigned j=0; j<c.getNumArgs(); j++ ){ + TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); + tn = tn[1]; + Node v = NodeManager::currentNM()->mkBoundVar( tn ); + newChildren.push_back( v ); + newVars.push_back( v ); + } + subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) ); + Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; + args.erase( ita ); + args.insert( args.end(), newVars.begin(), newVars.end() ); + return true; + } + }else if( lit.getKind()==BOUND_VARIABLE ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit ); + if( ita!=args.end() ){ + Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl; + vars.push_back( lit ); + subs.push_back( NodeManager::currentNM()->mkConst( pol ) ); + args.erase( ita ); + return true; + } + } + return false; +} + +Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){ + Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; + QuantPhaseReq qpr( body ); + std::vector< Node > vars; + std::vector< Node > subs; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; + if( ( it->first.getKind()==EQUAL && it->second && options::varElimQuant() ) || + ( it->first.getKind()==APPLY_TESTER && it->second && it->first[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ) || + ( it->first.getKind()==BOUND_VARIABLE && options::varElimQuant() ) ){ + if( computeVariableElimLit( it->first, it->second, args, vars, subs, var_parent ) ){ + break; } } } @@ -838,6 +885,22 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } +Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ + //the parent id's for each variable, if using purifyQuant + std::map< Node, std::vector< int > > var_parent; + if( options::purifyQuant() ){ + body = computePurify( body, args, var_parent ); + } + if( options::varElimQuant() || options::dtVarExpandQuant() ){ + Node prev; + do{ + prev = body; + body = computeVarElimination2( body, args, ipl, var_parent ); + }while( prev!=body && !args.empty() ); + } + return body; +} + Node QuantifiersRewriter::computeClause( Node n ){ Assert( isClause( n ) ); if( isLiteral( n ) ){ @@ -1348,7 +1411,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return options::varElimQuant() || options::dtVarExpandQuant(); + return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant(); //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); }else{ @@ -1394,11 +1457,7 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - Node prev; - do{ - prev = n; - n = computeVarElimination( n, args, ipl ); - }while( prev!=n && !args.empty() ); + n = computeVarElimination( n, args, ipl ); //}else if( computeOption==COMPUTE_CNF ){ //n = computeCNF( n, args, defs, false ); //ipl = Node::null(); @@ -1620,3 +1679,83 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v } return n; } + + +Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, + std::map< Node, std::vector< int > >& var_parent, int parentId ){ + std::map< Node, Node >::iterator it = visited.find( body ); + if( it!=visited.end() ){ + return it->second; + }else{ + Node ret = body; + if( body.getNumChildren()>0 && body.getKind()!=FORALL ){ + std::vector< Node > children; + bool childrenChanged = false; + int id = getPurifyId( body ); + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id ); + childrenChanged = childrenChanged || bi!=body[i]; + children.push_back( bi ); + if( id!=0 && bi.getKind()==BOUND_VARIABLE ){ + if( std::find( var_parent[bi].begin(), var_parent[bi].end(), id )==var_parent[bi].end() ){ + var_parent[bi].push_back( id ); + } + } + } + if( childrenChanged ){ + if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), body.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); + } + if( parentId!=0 && parentId!=id ){ + //must purify if this has a bound variable + if( TermDb::containsTerms( ret, args ) ){ + Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() ); + var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) ); + ret = v; + args.push_back( v ); + } + } + } + visited[body] = ret; + return ret; + } +} + +Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { + std::map< Node, Node > visited; + std::map< Node, Node > var_to_term; + Node pbody = computePurify2( body, args, visited, var_to_term, var_parent, 0 ); + if( pbody==body ){ + return body; + }else{ + Trace("quantifiers-rewrite-purify") << "Purify : " << body << std::endl; + Trace("quantifiers-rewrite-purify") << " Got : " << pbody << std::endl; + for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){ + Trace("quantifiers-rewrite-purify") << " " << it->first << " : " << it->second << std::endl; + } + Trace("quantifiers-rewrite-purify") << "Variable parents : " << std::endl; + for( std::map< Node, std::vector< int > >::iterator it = var_parent.begin(); it != var_parent.end(); ++it ){ + Trace("quantifiers-rewrite-purify") << " " << it->first << " -> "; + for( unsigned i=0; i<it->second.size(); i++ ){ + Trace("quantifiers-rewrite-purify") << it->second[i] << " "; + } + Trace("quantifiers-rewrite-purify") << std::endl; + } + Trace("quantifiers-rewrite-purify") << std::endl; + std::vector< Node > disj; + for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){ + disj.push_back( it->second.negate() ); + } + Node res; + if( disj.empty() ){ + res = pbody; + }else{ + disj.push_back( pbody ); + res = NodeManager::currentNM()->mkNode( OR, disj ); + } + Trace("quantifiers-rewrite-purify") << "Constructed : " << res << std::endl << std::endl; + return res; + } +} |