From 55499c51c818ce1488c63e8e42841eb1293db922 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Nov 2016 10:35:46 -0600
Subject: [PATCH] Minor fixes related to ExtTheory + incremental, fixes bug760.

---
 src/theory/strings/theory_strings.cpp |  2 +-
 src/theory/theory.cpp                 | 17 +++++++++++++----
 src/theory/theory.h                   |  1 +
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ade5428ca..26e6908da 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1133,7 +1133,7 @@ void TheoryStrings::checkInit() {
                   }
                   //infer the equality
                   sendInference( exp, n.eqNode( nc ), "I_Norm" );
-                }else{
+                }else if( d_extt->hasFunctionKind( n.getKind() ) ){
                   //mark as congruent : only process if neither has been reduced
                   d_extt->markCongruent( nc, n );
                 }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 1c0a03e9c..2d8ea9fa8 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -324,7 +324,8 @@ void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node,
   if( !n.isConst() ){
     if( visited.find( n )==visited.end() ){
       visited[n] = true;
-      //treat terms not belonging to this theory as leaf
+      //treat terms not belonging to this theory as leaf  
+      //  AJR TODO : should include terms not belonging to this theory (commented below)
       if( n.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           collectVars( n[i], vars, visited );
@@ -349,6 +350,7 @@ void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std
       //do substitution, rewrite
       Node n = terms[i];
       std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
+      Trace("extt-debug") << "Check extf : " << n << std::endl;
       Assert( iti!=d_extf_info.end() );
       for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
         if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){
@@ -544,6 +546,8 @@ void ExtTheory::registerTermRec( Node n, std::map< Node, bool >& visited ) {
 
 //mark reduced
 void ExtTheory::markReduced( Node n, bool contextDepend ) {
+  registerTerm( n );
+  Assert( d_ext_func_terms.find( n )!=d_ext_func_terms.end() );
   d_ext_func_terms[n] = false;
   if( !contextDepend ){
     d_ci_inactive.insert( n );
@@ -563,14 +567,19 @@ void ExtTheory::markReduced( Node n, bool contextDepend ) {
 
 //mark congruent
 void ExtTheory::markCongruent( Node a, Node b ) {
+  Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl;
+  registerTerm( a );
+  registerTerm( b );
   NodeBoolMap::const_iterator it = d_ext_func_terms.find( b );
   if( it!=d_ext_func_terms.end() ){
-    if( d_ext_func_terms.find( a )==d_ext_func_terms.end() ){
-      d_ext_func_terms[a] = (*it).second;
-    }else{
+    if( d_ext_func_terms.find( a )!=d_ext_func_terms.end() ){
       d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
+    }else{
+      Assert( false );
     }
     d_ext_func_terms[b] = false;
+  }else{
+    Assert( false );
   }
 }
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index ffcec7c0c..fd8cffa9f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -1027,6 +1027,7 @@ public:
   virtual ~ExtTheory(){}
   //add extf kind
   void addFunctionKind( Kind k ) { d_extf_kind[k] = true; }
+  bool hasFunctionKind( Kind k ) { return d_extf_kind.find( k )!=d_extf_kind.end(); }
   //register term
   //  adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called
   void registerTerm( Node n );
-- 
2.30.2