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 abd44dac7314b1231cf50c3666d7ff2d8cc29b61..4ce4b8db8659cae76c01f0b426f412eda333a909 100644 (file)
--- 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"