Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.

1 files changed, 32 insertions, 27 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 511103019..65b976b4a 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -47,7 +47,7 @@ d_quantEngine( qe ), d_f( f ){
         d_mg->setActiveAdd(true);
       }
     }else{
-      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption );
+      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
       //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
       //d_mg->setActiveAdd();
     }
@@ -385,29 +385,7 @@ 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 ){
@@ -438,9 +416,36 @@ 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 );
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
+  if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+    if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
+      bool hasVar = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( n[i].getKind()==INST_CONSTANT ){
+          hasVar = true;
+          if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
+            vars.push_back( n[i] );
+          }else{
+            //do not allow duplicate variables
+            return false;
+          }
+        }else{
+          //do not allow nested function applications
+          return false;
+        }
+      }
+      if( hasVar ){
+        patTerms.push_back( n );
+      }
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
+        return false;
+      } 
+    }
+  }
+  return true;
 }
 
 void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){