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, 37 insertions, 20 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c87753d8d..a80177429 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1268,25 +1268,22 @@ void SmtEngine::setDefaults() {
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
-
-  //for finite model finding
-  if( ! options::instWhenMode.wasSetByUser()){
-    //instantiate only on last call
-    if( options::fmfInstEngine() ){
-      Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
-      options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
+  //local theory extensions 
+  if( options::localTheoryExt() ){
+    //no E-matching?
+    if( !options::instMaxLevel.wasSetByUser() ){
+      options::instMaxLevel.set( 0 );
     }
   }
   if( d_logic.hasCardinalityConstraints() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
   }
-  if( options::recurseCbqi() ){
-    options::cbqi.set( true );
-  }
   if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
     options::fmfBoundInt.set( true );
   }
+  //now have determined whether fmfBoundInt is on/off
+  //apply fmfBoundInt options
   if( options::fmfBoundInt() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
@@ -1301,6 +1298,35 @@ void SmtEngine::setDefaults() {
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
+  if( options::fmfFunWellDefined() ){
+    if( !options::finiteModelFind.wasSetByUser() ){
+      options::finiteModelFind.set( true );
+    }
+  }
+  
+  //now, have determined whether finite model find is on/off
+  //apply finite model finding options
+  if( options::finiteModelFind() ){
+    if( !options::eMatching.wasSetByUser() ){
+      options::eMatching.set( options::fmfInstEngine() );
+    }
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+    //for finite model finding
+    if( ! options::instWhenMode.wasSetByUser()){
+      //instantiate only on last call
+      if( options::eMatching() ){
+        Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
+        options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
+      }
+    }
+  }
+  
+  //implied options...
+  if( options::recurseCbqi() ){
+    options::cbqi.set( true );
+  }
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
@@ -1342,16 +1368,7 @@ void SmtEngine::setDefaults() {
       options::conjectureGen.set( false );
     }
   }
-  if( options::fmfFunWellDefined() ){
-    if( !options::finiteModelFind.wasSetByUser() ){
-      options::finiteModelFind.set( true );
-    }
-  }
-  if( options::finiteModelFind() ){
-    if( !options::quantConflictFind.wasSetByUser() ){
-      options::quantConflictFind.set( false );
-    }
-  }
+
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
     if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){