From 1339e2a3b884d34a9c27eb45bb6847a493fe0365 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Aug 2020 15:36:38 -0500 Subject: Remove instantiation model true option (#4861) This was an option that rejected instantiations that are true according to the current model's equality engine. This option was never helpful and will be burdensome to maintain with new updates to equality engine infrastructure. --- src/options/quantifiers_options.toml | 17 ----------------- 1 file changed, 17 deletions(-) (limited to 'src/options/quantifiers_options.toml') diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index b62468cdd..4b130158c 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -492,15 +492,6 @@ header = "options/quantifiers_options.h" default = "true" help = "allow theory combination to happen once initially, before quantifier strategies are run" -[[option]] - name = "quantModelEe" - category = "regular" - long = "quant-model-ee" - type = "bool" - default = "false" - read_only = true - help = "use equality engine of model for last call effort" - [[option]] name = "instMaxLevel" category = "regular" @@ -823,14 +814,6 @@ header = "options/quantifiers_options.h" default = "true" help = "do not consider instances of quantified formulas that are currently entailed" -[[option]] - name = "instNoModelTrue" - category = "regular" - long = "inst-no-model-true" - type = "bool" - default = "false" - help = "do not consider instances of quantified formulas that are currently true in model, if it is available" - [[option]] name = "qcfEagerTest" category = "regular" -- cgit v1.2.3