More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.

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