replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros

8 files changed, 267 insertions, 80 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index ed60e77a9..371aa5543 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -42,7 +42,9 @@ libquantifiers_la_SOURCES = \
 	quant_util.h \
 	quant_util.cpp \
 	inst_match_generator.h \
-	inst_match_generator.cpp
+	inst_match_generator.cpp \
+	macros.h \
+	macros.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
new file mode 100755
index 000000000..10db57184
--- /dev/null
+++ b/src/theory/quantifiers/macros.cpp
@@ -0,0 +1,128 @@
+/*********************                                                        */

+/*! \file macros.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Sort inference module

+ **

+ ** This class implements quantifiers macro definitions.

+ **/

+

+#include <vector>

+

+#include "theory/quantifiers/macros.h"

+

+using namespace CVC4;

+using namespace std;

+using namespace CVC4::theory;

+using namespace CVC4::theory::quantifiers;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+

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

+      std::vector< Node > args;

+      for( size_t j=0; j<assertions[i][0].getNumChildren(); j++ ){

+        args.push_back( assertions[i][0][j] );

+      }

+      //look at the body of the quantifier for macro definition

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

+  }

+}

+

+bool QuantifierMacros::containsOp( Node n, Node op ){

+  if( n.getKind()==APPLY_UF ){

+    if( n.getOperator()==op ){

+      return true;

+    }

+  }

+  for( size_t i=0; i<n.getNumChildren(); i++ ){

+    if( containsOp( n[i], op ) ){

+      return true;

+    }

+  }

+  return false;

+}

+

+bool QuantifierMacros::isMacroKind( Node n, bool pol ){

+  return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );

+}

+

+void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){

+  if( n.getKind()==NOT ){

+    process( n[0], !pol, args, f );

+  }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){

+    //bool favorPol = (n.getKind()==AND)==pol;

+    //conditional?

+  }else if( n.getKind()==ITE ){

+    //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;

+          }

+        }

+      }

+    }

+  }

+}

+

+Node QuantifierMacros::simplify( Node n ){

+#if 0

+  std::vector< Node > children;

+  bool childChanged = false;

+  for( size_t i=0; i<n.getNumChildren(); i++ ){

+    Node nn = simplify( n[i] );

+    children.push_back( nn );

+    childChanged = childChanged || nn!=n[i];

+  }

+  if( n.getKind()==APPLY_UF ){

+    Node op = n.getOperator();

+    if( d_macro_defs.find( op )!=d_macro_defs.end() ){

+      //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;

+    }

+  }

+  if( childChanged ){

+    if( n.isParameterized() ){

+      std::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
new file mode 100755
index 000000000..d93070481
--- /dev/null
+++ b/src/theory/quantifiers/macros.h
@@ -0,0 +1,51 @@
+/*********************                                                        */

+/*! \file macros.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Pre-process step for detecting quantifier macro definitions

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__QUANTIFIERS_MACROS_H

+#define __CVC4__QUANTIFIERS_MACROS_H

+

+#include <iostream>

+#include <string>

+#include <vector>

+#include <map>

+#include "expr/node.h"

+#include "expr/type_node.h"

+

+namespace CVC4 {

+namespace theory {

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

+private:

+  Node simplify( Node n );

+public:

+  QuantifierMacros(){}

+  ~QuantifierMacros(){}

+

+  void simplify( std::vector< Node >& assertions, bool doRewrite = false );

+};

+

+}

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2c36520e4..24d0c4047 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -37,6 +37,10 @@ option cnfQuant --cnf-quant bool :default false
 option preSkolemQuant --pre-skolem-quant bool :default false
  apply skolemization eagerly to bodies of quantified formulas
 
+# Whether to perform quantifier macro expansion
+option macrosQuant --macros-quant bool :default false
+ perform quantifiers macro expansions
+
 # Whether to use smart triggers
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b55e8abdf..2c2ee0bfe 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -468,6 +468,77 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain
   }
 }
 
+/** is n1 an instance of n2 or vice versa? */
+int TermDb::isInstanceOf( Node n1, Node n2 ){
+  if( n1==n2 ){
+    return 1;
+  }else if( n1.getKind()==n2.getKind() ){
+    if( n1.getKind()==APPLY_UF ){
+      if( n1.getOperator()==n2.getOperator() ){
+        int result = 0;
+        for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+          if( n1[i]!=n2[i] ){
+            int cResult = isInstanceOf( n1[i], n2[i] );
+            if( cResult==0 ){
+              return 0;
+            }else if( cResult!=result ){
+              if( result!=0 ){
+                return 0;
+              }else{
+                result = cResult;
+              }
+            }
+          }
+        }
+        return result;
+      }
+    }
+    return 0;
+  }else if( n2.getKind()==INST_CONSTANT ){
+    computeVarContains( n1 );
+    //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
+    //  return 1;
+    //}
+    if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){
+      return 1;
+    }
+  }else if( n1.getKind()==INST_CONSTANT ){
+    computeVarContains( n2 );
+    //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
+    //  return -1;
+    //}
+    if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){
+      return 1;
+    }
+  }
+  return 0;
+}
+
+void TermDb::filterInstances( std::vector< Node >& nodes ){
+  std::vector< bool > active;
+  active.resize( nodes.size(), true );
+  for( int i=0; i<(int)nodes.size(); i++ ){
+    for( int j=i+1; j<(int)nodes.size(); j++ ){
+      if( active[i] && active[j] ){
+        int result = isInstanceOf( nodes[i], nodes[j] );
+        if( result==1 ){
+          active[j] = false;
+        }else if( result==-1 ){
+          active[i] = false;
+        }
+      }
+    }
+  }
+  std::vector< Node > temp;
+  for( int i=0; i<(int)nodes.size(); i++ ){
+    if( active[i] ){
+      temp.push_back( nodes[i] );
+    }
+  }
+  nodes.clear();
+  nodes.insert( nodes.begin(), temp.begin(), temp.end() );
+}
+
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
     d_op_triggers[op].push_back( tr );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2bae5a043..a1f1de1dc 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -65,6 +65,10 @@ class QuantifiersEngine;
 namespace inst{
   class Trigger;
 }
