+ if( isMacroLiteral( n, pol ) ){\r
+ std::vector< Node > candidates;\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ getMacroCandidates( n[i], candidates );\r
+ }\r
+ for( size_t i=0; i<candidates.size(); i++ ){\r
+ Node m = candidates[i];\r
+ Node op = m.getOperator();\r
+ if( !containsBadOp( n, m ) ){\r
+ std::vector< Node > fvs;\r
+ getFreeVariables( m, args, fvs, false );\r
+ //get definition and condition\r
+ Node n_def = solveInEquality( m, n ); //definition for the macro\r
+ //definition must exist and not contain any free variables apart from fvs\r
+ if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){\r
+ Node n_cond; //condition when this definition holds\r
+ //conditional must not contain any free variables apart from fvs\r
+ if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){\r
+ Trace("macros") << m << " is possible macro in " << f << std::endl;\r
+ //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where\r
+ // x1 ... xn are distinct variables\r
+ if( d_macro_basis[op].empty() ){\r
+ for( size_t a=0; a<m.getNumChildren(); a++ ){\r
+ std::stringstream ss;\r
+ ss << "mda_" << op << "_$$";\r
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );\r
+ d_macro_basis[op].push_back( v );\r
+ }\r
+ }\r
+ std::vector< Node > eq;\r
+ for( size_t a=0; a<m.getNumChildren(); a++ ){\r
+ eq.push_back( m[a] );\r
+ }\r
+ //solve system of equations "d_macro_basis[op] = m" for variables in fvs\r
+ std::map< Node, Node > solved;\r
+ //solve obvious cases first\r
+ for( size_t a=0; a<eq.size(); a++ ){\r
+ if( std::find( fvs.begin(), fvs.end(), eq[a] )!=fvs.end() ){\r
+ if( solved[ eq[a] ].isNull() ){\r
+ solved[ eq[a] ] = d_macro_basis[op][a];\r
+ }\r
+ }\r
+ }\r
+ //now, apply substitution for obvious cases\r
+ std::vector< Node > vars;\r
+ std::vector< Node > subs;\r
+ getSubstitution( fvs, solved, vars, subs, false );\r
+ for( size_t a=0; a<eq.size(); a++ ){\r
+ eq[a] = eq[a].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ }\r
+\r
+ Trace("macros-eq") << "Solve system of equations : " << std::endl;\r
+ for( size_t a=0; a<m.getNumChildren(); a++ ){\r
+ if( d_macro_basis[op][a]!=eq[a] ){\r
+ Trace("macros-eq") << " " << d_macro_basis[op][a] << " = " << eq[a] << std::endl;\r
+ }\r
+ }\r
+ Trace("macros-eq") << " for ";\r
+ for( size_t a=0; a<fvs.size(); a++ ){\r
+ if( solved[ fvs[a] ].isNull() ){\r
+ Trace("macros-eq") << fvs[a] << " ";\r
+ }\r
+ }\r
+ Trace("macros-eq") << std::endl;\r
+ //DO_THIS\r
+\r
+\r
+ vars.clear();\r
+ subs.clear();\r
+ if( getSubstitution( fvs, solved, vars, subs, true ) ){\r
+ //build condition\r
+ std::vector< Node > conds;\r
+ if( !n_cond.isNull() ){\r
+ //must apply substitution obtained from solving system of equations to original condition\r
+ n_cond = n_cond.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ conds.push_back( n_cond );\r
+ }\r
+ for( size_t a=0; a<eq.size(); a++ ){\r
+ //collect conditions based on solving argument's system of equations\r
+ if( d_macro_basis[op][a]!=eq[a] ){\r
+ conds.push_back( NodeManager::currentNM()->mkNode( eq[a].getType().isBoolean() ? IFF : EQUAL, d_macro_basis[op][a], eq[a] ) );\r
+ }\r
+ }\r
+ //build the condition\r
+ if( !conds.empty() ){\r
+ n_cond = conds.size()==1 ? conds[0] : NodeManager::currentNM()->mkNode( AND, conds );\r
+ }\r
+ //apply the substitution to the\r
+ n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ //now see if definition is consistent with others\r
+ if( isConsistentDefinition( op, n_cond, n_def ) ){\r
+ //must clear if it is a base definition\r
+ if( n_cond.isNull() ){\r
+ d_macro_def_cases[ op ].clear();\r
+ }\r
+ d_macro_def_cases[ op ].push_back( std::pair< Node, Node >( n_cond, n_def ) );\r
+ }\r
+ }\r
+ }\r