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.

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index c6f38f29815c84aaef0b5479165ebd7dd11a0ce8..c3fa664d9f39b5ce0d18dbad9cf59bc64d871798 100644 (file)
--- 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<Node> 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 ab3dbea9556ac07700172f9fd7eb18879c76fe55..1e78d103ef421a41524624e383dcebe7fd9f3077 100644 (file)
--- 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 6214737ad19d2fa9cc49a83d052f6d9173bd42c4..ccd177b7ddc4e7c38d5f2ec2f53de3abef1b2855 100644 (file)
--- 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 68a2fb9a36223e0523ba2a4ea086441a0befe27a..c631404158923202abe126c7931229b801b57cce 100644 (file)
--- 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)