support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)

5 files changed, 315 insertions, 52 deletions

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 );

 };

 

 }