From 920343a4a5586297dd98305b83785207025083b8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Mar 2020 15:25:06 -0500 Subject: [PATCH] Remove local theory extension option (#4048) This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0. --- src/options/quantifiers_options.toml | 9 --------- src/smt/smt_engine.cpp | 6 ------ 2 files changed, 15 deletions(-) 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); -- 2.30.2