From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Mar 2020 20:25:06 +0000 (-0500)
Subject: Remove local theory extension option (#4048)
X-Git-Tag: cvc5-1.0.0~3499
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=920343a4a5586297dd98305b83785207025083b8;p=cvc5.git

Remove local theory extension option (#4048)

This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e104101ef..6e0460ae9 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1925,15 +1925,6 @@ header = "options/quantifiers_options.h"
 
 ### Local theory extensions options
 
-[[option]]
-  name       = "localTheoryExt"
-  category   = "regular"
-  long       = "local-t-ext"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "do instantiation based on local theory extensions"
-
 [[option]]
   name       = "lteRestrictInstClosure"
   category   = "regular"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fbc5821ce..5fc0189c3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1814,12 +1814,6 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  //local theory extensions
-  if( options::localTheoryExt() ){
-    if( !options::instMaxLevel.wasSetByUser() ){
-      options::instMaxLevel.set( 0 );
-    }
-  }
   if( options::instMaxLevel()!=-1 ){
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
     options::cbqi.set(false);