From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Jul 2020 11:48:40 +0000 (-0500)
Subject: Always interleave theory combination with quantifiers (#4703)
X-Git-Tag: cvc5-1.0.0~3143
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=767380812cff0b8299ddf0784c149c80d2e6ecbd;p=cvc5.git

Always interleave theory combination with quantifiers (#4703)

This removes an option setting that made quantifiers always run at full effort (before theory combination) when an undecidable theory was present. The intuition is that such theories may also be unfair wrt theory combination, so quantifiers might as well "join them" at full effort.

However, this option modification significantly hurts our performance in terms of timeouts on verification benchmarks from Facebook, where theory combination needs to run but quantifiers (alone) is preempting it from running. The correct solution is in fact to have other theories interleave with theory combination with the same policy as quantifiers (I've opened CVC4/cvc4-wishues#74).
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index abd44dac7..4ce4b8db8 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -852,17 +852,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     options::finiteModelFind.set(true);
   }
 
-  // if it contains a theory with non-termination, do not strictly enforce that
-  // quantifiers and theory combination must be interleaved
-  if (logic.isTheoryEnabled(THEORY_STRINGS)
-      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
-  {
-    if (!options::instWhenStrictInterleave.wasSetByUser())
-    {
-      options::instWhenStrictInterleave.set(false);
-    }
-  }
-
   if (options::instMaxLevel() != -1)
   {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"