From a441252481616ff4851f208caffce826a026ae30 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Nov 2012 17:34:00 +0000
Subject: [PATCH] support for quantifiers macros, bug fix for bug 454 involving
 E-matching Array select terms (thanks for the bug report Francois)

---
 src/smt/smt_engine.cpp                        |   7 +-
 src/theory/quantifiers/inst_match.cpp         |  12 +
 src/theory/quantifiers/inst_match.h           |   9 +-
 .../quantifiers/inst_match_generator.cpp      |   2 +-
 src/theory/quantifiers/macros.cpp             | 323 +++++++++++++++---
 src/theory/quantifiers/macros.h               |  21 +-
 6 files changed, 320 insertions(+), 54 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e4d21c72e..b9025a2ce 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2109,8 +2109,11 @@ void SmtEnginePrivate::processAssertions() {
 
   if( options::macrosQuant() ){
     //quantifiers macro expansion
-    QuantifierMacros qm;
-    qm.simplify( d_assertionsToPreprocess );
+    bool success;
+    do{
+      QuantifierMacros qm;
+      success = qm.simplify( d_assertionsToPreprocess, true );
+    }while( success );
   }
 
   if( options::sortInference() ){
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 16f06017e..1a48ec161 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -134,6 +134,18 @@ Node InstMatch::getValue( Node var ) const{
   }
 }
 
+void InstMatch::set(TNode var, TNode n){
+  Assert( !var.isNull() );
+  if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
+  	//var.getType() == n.getType()
+  	!n.getType().isSubtypeOf( var.getType() ) ){
+    Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
+    Trace("inst-match-warn") << var << " " << var.getType() << n << " " << n.getType() << std::endl ;
+    Assert(false);
+  }
+  d_map[var] = n;
+}
+
 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 41ebb63d2..c8f843c90 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -92,14 +92,7 @@ public:
   /** get */
   Node get( TNode var ) { return d_map[var]; }
   /** set */
-  void set(TNode var, TNode n){
-    //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
-    Assert( !var.isNull() );
-    Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-            //var.getType() == n.getType()
-            n.getType().isSubtypeOf( var.getType() ) );
-    d_map[var] = n;
-  }
+  void set(TNode var, TNode n);
   size_t size(){ return d_map.size(); }
   /* iterator */
   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index a70fd9d7e..3b5e594fb 100755
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -629,7 +629,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
       Node ic = d_match_pattern[argIndex];
       for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
         Node t = it->first;
-        if( m.get( ic ).isNull() || m.get( ic )==t ){
+        if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){
           Node prev = m.get( ic );
           m.set( ic, t);
           addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 10db57184..c116b73f5 100755
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "theory/quantifiers/macros.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4;
 using namespace std;
@@ -25,7 +26,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 using namespace CVC4::context;
 
-void QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
+bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
   //first, collect macro definitions
   for( size_t i=0; i<assertions.size(); i++ ){
     if( assertions[i].getKind()==FORALL ){
@@ -37,28 +38,196 @@ void QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
       process( assertions[i][1], true, args, assertions[i] );
     }
   }
-  //now, rewrite based on macro definitions
-  for( size_t i=0; i<assertions.size(); i++ ){
-    assertions[i] = simplify( assertions[i] );
+  //create macro defs
+  for( std::map< Node, std::vector< std::pair< Node, Node > > >::iterator it = d_macro_def_cases.begin();
+       it != d_macro_def_cases.end(); ++it ){
+    //create ite based on case definitions
+    Node val;
+    for( size_t i=0; i<it->second.size(); ++i ){
+      if( it->second[i].first.isNull() ){
+        Assert( i==0 );
+        val = it->second[i].second;
+      }else{
+        //if value is null, must generate it
+        if( val.isNull() ){
+          std::stringstream ss;
+          ss << "mdo_" << it->first << "_$$";
+          Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" );
+          //will be defined in terms of fresh operator
+          std::vector< Node > children;
+          children.push_back( op );
+          children.insert( children.end(), d_macro_basis[ it->first ].begin(), d_macro_basis[ it->first ].end() );
+          val = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+        }
+        val = NodeManager::currentNM()->mkNode( ITE, it->second[i].first, it->second[i].second, val );
+      }
+    }
+    d_macro_defs[ it->first ] = val;
+    Trace("macros-def") << "* " << val << " is a macro for " << it->first << std::endl;
+  }
+  //now simplify bodies
+  for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+    d_macro_defs[ it->first ] = Rewriter::rewrite( simplify( it->second ) );
+  }
+  bool retVal = false;
+  if( doRewrite && !d_macro_defs.empty() ){
+    //now, rewrite based on macro definitions
+    for( size_t i=0; i<assertions.size(); i++ ){
+      Node prev = assertions[i];
+      assertions[i] = simplify( assertions[i] );
+      if( prev!=assertions[i] ){
+        assertions[i] = Rewriter::rewrite( assertions[i] );
+        Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl;
+        retVal = true;
+      }
+    }
+  }
+  return retVal;
+}
+
+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 ) ){
+        return true;
+      }
+    }
+    return false;
   }
 }
 
