From 8319e8d21f43b268168e4e66b1341630c7fb44e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Dec 2012 14:47:08 -0600 Subject: [PATCH] adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken) (cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276) --- src/theory/datatypes/theory_datatypes.cpp | 50 ++++++++++--------- src/theory/datatypes/theory_datatypes.h | 2 + .../quantifiers/quantifiers_attributes.cpp | 2 +- .../quantifiers/quantifiers_attributes.h | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.h | 2 +- 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 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 ); -- 2.30.2