diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-22 20:06:51 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-22 20:06:51 +0200 |
| commit | a7aba0c8580d5153fee99b4d59345e33c39c893b (patch) | |
| tree | bca5ab1672ed411119d53273c5e8c4d571142eea /src/smt/set_defaults.cpp | |
| parent | d758a32f5bb1361d766a71c3d2cdaeacb8f39a76 (diff) | |
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.
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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); |