From 767380812cff0b8299ddf0784c149c80d2e6ecbd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Jul 2020 06:48:40 -0500 Subject: [PATCH] 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). --- src/smt/set_defaults.cpp | 11 ----------- 1 file changed, 11 deletions(-) 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" -- 2.30.2