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/theory/strings/theory_strings.cpp | |
parent | d5d05e4723581c86808a866af1a9f20343ed36dc (diff) |
Minor fix to strings, cleanup in datatypes.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 17 |
1 files changed, 10 insertions, 7 deletions
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; } |