#include <vector>\r
\r
#include "theory/quantifiers/macros.h"\r
+#include "theory/rewriter.h"\r
\r
using namespace CVC4;\r
using namespace std;\r
using namespace CVC4::kind;\r
using namespace CVC4::context;\r
\r
-void QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){\r
+bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){\r
//first, collect macro definitions\r
for( size_t i=0; i<assertions.size(); i++ ){\r
if( assertions[i].getKind()==FORALL ){\r
process( assertions[i][1], true, args, assertions[i] );\r
}\r
}\r
- //now, rewrite based on macro definitions\r
- for( size_t i=0; i<assertions.size(); i++ ){\r
- assertions[i] = simplify( assertions[i] );\r
+ //create macro defs\r
+ for( std::map< Node, std::vector< std::pair< Node, Node > > >::iterator it = d_macro_def_cases.begin();\r
+ it != d_macro_def_cases.end(); ++it ){\r
+ //create ite based on case definitions\r
+ Node val;\r
+ for( size_t i=0; i<it->second.size(); ++i ){\r
+ if( it->second[i].first.isNull() ){\r
+ Assert( i==0 );\r
+ val = it->second[i].second;\r
+ }else{\r
+ //if value is null, must generate it\r
+ if( val.isNull() ){\r
+ std::stringstream ss;\r
+ ss << "mdo_" << it->first << "_$$";\r
+ Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" );\r
+ //will be defined in terms of fresh operator\r
+ std::vector< Node > children;\r
+ children.push_back( op );\r
+ children.insert( children.end(), d_macro_basis[ it->first ].begin(), d_macro_basis[ it->first ].end() );\r
+ val = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+ }\r
+ val = NodeManager::currentNM()->mkNode( ITE, it->second[i].first, it->second[i].second, val );\r
+ }\r
+ }\r
+ d_macro_defs[ it->first ] = val;\r
+ Trace("macros-def") << "* " << val << " is a macro for " << it->first << std::endl;\r
+ }\r
+ //now simplify bodies\r
+ for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){\r
+ d_macro_defs[ it->first ] = Rewriter::rewrite( simplify( it->second ) );\r
+ }\r
+ bool retVal = false;\r
+ if( doRewrite && !d_macro_defs.empty() ){\r
+ //now, rewrite based on macro definitions\r
+ for( size_t i=0; i<assertions.size(); i++ ){\r
+ Node prev = assertions[i];\r
+ assertions[i] = simplify( assertions[i] );\r
+ if( prev!=assertions[i] ){\r
+ assertions[i] = Rewriter::rewrite( assertions[i] );\r
+ Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl;\r
+ retVal = true;\r
+ }\r
+ }\r
+ }\r
+ return retVal;\r
+}\r
+\r
+bool QuantifierMacros::contains( Node n, Node n_s ){\r
+ if( n==n_s ){\r
+ return true;\r
+ }else{\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ if( contains( n[i], n_s ) ){\r
+ return true;\r
+ }\r
+ }\r
+ return false;\r
}\r
}\r
\r
-bool QuantifierMacros::containsOp( Node n, Node op ){\r
+bool QuantifierMacros::containsBadOp( Node n, Node n_op ){\r
+ if( n!=n_op ){\r
+ if( n.getKind()==APPLY_UF ){\r
+ Node op = n.getOperator();\r
+ if( op==n_op.getOperator() ){\r
+ return true;\r
+ }\r
+ if( d_macro_def_cases.find( op )!=d_macro_def_cases.end() && !d_macro_def_cases[op].empty() ){\r
+ return true;\r
+ }\r
+ }\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ if( containsBadOp( n[i], n_op ) ){\r
+ return true;\r
+ }\r
+ }\r
+ }\r
+ return false;\r
+}\r
+\r
+bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){\r
+ return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );\r
+}\r
+\r
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){\r
if( n.getKind()==APPLY_UF ){\r
- if( n.getOperator()==op ){\r
- return true;\r
+ candidates.push_back( n );\r
+ }else if( n.getKind()==PLUS ){\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ getMacroCandidates( n[i], candidates );\r
+ }\r
+ }else if( n.getKind()==MULT ){\r
+ //if the LHS is a constant\r
+ if( n.getNumChildren()==2 && n[0].isConst() ){\r
+ getMacroCandidates( n[1], candidates );\r
+ }\r
+ }\r
+}\r
+\r
+Node QuantifierMacros::solveInEquality( Node n, Node lit ){\r
+ if( lit.getKind()==IFF || lit.getKind()==EQUAL ){\r
+ //return the opposite side of the equality if defined that way\r
+ for( int i=0; i<2; i++ ){\r
+ if( lit[i]==n ){\r
+ return lit[ i==0 ? 1 : 0];\r
+ }\r
+ }\r
+ //must solve for term n in the literal lit\r
+ if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){\r
+ Node coeff;\r
+ Node term;\r
+ //could be solved for on LHS\r
+ if( lit[0].getKind()==MULT && lit[0][1]==n ){\r
+ Assert( lit[0][0].isConst() );\r
+ term = lit[1];\r
+ coeff = lit[0][0];\r
+ }else{\r
+ Assert( lit[1].getKind()==PLUS );\r
+ std::vector< Node > plus_children;\r
+ //find monomial with n\r
+ for( size_t j=0; j<lit[1].getNumChildren(); j++ ){\r
+ if( lit[1][j]==n ){\r
+ Assert( coeff.isNull() );\r
+ coeff = NodeManager::currentNM()->mkConst( Rational(1) );\r
+ }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){\r
+ Assert( coeff.isNull() );\r
+ Assert( lit[1][j][0].isConst() );\r
+ coeff = lit[1][j][0];\r
+ }else{\r
+ plus_children.push_back( lit[1][j] );\r
+ }\r
+ }\r
+ if( !coeff.isNull() ){\r
+ term = NodeManager::currentNM()->mkNode( PLUS, plus_children );\r
+ term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );\r
+ }\r
+ }\r
+ if( !coeff.isNull() ){\r
+ coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );\r
+ term = NodeManager::currentNM()->mkNode( MULT, coeff, term );\r
+ term = Rewriter::rewrite( term );\r
+ return term;\r
+ }\r
+ }\r
+ }\r
+ Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;\r
+ return Node::null();\r
+}\r
+\r
+bool QuantifierMacros::isConsistentDefinition( Node op, Node cond, Node def ){\r
+ if( d_macro_def_cases[op].empty() || ( cond.isNull() && !d_macro_def_cases[op][0].first.isNull() ) ){\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){\r
+ if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){\r
+ if( std::find( vars.begin(), vars.end(), n )==vars.end() ){\r
+ if( retOnly ){\r
+ return true;\r
+ }else{\r
+ vars.push_back( n );\r
+ }\r
}\r
}\r
for( size_t i=0; i<n.getNumChildren(); i++ ){\r
- if( containsOp( n[i], op ) ){\r
+ if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){\r
return true;\r
}\r
}\r
return false;\r
}\r
\r
-bool QuantifierMacros::isMacroKind( Node n, bool pol ){\r
- return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );\r
+bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,\r
+ std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){\r
+ bool success = true;\r
+ for( size_t a=0; a<v_quant.size(); a++ ){\r
+ if( !solved[ v_quant[a] ].isNull() ){\r
+ vars.push_back( v_quant[a] );\r
+ subs.push_back( solved[ v_quant[a] ] );\r
+ }else{\r
+ if( reqComplete ){\r
+ success = false;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ return success;\r
}\r
\r
void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){\r
//can not do anything\r
}else{\r
//literal case\r
- //only care about literals in form of (basis, definition)\r
- if( isMacroKind( n, pol ) ){\r
- for( int i=0; i<2; i++ ){\r
- int j = i==0 ? 1 : 0;\r
- //check if n[i] is the basis for a macro\r
- if( n[i].getKind()==APPLY_UF ){\r
- //make sure it doesn't occur in the potential definition\r
- if( !containsOp( n[j], n[i].getOperator() ) ){\r
- //bool usable = true;\r
- //for( size_j a=0; a<n[i].getNumChildren(); a++ )\r
- // if( std::find( args.begin(), args.end(), n[i][a] )==args.end() ){\r
- // }\r
- //}\r
- Trace("macros") << n << " is possible macro in " << f << std::endl;\r
+ 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
}\r
}\r
}\r
}\r
\r
Node QuantifierMacros::simplify( Node n ){\r
-#if 0\r
+ Trace("macros-debug") << "simplify " << n << std::endl;\r
std::vector< Node > children;\r
bool childChanged = false;\r
for( size_t i=0; i<n.getNumChildren(); i++ ){\r
}\r
if( n.getKind()==APPLY_UF ){\r
Node op = n.getOperator();\r
- if( d_macro_defs.find( op )!=d_macro_defs.end() ){\r
+ if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){\r
//do subsitutition\r
- Node ns = d_macro_defs[op].second;\r
- std::vector< Node > vars;\r
- for( size_t i = 0; i<d_macro_defs[op].first.getNumChildren(); i++ ){\r
- vars.push_back( d_macro_defs[op].first[i] );\r
- }\r
- ns = ns.substitute( vars.begin(), vars.end(), children.begin(), children.end() );\r
- return ns;\r
+ Node ret = d_macro_defs[op];\r
+ ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );\r
+ return ret;\r
}\r
}\r
if( childChanged ){\r
- if( n.isParameterized() ){\r
- std::insert( children.begin(), n.getOperator() );\r
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
+ children.insert( children.begin(), n.getOperator() );\r
}\r
return NodeManager::currentNM()->mkNode( n.getKind(), children );\r
}else{\r
return n;\r
}\r
-#else\r
- return n;\r
-#endif\r
}\r
projects / cvc5.git / commitdiff