From aaf5d11d3506c5f946c6b6edec2240d0a5b484d0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 May 2022 17:58:11 -0500 Subject: [PATCH] Add option to send all instantiations in a bounded range (#8796) There is a block of code in FMF instantiation that is questionable whether it is helpful, in particular for dealing with string reductions for long strings. --- src/options/quantifiers_options.toml | 8 ++++++++ src/theory/quantifiers/fmf/full_model_check.cpp | 3 ++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index a4c33c946..2d6d74bb4 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -659,6 +659,14 @@ name = "Quantifiers" default = "1000" help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted" +[[option]] + name = "fmfBoundBlast" + category = "expert" + long = "fmf-bound-blast" + type = "bool" + default = "false" + help = "send all instantiations for bounded ranges in a single round" + ### Conflict-based instantiation options [[option]] diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 6a419f08e..7c66a3e9a 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -919,7 +919,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, Trace("fmc-exh-debug") << std::endl; int index = riter.increment(); Trace("fmc-exh-debug") << "Incremented index " << index << std::endl; - if( !riter.isFinished() ){ + if (!options().quantifiers.fmfBoundBlast && !riter.isFinished()) + { if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0 && riter.d_enum_type[index] == ENUM_CUSTOM) { -- 2.30.2