More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.

3 files changed, 39 insertions, 4 deletions

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 0e365c875..cb772a31f 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -71,9 +71,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
         }
         Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
         
-        Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << " to ";
+        Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
+        Trace("fmf-fun-def") << "  to " << std::endl;
         assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
-        Trace("fmf-fun-def") << assertions[i] << std::endl;
+        Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
         fd_assertions.push_back( i );
       }
     }
@@ -86,7 +87,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
     Assert( constraints.empty() );
     if( n!=assertions[i] ){
       n = Rewriter::rewrite( n );
-      Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << " to " << n << std::endl;
+      Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
+      Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
+      Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
       assertions[i] = n;
     }
   }
@@ -139,7 +142,7 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co
       }else{
         //must add at higher level
       }
-      return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( AND, c );
+      return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c );
     }
   }else{
     //simplify term
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index b2b8e7197..511103019 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -385,6 +385,30 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
   }
 }
 
+bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) {
+  if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+    bool hasVar = false;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( n[i].getKind()==APPLY_UF ){
+        return false;
+      }else if( n[i].getKind()==INST_CONSTANT ){
+        hasVar = true;
+        //if( std::find( var_found.begin(), var_found.end(), n[i]
+      }
+    }
+    if( hasVar ){
+      patTerms.push_back( n );
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !isLocalTheoryExt2( n, var_found, patTerms ) ){
+        return false;
+      } 
+    }
+  }
+  return true;
+}
+
 bool Trigger::isBooleanTermTrigger( Node n ) {
   if( n.getKind()==ITE ){
     //check for boolean term converted to ITE
@@ -414,6 +438,11 @@ bool Trigger::isPureTheoryTrigger( Node n ) {
   }
 }
 
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& patTerms ) {
+  std::vector< Node > var_found;
+  return isLocalTheoryExt2( n, var_found, patTerms );
+}
+
 void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
   std::map< Node, bool > patMap;
   if( filterInst ){
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 75ada4f83..482701a82 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -95,6 +95,8 @@ private:
   static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
   static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
+  /** is local theory extensions term */
+  static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms );
 public:
   //different strategies for choosing trigger terms
   enum {
@@ -111,6 +113,7 @@ public:
   static bool isSimpleTrigger( Node n );
   static bool isBooleanTermTrigger( Node n );
   static bool isPureTheoryTrigger( Node n );
+  static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms );
   /** return data structure for producing matches for this trigger. */
   static InstMatchGenerator* getInstMatchGenerator( Node n );
   static Node getInversionVariable( Node n );