adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

6 files changed, 33 insertions, 27 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e23d9deae..9da83ce41 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -45,7 +45,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
   d_selector_apps( c ),
   d_labels( c ),
-  d_conflict( c, false ){
+  d_conflict( c, false ),
+  d_collectTermsCache( c ){
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -758,31 +759,34 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
 
 
 void TheoryDatatypes::collectTerms( Node n ) {
-  for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-    collectTerms( n[i] );
-  }
-  if( n.getKind() == APPLY_CONSTRUCTOR ){
-    //we must take into account subterm relation when checking for cycles
+  if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
+    d_collectTermsCache[n] = true;
     for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-      Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
-      bool result = d_cycle_check.addEdgeNode( n, n[i] );
-      d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
+      collectTerms( n[i] );
     }
-  }else if( n.getKind() == APPLY_SELECTOR ){
-    if( d_selector_apps.find( n )==d_selector_apps.end() ){
-      d_selector_apps[n] = false;
-      //we must also record which selectors exist
-      Debug("datatypes") << "  Found selector " << n << endl;
-      if (n.getType().isBoolean()) {
-        d_equalityEngine.addTriggerPredicate( n );
-      }else{
-        d_equalityEngine.addTerm( n );
+    if( n.getKind() == APPLY_CONSTRUCTOR ){
+      //we must take into account subterm relation when checking for cycles
+      for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+        Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
+        bool result = d_cycle_check.addEdgeNode( n, n[i] );
+        d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
       }
-      Node rep = getRepresentative( n[0] );
-      EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-      if( !eqc->d_selectors ){
-        eqc->d_selectors = true;
-        instantiate( eqc, rep );
+    }else if( n.getKind() == APPLY_SELECTOR ){
+      if( d_selector_apps.find( n )==d_selector_apps.end() ){
+        d_selector_apps[n] = false;
+        //we must also record which selectors exist
+        Debug("datatypes") << "  Found selector " << n << endl;
+        if (n.getType().isBoolean()) {
+          d_equalityEngine.addTriggerPredicate( n );
+        }else{
+          d_equalityEngine.addTerm( n );
+        }
+        Node rep = getRepresentative( n[0] );
+        EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
+        if( !eqc->d_selectors ){
+          eqc->d_selectors = true;
+          instantiate( eqc, rep );
+        }
       }
     }
   }
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 90d82e255..9846e80f2 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -156,6 +156,8 @@ private:
   context::CDO<bool> d_conflict;
   /** The conflict node */
   Node d_conflictNode;
+  /** cache for which terms we have called collectTerms(...) on */
+  BoolMap d_collectTermsCache;
   /** pending assertions/merges */
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 493a49e54..2f6dc47db 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -22,7 +22,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;

 using namespace CVC4::theory::quantifiers;

 

-void QuantifiersAttributes::setUserAttribute( std::string& attr, Node n ){

+void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){

   if( n.getKind()==FORALL ){

     if( attr=="axiom" ){

       Trace("quant-attr") << "Set axiom " << n << std::endl;

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 822d6c59f..88bac8bc9 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -40,7 +40,7 @@ struct QuantifiersAttributes
     *   This function will apply a custom set of attributes to all top-level universal

     *   quantifiers contained in n

     */

-  static void setUserAttribute( std::string& attr, Node n );

+  static void setUserAttribute( const std::string& attr, Node n );

 };

 

 

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index cfdb30f38..b1a7c9927 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -192,6 +192,6 @@ bool TheoryQuantifiers::restart(){
   }
 }
 
-void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){
+void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){
   QuantifiersAttributes::setUserAttribute( attr, n );
 }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index c3987144c..b4c8966c7 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -70,7 +70,7 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();
-  void setUserAttribute( std::string& attr, Node n );
+  void setUserAttribute( const std::string& attr, Node n );
   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
 private:
   void assertUniversal( Node n );