-bool QuantifierMacros::containsOp( Node n, Node op ){
+bool QuantifierMacros::containsBadOp( Node n, Node n_op ){
+  if( n!=n_op ){
+    if( n.getKind()==APPLY_UF ){
+      Node op = n.getOperator();
+      if( op==n_op.getOperator() ){
+        return true;
+      }
+      if( d_macro_def_cases.find( op )!=d_macro_def_cases.end() && !d_macro_def_cases[op].empty() ){
+        return true;
+      }
+    }
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( containsBadOp( n[i], n_op ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
+  return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );
+}
+
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
   if( n.getKind()==APPLY_UF ){
-    if( n.getOperator()==op ){
-      return true;
+    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 );
+    }
+  }
+}
+
+Node QuantifierMacros::solveInEquality( Node n, Node lit ){
+  if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+    //return the opposite side of the equality if defined that way
+    for( int i=0; i<2; i++ ){
+      if( lit[i]==n ){
+        return lit[ i==0 ? 1 : 0];
+      }
+    }
+    //must solve for term n in the literal lit
+    if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){
+      Node coeff;
+      Node term;
+      //could be solved for on LHS
+      if( lit[0].getKind()==MULT && lit[0][1]==n ){
+        Assert( lit[0][0].isConst() );
+        term = lit[1];
+        coeff = lit[0][0];
+      }else{
+        Assert( lit[1].getKind()==PLUS );
+        std::vector< Node > plus_children;
+        //find monomial with n
+        for( size_t j=0; j<lit[1].getNumChildren(); j++ ){
+          if( lit[1][j]==n ){
+            Assert( coeff.isNull() );
+            coeff = NodeManager::currentNM()->mkConst( Rational(1) );
+          }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){
+            Assert( coeff.isNull() );
+            Assert( lit[1][j][0].isConst() );
+            coeff = lit[1][j][0];
+          }else{
+            plus_children.push_back( lit[1][j] );
+          }
+        }
+        if( !coeff.isNull() ){
+          term = NodeManager::currentNM()->mkNode( PLUS, plus_children );
+          term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
+        }
+      }
+      if( !coeff.isNull() ){
+        coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );
+        term = NodeManager::currentNM()->mkNode( MULT, coeff, term );
+        term = Rewriter::rewrite( term );
+        return term;
+      }
+    }
+  }
+  Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
+  return Node::null();
+}
+
+bool QuantifierMacros::isConsistentDefinition( Node op, Node cond, Node def ){
+  if( d_macro_def_cases[op].empty() || ( cond.isNull() && !d_macro_def_cases[op][0].first.isNull() ) ){
+    return true;
+  }else{
+    return false;
+  }
+}
+
+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 );
+      }
     }
   }
   for( size_t i=0; i<n.getNumChildren(); i++ ){
-    if( containsOp( n[i], op ) ){
+    if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){
       return true;
     }
   }
   return false;
 }
 
-bool QuantifierMacros::isMacroKind( Node n, bool pol ){
-  return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
+bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
+                                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
+  bool success = true;
+  for( size_t a=0; a<v_quant.size(); a++ ){
+    if( !solved[ v_quant[a] ].isNull() ){
+      vars.push_back( v_quant[a] );
+      subs.push_back( solved[ v_quant[a] ] );
+    }else{
+      if( reqComplete ){
+        success = false;
+        break;
+      }
+    }
+  }
+  return success;
 }
 
 void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
@@ -71,20 +240,105 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
     //can not do anything
   }else{
     //literal case
-    //only care about literals in form of (basis, definition)
-    if( isMacroKind( n, pol ) ){
-      for( int i=0; i<2; i++ ){
-        int j = i==0 ? 1 : 0;
-        //check if n[i] is the basis for a macro
-        if( n[i].getKind()==APPLY_UF ){
-          //make sure it doesn't occur in the potential definition
-          if( !containsOp( n[j], n[i].getOperator() ) ){
-            //bool usable = true;
-            //for( size_j a=0; a<n[i].getNumChildren(); a++ )
-            //  if( std::find( args.begin(), args.end(), n[i][a] )==args.end() ){
-            //  }
-            //}
-            Trace("macros") << n << " is possible macro in " << f << std::endl;
+    if( isMacroLiteral( n, pol ) ){
+      std::vector< Node > candidates;
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        getMacroCandidates( n[i], candidates );
+      }
+      for( size_t i=0; i<candidates.size(); i++ ){
+        Node m = candidates[i];
+        Node op = m.getOperator();
+        if( !containsBadOp( n, m ) ){
+          std::vector< Node > fvs;
+          getFreeVariables( m, args, fvs, false );
+          //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
+          if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){
+            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") << 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 );
+                }
+              }
+              std::vector< Node > eq;
+              for( size_t a=0; a<m.getNumChildren(); a++ ){
+                eq.push_back( m[a] );
+              }
+              //solve system of equations "d_macro_basis[op] = m" for variables in fvs
+              std::map< Node, Node > solved;
+              //solve obvious cases first
+              for( size_t a=0; a<eq.size(); a++ ){
+                if( std::find( fvs.begin(), fvs.end(), eq[a] )!=fvs.end() ){
+                  if( solved[ eq[a] ].isNull() ){
+                    solved[ eq[a] ] = d_macro_basis[op][a];
+                  }
+                }
+              }
+              //now, apply substitution for obvious cases
+              std::vector< Node > vars;
+              std::vector< Node > subs;
+              getSubstitution( fvs, solved, vars, subs, false );
+              for( size_t a=0; a<eq.size(); a++ ){
+                eq[a] = eq[a].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+              }
+
+              Trace("macros-eq") << "Solve system of equations : " << std::endl;
+              for( size_t a=0; a<m.getNumChildren(); a++ ){
+                if( d_macro_basis[op][a]!=eq[a] ){
+                  Trace("macros-eq") << "   " << d_macro_basis[op][a] << " = " << eq[a] << std::endl;
+                }
+              }
+              Trace("macros-eq") << " for ";
+              for( size_t a=0; a<fvs.size(); a++ ){
+                if( solved[ fvs[a] ].isNull() ){
+                  Trace("macros-eq") << fvs[a] << " ";
+                }
+              }
+              Trace("macros-eq") << std::endl;
+              //DO_THIS
+
+
+              vars.clear();
+              subs.clear();
+              if( getSubstitution( fvs, solved, vars, subs, true ) ){
+                //build condition
+                std::vector< Node > conds;
+                if( !n_cond.isNull() ){
+                  //must apply substitution obtained from solving system of equations to original condition
+                  n_cond = n_cond.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+                  conds.push_back( n_cond );
+                }
+                for( size_t a=0; a<eq.size(); a++ ){
+                  //collect conditions based on solving argument's system of equations
+                  if( d_macro_basis[op][a]!=eq[a] ){
+                    conds.push_back( NodeManager::currentNM()->mkNode( eq[a].getType().isBoolean() ? IFF : EQUAL, d_macro_basis[op][a], eq[a] ) );
+                  }
+                }
+                //build the condition
+                if( !conds.empty() ){
+                  n_cond = conds.size()==1 ? conds[0] : NodeManager::currentNM()->mkNode( AND, conds );
+                }
+                //apply the substitution to the
+                n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+                //now see if definition is consistent with others
+                if( isConsistentDefinition( op, n_cond, n_def ) ){
+                  //must clear if it is a base definition
+                  if( n_cond.isNull() ){
+                    d_macro_def_cases[ op ].clear();
+                  }
+                  d_macro_def_cases[ op ].push_back( std::pair< Node, Node >( n_cond, n_def ) );
+                }
+              }
+            }
           }
         }
       }
@@ -93,7 +347,7 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
 }
 
 Node QuantifierMacros::simplify( Node n ){
-#if 0
+  Trace("macros-debug") << "simplify " << n << std::endl;
   std::vector< Node > children;
   bool childChanged = false;
   for( size_t i=0; i<n.getNumChildren(); i++ ){
@@ -103,26 +357,19 @@ Node QuantifierMacros::simplify( Node n ){
   }
   if( n.getKind()==APPLY_UF ){
     Node op = n.getOperator();
-    if( d_macro_defs.find( op )!=d_macro_defs.end() ){
+    if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
       //do subsitutition
-      Node ns = d_macro_defs[op].second;
-      std::vector< Node > vars;
-      for( size_t i = 0; i<d_macro_defs[op].first.getNumChildren(); i++ ){
-        vars.push_back( d_macro_defs[op].first[i] );
-      }
-      ns = ns.substitute( vars.begin(), vars.end(), children.begin(), children.end() );
-      return ns;
+      Node ret = d_macro_defs[op];
+      ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );
+      return ret;
     }
   }
   if( childChanged ){
-    if( n.isParameterized() ){
-      std::insert( children.begin(), n.getOperator() );
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), n.getOperator() );
     }
     return NodeManager::currentNM()->mkNode( n.getKind(), children );
   }else{
     return n;
   }
