From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 2 Oct 2020 15:25:29 +0000 (+0200)
Subject: Allow for theory combination of strings with nonlinear real arithmetic. (#5111)
X-Git-Tag: cvc5-1.0.0~2765
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f396917c481de7a57782a5daf31992c37d7d964;p=cvc5.git

Allow for theory combination of strings with nonlinear real arithmetic. (#5111)

This PR makes sure that enabling strings and nonlinear real arithmetic at the same time works fine.
Right now, the configuration for strings enforces linear arithmetic if no integers are enabled, in particular for NRA.

Fixed #5109.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 79490045b..468e246c4 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -546,8 +546,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     LogicInfo log(logic.getUnlockedCopy());
     // Strings requires arith for length constraints, and also UF
     needsUf = true;
-    if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()
-        || !logic.areIntegersUsed())
+    if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
     {
       Notice()
           << "Enabling linear integer arithmetic because strings are enabled"
@@ -556,6 +555,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       log.enableIntegers();
       log.arithOnlyLinear();
     }
+    else if (!logic.areIntegersUsed())
+    {
+      Notice() << "Enabling integer arithmetic because strings are enabled"
+               << std::endl;
+      log.enableIntegers();
+    }
     logic = log;
     logic.lock();
   }