diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 17:10:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 17:10:03 -0500 |
commit | 453ae55ac7adcda70b4dfbc95c78e899961c8e2d (patch) | |
tree | d74bc7ca24a3b33410458c5b138d87c4f610ab39 /src | |
parent | d5d05e4723581c86808a866af1a9f20343ed36dc (diff) |
Minor fix to strings, cleanup in datatypes.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 53 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 6 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 17 |
3 files changed, 37 insertions, 39 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 89ba3c6a7..0100f1833 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -56,8 +56,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, //d_consEqc( c ), d_conflict( c, false ), d_collectTermsCache( c ), - d_consTerms( c ), - d_selTerms( c ), + d_functionTerms( c ), d_singleton_eq( u ), d_lemmas_produced_c( u ) { @@ -1352,36 +1351,32 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers:: void TheoryDatatypes::computeCareGraph(){ unsigned n_pairs = 0; - Trace("dt-cg-summary") << "Compute graph for dt..." << d_consTerms.size() << " " << d_selTerms.size() << " " << d_sharedTerms.size() << std::endl; + Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl; Trace("dt-cg") << "Build indices..." << std::endl; std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > > index; std::map< Node, unsigned > arity; //populate indices - for( unsigned r=0; r<2; r++ ){ - unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size(); - for( unsigned i=0; i<functionTerms; i++ ){ - TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i]; - if( f1.getNumChildren()>0 ){ - Assert(d_equalityEngine.hasTerm(f1)); - Trace("dt-cg-debug") << "...build for " << f1 << std::endl; - //break into index based on operator, and type of first argument (since some operators are parametric) - Node op = f1.getOperator(); - TypeNode tn = f1[0].getType(); - std::vector< TNode > reps; - bool has_trigger_arg = false; - for( unsigned j=0; j<f1.getNumChildren(); j++ ){ - reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) ); - if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_DATATYPES ) ){ - has_trigger_arg = true; - } - } - //only may contribute to care pairs if has at least one trigger argument - if( has_trigger_arg ){ - index[tn][op].addTerm( f1, reps ); - arity[op] = reps.size(); - } + unsigned functionTerms = d_functionTerms.size(); + for( unsigned i=0; i<functionTerms; i++ ){ + TNode f1 = d_functionTerms[i]; + Assert(d_equalityEngine.hasTerm(f1)); + Trace("dt-cg-debug") << "...build for " << f1 << std::endl; + //break into index based on operator, and type of first argument (since some operators are parametric) + Node op = f1.getOperator(); + TypeNode tn = f1[0].getType(); + std::vector< TNode > reps; + bool has_trigger_arg = false; + for( unsigned j=0; j<f1.getNumChildren(); j++ ){ + reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) ); + if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_DATATYPES ) ){ + has_trigger_arg = true; } } + //only may contribute to care pairs if has at least one trigger argument + if( has_trigger_arg ){ + index[tn][op].addTerm( f1, reps ); + arity[op] = reps.size(); + } } //for each index for( std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > >::iterator iti = index.begin(); iti != index.end(); ++iti ){ @@ -1607,11 +1602,13 @@ void TheoryDatatypes::collectTerms( Node n ) { //} if( n.getKind() == APPLY_CONSTRUCTOR ){ Debug("datatypes") << " Found constructor " << n << endl; - d_consTerms.push_back( n ); + if( n.getNumChildren()>0 ){ + d_functionTerms.push_back( n ); + } }else{ if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ - d_selTerms.push_back( n ); + d_functionTerms.push_back( n ); //we must also record which selectors exist Trace("dt-collapse-sel") << " Found selector " << n << endl; Node rep = getRepresentative( n[0] ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index f3963f972..a1882d171 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -181,10 +181,8 @@ private: std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending_merge; - /** All the constructor terms that the theory has seen */ - context::CDList<TNode> d_consTerms; - /** All the selector terms that the theory has seen */ - context::CDList<TNode> d_selTerms; + /** All the function terms that the theory has seen */ + context::CDList<TNode> d_functionTerms; /** counter for forcing assignments (ensures fairness) */ unsigned d_dtfCounter; /** expand definition skolem functions */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 52d71a8a9..f2af6452b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -456,11 +456,6 @@ void TheoryStrings::preRegisterTerm(TNode n) { ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp"; throw LogicException(ss.str()); } - }else{ - //collect extended functions here: some may not be asserted to strings (such as those with return type Int), - // but we need to record them so they are treated properly - std::map< Node, bool > visited; - collectExtendedFuncTerms( n, visited ); } switch( n.getKind() ) { case kind::EQUAL: { @@ -475,19 +470,26 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; } default: { - if( n.getType().isString() ) { + TypeNode tn = n.getType(); + if( tn.isString() ) { registerTerm( n, 0 ); // FMF if( n.getKind() == kind::VARIABLE && options::stringFMF() ){ d_input_vars.insert(n); } d_equalityEngine.addTerm(n); - } else if (n.getType().isBoolean()) { + } else if (tn.isBoolean()) { // Get triggered for both equal and dis-equal d_equalityEngine.addTriggerPredicate(n); } else { // Function applications/predicates d_equalityEngine.addTerm(n); + if( options::stringExp() ){ + //collect extended functions here: some may not be asserted to strings (such as those with return type Int), + // but we need to record them so they are treated properly + std::map< Node, bool > visited; + collectExtendedFuncTerms( n, visited ); + } } //concat terms do not contribute to theory combination? TODO: verify if( n.hasOperator() && kindToTheoryId( n.getKind() )==THEORY_STRINGS && n.getKind()!=kind::STRING_CONCAT ){ @@ -499,6 +501,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { } Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { + Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; return node; } |