diff options
Diffstat (limited to 'src/theory/quantifiers/macros.cpp')
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 233 |
1 files changed, 124 insertions, 109 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index c26aea465..163005806 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -22,6 +22,8 @@ #include "smt/smt_engine_scope.h" #include "theory/quantifiers/modes.h" #include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" using namespace CVC4; using namespace std; @@ -31,26 +33,14 @@ using namespace CVC4::kind; bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ - unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_GROUND ? 1 : 2; + unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r<rmax; r++ ){ d_ground_macros = (r==0); Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl; //first, collect macro definitions - std::map< unsigned, Node > simp_assertions; - int last_macro = -1; for( int i=0; i<(int)assertions.size(); i++ ){ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; - Node curr = assertions[i]; - //do simplification before process - if( doRewrite && !d_macro_defs_new.empty() ){ - curr = simplify( assertions[i] ); - curr = Rewriter::rewrite( curr ); - if( curr!=assertions[i] ){ - simp_assertions[i] = curr; - } - } - if( processAssertion( curr ) ){ - last_macro = i; + if( processAssertion( assertions[i] ) ){ //process this assertion again i--; } @@ -61,15 +51,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite Trace("macros") << "Do simplifications..." << std::endl; //now, rewrite based on macro definitions for( unsigned i=0; i<assertions.size(); i++ ){ - Node curr = assertions[i]; - std::map< unsigned, Node >::iterator it = simp_assertions.find( i ); - if( it!=simp_assertions.end() ){ - curr = it->second; - } - //simplify again if before last macro - if( (int)i<last_macro ){ - curr = simplify( curr ); - } + Node curr = simplify( assertions[i] ); if( curr!=assertions[i] ){ curr = Rewriter::rewrite( curr ); Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl; @@ -84,8 +66,8 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite } } } - for( int i=0; i<(int)assertions.size(); i++ ){ - if( Trace.isOn("macros-warn") ){ + if( Trace.isOn("macros-warn") ){ + for( int i=0; i<(int)assertions.size(); i++ ){ debugMacroDefinition( assertions[i], assertions[i] ); } } @@ -99,47 +81,45 @@ bool QuantifierMacros::processAssertion( Node n ) { return true; } } - return false; - }else if( n.getKind()==FORALL ){ + }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){ std::vector< Node > args; for( size_t j=0; j<n[0].getNumChildren(); j++ ){ args.push_back( n[0][j] ); } + Node nproc = n[1]; + if( !d_macro_defs_new.empty() ){ + nproc = simplify( nproc ); + if( nproc!=n[1] ){ + nproc = Rewriter::rewrite( nproc ); + } + } //look at the body of the quantifier for macro definition - return process( n[1], true, args, n ); - }else{ - return false; + if( process( nproc, true, args, n ) ){ + d_quant_macros[n] = true; + return true; + } } + return false; } -bool QuantifierMacros::contains( Node n, Node n_s ){ - if( n==n_s ){ - return true; - }else{ - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( contains( n[i], n_s ) ){ +bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + Node nop = n.getOperator(); + if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ return true; } - } - return false; - } -} - -bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc ){ - if( n.getKind()==APPLY_UF ){ - Node nop = n.getOperator(); - if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ + if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ + opc.push_back( nop ); + } + }else if( d_ground_macros && n.getKind()==FORALL ){ return true; } - if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ - opc.push_back( nop ); - } - }else if( d_ground_macros && n.getKind()==FORALL ){ - return true; - } - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( containsBadOp( n[i], op, opc ) ){ - return true; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( containsBadOp( n[i], op, opc, visited ) ){ + return true; + } } } return false; @@ -149,6 +129,19 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ return pol && ( n.getKind()==EQUAL || n.getKind()==IFF ); } +bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { + Node icn = d_qe->getTermDatabase()->getInstConstantNode( n, f ); + Trace("macros-debug2") << "Get free variables in " << icn << std::endl; + std::vector< Node > var; + d_qe->getTermDatabase()->getVarContainsNode( f, icn, var ); + Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; + std::vector< Node > trigger_var; + inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var ); + Trace("macros-debug2") << "Done." << std::endl; + //only if all variables are also trigger variables + return trigger_var.size()>=var.size(); +} + bool QuantifierMacros::isBoundVarApplyUf( Node n ) { Assert( n.getKind()==APPLY_UF ); TypeNode tn = n.getOperator().getType(); @@ -168,22 +161,25 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) { return true; } -void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){ - if( n.getKind()==APPLY_UF ){ - if( isBoundVarApplyUf( n ) ){ - candidates.push_back( n ); - } - }else if( n.getKind()==PLUS ){ - for( size_t i=0; i<n.getNumChildren(); i++ ){ - getMacroCandidates( n[i], candidates ); - } - }else if( n.getKind()==MULT ){ - //if the LHS is a constant - if( n.getNumChildren()==2 && n[0].isConst() ){ - getMacroCandidates( n[1], candidates ); +void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + if( isBoundVarApplyUf( n ) ){ + candidates.push_back( n ); + } + }else if( n.getKind()==PLUS ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + getMacroCandidates( n[i], candidates, visited ); + } + }else if( n.getKind()==MULT ){ + //if the LHS is a constant + if( n.getNumChildren()==2 && n[0].isConst() ){ + getMacroCandidates( n[1], candidates, visited ); + } + }else if( n.getKind()==NOT ){ + getMacroCandidates( n[0], candidates, visited ); } - }else if( n.getKind()==NOT ){ - getMacroCandidates( n[0], candidates ); } } @@ -239,19 +235,22 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){ return Node::null(); } -bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){ - if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ - if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ - if( retOnly ){ - return true; - }else{ - vars.push_back( n ); +bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ + if( retOnly ){ + return true; + }else{ + vars.push_back( n ); + } } } - } - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){ - return true; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){ + return true; + } } } return false; @@ -305,46 +304,58 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod }else{ //literal case if( isMacroLiteral( n, pol ) ){ + std::map< Node, bool > visited; std::vector< Node > candidates; for( size_t i=0; i<n.getNumChildren(); i++ ){ - getMacroCandidates( n[i], candidates ); + getMacroCandidates( n[i], candidates, visited ); } for( size_t i=0; i<candidates.size(); i++ ){ Node m = candidates[i]; Node op = m.getOperator(); if( d_macro_defs.find( op )==d_macro_defs.end() ){ std::vector< Node > fvs; - getFreeVariables( m, args, fvs, false ); + visited.clear(); + getFreeVariables( m, args, fvs, false, visited ); //get definition and condition Node n_def = solveInEquality( m, n ); //definition for the macro - //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains - std::vector< Node > opc; - if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op, opc ) ){ - Node n_cond; //condition when this definition holds - //conditional must not contain any free variables apart from fvs - if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){ - Trace("macros-debug") << m << " is possible macro in " << f << std::endl; - //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where - // x1 ... xn are distinct variables - if( d_macro_basis[op].empty() ){ - for( size_t a=0; a<m.getNumChildren(); a++ ){ - std::stringstream ss; - ss << "mda_" << op << ""; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); - d_macro_basis[op].push_back( v ); + if( !n_def.isNull() ){ + Trace("macros-debug") << m << " is possible macro in " << f << std::endl; + Trace("macros-debug") << " corresponding definition is : " << n_def << std::endl; + visited.clear(); + //definition must exist and not contain any free variables apart from fvs + if( !getFreeVariables( n_def, args, fvs, true, visited ) ){ + Trace("macros-debug") << "...free variables are contained." << std::endl; + visited.clear(); + //cannot contain a defined operator, opc is list of functions it contains + std::vector< Node > opc; + if( !containsBadOp( n_def, op, opc, visited ) ){ + Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl; + //must be ground UF term if mode is GROUND_UF + if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){ + Trace("macros-debug") << "...respects ground-uf constraint." << std::endl; + //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where + // x1 ... xn are distinct variables + if( d_macro_basis[op].empty() ){ + for( size_t a=0; a<m.getNumChildren(); a++ ){ + std::stringstream ss; + ss << "mda_" << op << ""; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); + d_macro_basis[op].push_back( v ); + } + } + std::map< Node, Node > solved; + for( size_t a=0; a<m.getNumChildren(); a++ ){ + solved[m[a]] = d_macro_basis[op][a]; + } + std::vector< Node > vars; + std::vector< Node > subs; + if( getSubstitution( fvs, solved, vars, subs, true ) ){ + n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + addMacro( op, n_def, opc ); + return true; + } } } - std::map< Node, Node > solved; - for( size_t a=0; a<m.getNumChildren(); a++ ){ - solved[m[a]] = d_macro_basis[op][a]; - } - std::vector< Node > vars; - std::vector< Node > subs; - if( getSubstitution( fvs, solved, vars, subs, true ) ){ - n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - addMacro( op, n_def, opc ); - return true; - } } } } @@ -416,7 +427,11 @@ void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) { } void QuantifierMacros::finalizeDefinitions() { - if( options::incrementalSolving() || options::produceModels() || Trace.isOn("macros-warn") ){ + bool doDefs = false; + if( Trace.isOn("macros-warn") ){ + doDefs = true; + } + if( options::incrementalSolving() || options::produceModels() || doDefs ){ Trace("macros") << "Store as defined functions..." << std::endl; //also store as defined functions for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){ |