Minor fix to strings, cleanup in datatypes.

5 files changed, 48 insertions, 40 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;
 }
 
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 771b9f031..3daf646ab 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -76,7 +76,8 @@ TESTS = \
   type002.smt2 \
   crash-1019.smt2 \
   norn-31.smt2 \
-  strings-native-simple.cvc
+  strings-native-simple.cvc \
+  cmu-2db2-extf-reg.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2
new file mode 100644
index 000000000..b513494b8
--- /dev/null
+++ b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun s () String)
+
+(assert (and (not (not (= (ite (= (str.indexof s "bar" 1) (- 1)) 1 0) 0))) (not (not (= (ite (= (str.indexof s "bar" 1) 3) 1 0) 0)))))
+
+(check-sat)