+namespace rrinst{
+  class Trigger;
+}
+
 
 namespace quantifiers {
 
@@ -82,6 +86,7 @@ public:
 class TermDb {
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class ::CVC4::theory::inst::Trigger;
+  friend class ::CVC4::theory::rrinst::Trigger;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -218,6 +223,10 @@ public:
   void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
   /** register trigger (for eager quantifier instantiation) */
   void registerTrigger( inst::Trigger* tr, Node op );
+  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+  int isInstanceOf( Node n1, Node n2 );
+  /** filter all nodes that have instances */
+  void filterInstances( std::vector< Node >& nodes );
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 67b2e6bd8..a9c5e8b96 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -250,32 +250,6 @@ bool Trigger::isSimpleTrigger( Node n ){
   }
 }
 
-/** filter all nodes that have instances */
-void Trigger::filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes ){
-  std::vector< bool > active;
-  active.resize( nodes.size(), true );
-  for( int i=0; i<(int)nodes.size(); i++ ){
-    for( int j=i+1; j<(int)nodes.size(); j++ ){
-      if( active[i] && active[j] ){
-        int result = isInstanceOf( qe, nodes[i], nodes[j] );
-        if( result==1 ){
-          active[j] = false;
-        }else if( result==-1 ){
-          active[i] = false;
-        }
-      }
-    }
-  }
-  std::vector< Node > temp;
-  for( int i=0; i<(int)nodes.size(); i++ ){
-    if( active[i] ){
-      temp.push_back( nodes[i] );
-    }
-  }
-  nodes.clear();
-  nodes.insert( nodes.begin(), temp.begin(), temp.end() );
-}
-
 
 bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
   if( patMap.find( n )==patMap.end() ){
@@ -345,7 +319,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
     collectPatTerms( qe, f, n, patTerms2, TS_ALL, false );
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
-    filterInstances( qe, temp );
+    qe->getTermDatabase()->filterInstances( temp );
     if( temp.size()!=patTerms2.size() ){
       Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
       Debug("trigger-filter-instance") << "Old: ";
@@ -378,54 +352,6 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
   }
 }
 
-/** is n1 an instance of n2 or vice versa? */
-int Trigger::isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ){
-  if( n1==n2 ){
-    return 1;
-  }else if( n1.getKind()==n2.getKind() ){
-    if( n1.getKind()==APPLY_UF ){
-      if( n1.getOperator()==n2.getOperator() ){
-        int result = 0;
-        for( int i=0; i<(int)n1.getNumChildren(); i++ ){
-          if( n1[i]!=n2[i] ){
-            int cResult = isInstanceOf( qe, n1[i], n2[i] );
-            if( cResult==0 ){
-              return 0;
-            }else if( cResult!=result ){
-              if( result!=0 ){
-                return 0;
-              }else{
-                result = cResult;
-              }
-            }
-          }
-        }
-        return result;
-      }
-    }
-    return 0;
-  }else if( n2.getKind()==INST_CONSTANT ){
-    qe->getTermDatabase()->computeVarContains( n1 );
-    //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
-    //  return 1;
-    //}
-    if( qe->getTermDatabase()->d_var_contains[ n1 ].size()==1 &&
-        qe->getTermDatabase()->d_var_contains[ n1 ][ 0 ]==n2 ){
-      return 1;
-    }
-  }else if( n1.getKind()==INST_CONSTANT ){
-    qe->getTermDatabase()->computeVarContains( n2 );
-    //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
-    //  return -1;
-    //}
-    if( qe->getTermDatabase()->d_var_contains[ n2 ].size()==1 &&
-        qe->getTermDatabase()->d_var_contains[ n2 ][ 0 ]==n1 ){
-      return 1;
-    }
-  }
-  return 0;
-}
-
 bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
   if( n.getKind()==PLUS ){
     Assert( coeffs.empty() );
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 267debb02..6fcd316f4 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -108,10 +108,6 @@ public:
   static bool isUsableTrigger( Node n, Node f );
   static bool isAtomicTrigger( Node n );
   static bool isSimpleTrigger( Node n );
-  /** filter all nodes that have instances */
-  static void filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes );
-  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  static int isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 );
   /** get pattern arithmetic */
   static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );