Only enable transcendentals if logic is N[I]RAT (#2052)

1 files changed, 56 insertions, 15 deletions

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 1c9e3d0ef..f2c6df0b6 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -36,6 +36,7 @@ LogicInfo::LogicInfo()
       d_sharingTheories(0),
       d_integers(true),
       d_reals(true),
+      d_transcendentals(true),
       d_linear(false),
       d_differenceLogic(false),
       d_cardinalityConstraints(false),
@@ -53,6 +54,7 @@ LogicInfo::LogicInfo(std::string logicString)
       d_sharingTheories(0),
       d_integers(false),
       d_reals(false),
+      d_transcendentals(false),
       d_linear(false),
       d_differenceLogic(false),
       d_cardinalityConstraints(false),
@@ -69,6 +71,7 @@ LogicInfo::LogicInfo(const char* logicString)
       d_sharingTheories(0),
       d_integers(false),
       d_reals(false),
+      d_transcendentals(false),
       d_linear(false),
       d_differenceLogic(false),
       d_cardinalityConstraints(false),
@@ -156,6 +159,18 @@ bool LogicInfo::areRealsUsed() const {
   return d_reals;
 }
 
+bool LogicInfo::areTranscendentalsUsed() const
+{
+  PrettyCheckArgument(d_locked,
+                      *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH),
+                      *this,
+                      "Arithmetic not used in this LogicInfo; cannot ask "
+                      "whether transcendentals are used");
+  return d_transcendentals;
+}
+
 bool LogicInfo::isLinear() const {
   PrettyCheckArgument(d_locked, *this,
                       "This LogicInfo isn't locked yet, and cannot be queried");
@@ -193,11 +208,10 @@ bool LogicInfo::operator==(const LogicInfo& other) const {
   PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
   if(isTheoryEnabled(theory::THEORY_ARITH)) {
-    return
-        d_integers == other.d_integers &&
-        d_reals == other.d_reals &&
-        d_linear == other.d_linear &&
-        d_differenceLogic == other.d_differenceLogic;
+    return d_integers == other.d_integers && d_reals == other.d_reals
+           && d_transcendentals == other.d_transcendentals
+           && d_linear == other.d_linear
+           && d_differenceLogic == other.d_differenceLogic;
   } else {
     return true;
   }
@@ -214,11 +228,10 @@ bool LogicInfo::operator<=(const LogicInfo& other) const {
   PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
-    return
-        (!d_integers || other.d_integers) &&
-        (!d_reals || other.d_reals) &&
-        (d_linear || !other.d_linear) &&
-        (d_differenceLogic || !other.d_differenceLogic);
+    return (!d_integers || other.d_integers) && (!d_reals || other.d_reals)
+           && (!d_transcendentals || other.d_transcendentals)
+           && (d_linear || !other.d_linear)
+           && (d_differenceLogic || !other.d_differenceLogic);
   } else {
     return true;
   }
@@ -235,11 +248,10 @@ bool LogicInfo::operator>=(const LogicInfo& other) const {
   PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
-    return
-        (d_integers || !other.d_integers) &&
-        (d_reals || !other.d_reals) &&
-        (!d_linear || other.d_linear) &&
-        (!d_differenceLogic || other.d_differenceLogic);
+    return (d_integers || !other.d_integers) && (d_reals || !other.d_reals)
+           && (d_transcendentals || !other.d_transcendentals)
+           && (!d_linear || other.d_linear)
+           && (!d_differenceLogic || other.d_differenceLogic);
     } else {
     return true;
   }
@@ -301,6 +313,7 @@ std::string LogicInfo::getLogicString() const {
           ss << (areIntegersUsed() ? "I" : "");
           ss << (areRealsUsed() ? "R" : "");
           ss << "A";
+          ss << (areTranscendentalsUsed() ? "T" : "");
         }
         ++seen;
       }
@@ -471,11 +484,21 @@ void LogicInfo::setLogicString(std::string logicString)
         enableReals();
         arithNonLinear();
         p += 3;
+        if (*p == 'T')
+        {
+          arithTranscendentals();
+          p += 1;
+        }
       } else if(!strncmp(p, "NIRA", 4)) {
         enableIntegers();
         enableReals();
         arithNonLinear();
         p += 4;
+        if (*p == 'T')
+        {
+          arithTranscendentals();
+          p += 1;
+        }
       }
       if(!strncmp(p, "FS", 2)) {
         enableTheory(THEORY_SETS);
@@ -581,11 +604,28 @@ void LogicInfo::disableReals() {
   }
 }
 
+void LogicInfo::arithTranscendentals()
+{
+  PrettyCheckArgument(
+      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  d_logicString = "";
+  d_transcendentals = true;
+  if (!d_reals)
+  {
+    enableReals();
+  }
+  if (d_linear)
+  {
+    arithNonLinear();
+  }
+}
+
 void LogicInfo::arithOnlyDifference() {
   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = true;
+  d_transcendentals = false;
 }
 
 void LogicInfo::arithOnlyLinear() {
@@ -593,6 +633,7 @@ void LogicInfo::arithOnlyLinear() {
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = false;
+  d_transcendentals = false;
 }
 
 void LogicInfo::arithNonLinear() {