-#else
-  return n;
-#endif
 }
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index d93070481..b1fbb3e68 100755
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -31,17 +31,28 @@ namespace quantifiers {
 class QuantifierMacros{
 private:
   void process( Node n, bool pol, std::vector< Node >& args, Node f );
-  bool containsOp( Node n, Node op );
-  bool isMacroKind( Node n, bool pol );
-  //map from operators to macro definition ( basis, definition )
-  std::map< Node, std::pair< Node, Node > > d_macro_defs;
+  bool contains( Node n, Node n_s );
+  bool containsBadOp( Node n, Node n_op );
+  bool isMacroLiteral( Node n, bool pol );
+  void getMacroCandidates( Node n, std::vector< Node >& candidates );
+  Node solveInEquality( Node n, Node lit );
+  bool isConsistentDefinition( Node op, Node cond, Node def );
+  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );
+  bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
+                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
+  //map from operators to macro basis terms
+  std::map< Node, std::vector< Node > > d_macro_basis;
+  //map from operators to map from conditions to definition cases
+  std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases;
+  //map from operators to macro definition
+  std::map< Node, Node > d_macro_defs;
 private:
   Node simplify( Node n );
 public:
   QuantifierMacros(){}
   ~QuantifierMacros(){}
 
-  void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+  bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
 };
 
 }
-- 
2.30.2