From 698d244a00618a0399bce9e15eddef52f68b8c94 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 3 Jul 2021 12:11:57 -0700 Subject: [PATCH] Fix performance of string regression (#6832) Regression cmu-dis-0707-3.smt2 has been timing out when using an ASan build after commit a4f38d6. Before that commit --strings-exp implicitly enabled --fmf-bound. After the commit, the solver was supposed to apply the same reasoning but only to interal quantifiers and without enabling --fmf-bound. However, the commit missed some options checks that now also have to check whether --strings-exp is enabled. This commit updates those option checks. With this fix, we get a slightly different value for bug590.smt2 after replying unknown. This commit updates the regression to be more lenient with the value returned. --- src/theory/quantifiers/fmf/full_model_check.cpp | 3 ++- src/theory/quantifiers/fmf/model_builder.cpp | 4 +++- src/theory/quantifiers_engine.cpp | 3 ++- test/regress/regress1/bug590.smt2 | 3 ++- 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index c6f38f298..c3fa664d9 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -17,6 +17,7 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" +#include "options/strings_options.h" #include "options/theory_options.h" #include "options/uf_options.h" #include "theory/quantifiers/first_order_model.h" @@ -706,7 +707,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i d_star_insts[f].push_back(i); continue; } - if (options::fmfBound()) + if (options::fmfBound() || options::stringExp()) { std::vector cond; cond.push_back(d_quant_cond[f]); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index ab3dbea95..1e78d103e 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/fmf/model_builder.h" #include "options/quantifiers_options.h" +#include "options/strings_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/instantiate.h" @@ -52,7 +53,8 @@ void QModelBuilder::finishInit() } bool QModelBuilder::optUseModel() { - return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound(); + return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound() + || options::stringExp(); } bool QModelBuilder::preProcessBuildModel(TheoryModel* m) { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6214737ad..ccd177b7d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -19,6 +19,7 @@ #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "options/strings_options.h" #include "options/uf_options.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/equality_query.h" @@ -67,7 +68,7 @@ QuantifiersEngine::QuantifiersEngine( // Finite model finding requires specialized ways of building the model. // We require constructing the model here, since it is required for // initializing the CombinationEngine and the rest of quantifiers engine. - if (options::fmfBound() + if (options::fmfBound() || options::stringExp() || (options::finiteModelFind() && (options::mbqiMode() == options::MbqiMode::FMC || options::mbqiMode() == options::MbqiMode::TRUST))) diff --git a/test/regress/regress1/bug590.smt2 b/test/regress/regress1/bug590.smt2 index 68a2fb9a3..c63140415 100644 --- a/test/regress/regress1/bug590.smt2 +++ b/test/regress/regress1/bug590.smt2 @@ -1,5 +1,6 @@ +; SCRUBBER: grep -o "unknown\|((charlst2 (" ; EXPECT: unknown -; EXPECT: ((charlst2 ((as const (Array Int String)) ""))) +; EXPECT: ((charlst2 ( (set-logic ALL) (set-option :strings-exp true) -- 2.30.2