From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 3 Jul 2021 19:11:57 +0000 (-0700)
Subject: Fix performance of string regression (#6832)
X-Git-Tag: cvc5-1.0.0~1530
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=698d244a00618a0399bce9e15eddef52f68b8c94;p=cvc5.git

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 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<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 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)