From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 22 Oct 2020 18:06:51 +0000 (+0200)
Subject: Use theoryof-mode=type for QF_NRA (#5326)
X-Git-Tag: cvc5-1.0.0~2668
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7aba0c8580d5153fee99b4d59345e33c39c893b;p=cvc5.git

Use theoryof-mode=type for QF_NRA (#5326)

We've observed that our QF_NRA solving benefits significantly from --theoryof-mode=type across the board (of other options that influence QF_NRA solving). This PR sets type as the new default for QF_NRA solving.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4402beba2..27959a6bc 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -604,7 +604,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
         && !logic.isTheoryEnabled(THEORY_STRINGS)
         && !logic.isTheoryEnabled(THEORY_SETS)
-        && !logic.isTheoryEnabled(THEORY_BAGS))
+        && !logic.isTheoryEnabled(THEORY_BAGS)
+        && !(logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+             && !logic.isQuantified()))
     {
       Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
       options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);