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

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index cdb79986437d693499a4dab943e027cecfe8c386..2c7dfb333f3f88fec61762e05ef91beeed466329 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -51,8 +51,13 @@ void Smt2::addArithmeticOperators() {
   Parser::addOperator(kind::LEQ);
   Parser::addOperator(kind::GT);
   Parser::addOperator(kind::GEQ);
-  
+
+  // NOTE: this operator is non-standard
   addOperator(kind::POW, "^");
+}
+
+void Smt2::addTranscendentalOperators()
+{
   addOperator(kind::EXPONENTIAL, "exp");
   addOperator(kind::SINE, "sin");
   addOperator(kind::COSINE, "cos");
@@ -66,7 +71,6 @@ void Smt2::addArithmeticOperators() {
   addOperator(kind::ARCCOSECANT, "arccsc");
   addOperator(kind::ARCSECANT, "arcsec");
   addOperator(kind::ARCCOTANGENT, "arccot");
-
   addOperator(kind::SQRT, "sqrt");
 }
 
@@ -249,6 +253,8 @@ void Smt2::addTheory(Theory theory) {
     Parser::addOperator(kind::DIVISION);
     break;
 
+  case THEORY_TRANSCENDENTALS: addTranscendentalOperators(); break;
+
   case THEORY_QUANTIFIERS:
     break;
 
@@ -486,6 +492,11 @@ void Smt2::setLogic(std::string name) {
     } else if(d_logic.areRealsUsed()) {
       addTheory(THEORY_REALS);
     }
+
+    if (d_logic.areTranscendentalsUsed())
+    {
+      addTheory(THEORY_TRANSCENDENTALS);
+    }
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 3def5696bfe065dc155c71790327af1da425657d..36c2479adba9a344e1930746cc0b5bef04ecc0ef 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -40,21 +40,23 @@ class Smt2 : public Parser {
   friend class ParserBuilder;
 
 public:
-  enum Theory {
-    THEORY_ARRAYS,
-    THEORY_BITVECTORS,
-    THEORY_CORE,
-    THEORY_DATATYPES,
-    THEORY_INTS,
-    THEORY_REALS,
-    THEORY_REALS_INTS,
-    THEORY_QUANTIFIERS,
-    THEORY_SETS,
-    THEORY_STRINGS,
-    THEORY_UF,
-    THEORY_FP,
-    THEORY_SEP
-  };
+ enum Theory
+ {
+   THEORY_ARRAYS,
+   THEORY_BITVECTORS,
+   THEORY_CORE,
+   THEORY_DATATYPES,
+   THEORY_INTS,
+   THEORY_REALS,
+   THEORY_TRANSCENDENTALS,
+   THEORY_REALS_INTS,
+   THEORY_QUANTIFIERS,
+   THEORY_SETS,
+   THEORY_STRINGS,
+   THEORY_UF,
+   THEORY_FP,
+   THEORY_SEP
+ };
 
 private:
   bool d_logicSet;
@@ -186,6 +188,12 @@ public:
       ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB";
       parseError(ss.str());
     }
+    else if (isOperatorEnabled(name))
+    {
+      std::stringstream ss;
+      ss << "Symbol `" << name << "' is shadowing a theory function symbol";
+      parseError(ss.str());
+    }
   }
 
   void includeFile(const std::string& filename);
@@ -386,6 +394,8 @@ private:
 
   void addArithmeticOperators();
 
+  void addTranscendentalOperators();
+
   void addBitvectorOperators();
 
   void addStringOperators();

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 1c9e3d0eff3c469f20b124b34564ca1118ef2437..f2c6df0b65c62ff11dc748889a00d582a395fe5d 100644 (file)
--- 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() {

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index cbb04604ef2eb2851da552a913d278d8a5925058..5eac6a3da1800ac2b61b30e306b03eb60b9eae14 100644 (file)
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -51,6 +51,8 @@ class CVC4_PUBLIC LogicInfo {
   bool d_integers;
   /** are reals used in this logic? */
   bool d_reals;
+  /** transcendentals in this logic? */
+  bool d_transcendentals;
   /** linear-only arithmetic in this logic? */
   bool d_linear;
   /** difference-only arithmetic in this logic? */
@@ -138,6 +140,9 @@ public:
   /** Are reals in this logic? */
   bool areRealsUsed() const;
 
+  /** Are transcendentals in this logic? */
+  bool areTranscendentalsUsed() const;
+
   /** Does this logic only linear arithmetic? */
   bool isLinear() const;
 
@@ -206,6 +211,8 @@ public:
   void enableReals();
   /** Disable the use of reals in this logic. */
   void disableReals();
+  /** Enable the use of transcendentals in this logic. */
+  void arithTranscendentals();
   /** Only permit difference arithmetic in this logic. */
   void arithOnlyDifference();
   /** Only permit linear arithmetic in this logic. */

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 2ac299177f10bc6c3cad7e6257c50722c79af96e..4a7267a60d34b5bca95202643aa7dd635ba7afe2 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -513,6 +513,8 @@ REG0_TESTS = \
        regress0/parser/as.smt2 \
        regress0/parser/constraint.smt2 \
        regress0/parser/declarefun-emptyset-uf.smt2 \
+       regress0/parser/shadow_fun_symbol_all.smt2 \
+       regress0/parser/shadow_fun_symbol_nirat.smt2 \
        regress0/parser/strings20.smt2 \
        regress0/parser/strings25.smt2 \
        regress0/precedence/and-not.cvc \
@@ -602,8 +604,8 @@ REG0_TESTS = \
        regress0/quantifiers/floor.smt2 \
        regress0/quantifiers/is-even-pred.smt2 \
        regress0/quantifiers/is-int.smt2 \
-       regress0/quantifiers/issue2031-bv-var-elim.smt2 \
        regress0/quantifiers/issue1805.smt2 \
+       regress0/quantifiers/issue2031-bv-var-elim.smt2 \
        regress0/quantifiers/issue2033-macro-arith.smt2 \
        regress0/quantifiers/lra-triv-gn.smt2 \
        regress0/quantifiers/macros-int-real.smt2 \

diff --git a/test/regress/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/regress0/nl/nta/cos-sig-value.smt2
index e1baeed9c95b476c33c7b022b004202925ab0d9b..7bd65b72bead644ad423cad98809f47a644cdb6c 100644 (file)
--- a/test/regress/regress0/nl/nta/cos-sig-value.smt2
+++ b/test/regress/regress0/nl/nta/cos-sig-value.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (not (= (cos 0.0) 1.0)))

diff --git a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
index 33806cf75b85c657fc311aac0477b3d5f53bf787..25fca9f03081eb035c60fbc09911016ef5f28326 100644 (file)
--- a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
+++ b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun x () Real)
 
 (assert (> (exp (- (/ 1 2))) 0.65))

diff --git a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
index b0ea1b39e262a44bdb67df553d9ac0ee62cb0afc..defd35f9ae1d691904145abff2a7d9a8b488f7e6 100644 (file)
--- a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
+++ b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun x () Real)
 
 (assert (< (exp (- (/ 1 2))) 0.6))

diff --git a/test/regress/regress0/nl/nta/exp1-ub.smt2 b/test/regress/regress0/nl/nta/exp1-ub.smt2
index 3b3a14c89e8c05fdea396256c1bf367f61a997be..6608e66186ab6de7c194ce46d3ad565c9d4a12ad 100644 (file)
--- a/test/regress/regress0/nl/nta/exp1-ub.smt2
+++ b/test/regress/regress0/nl/nta/exp1-ub.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress0/nl/nta/sin-sym.smt2 b/test/regress/regress0/nl/nta/sin-sym.smt2
index 3669064642f78b1fbd87d869feefa9fb3de7eaf3..292f091ac247d9c3bac96a4e2559a1764dcd124b 100644 (file)
--- a/test/regress/regress0/nl/nta/sin-sym.smt2
+++ b/test/regress/regress0/nl/nta/sin-sym.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --nl-ext-tplanes
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (not (= (+ (sin 0.2) (sin (- 0.2))) 0.0)))

diff --git a/test/regress/regress0/nl/nta/sqrt-simple.smt2 b/test/regress/regress0/nl/nta/sqrt-simple.smt2
index ade068152c6141e2ca68df289b2a14ce58cf4a34..59a0f46d2c4e4595fab87d89d2deb6959675caa6 100644 (file)
--- a/test/regress/regress0/nl/nta/sqrt-simple.smt2
+++ b/test/regress/regress0/nl/nta/sqrt-simple.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (> x 0.0))

diff --git a/test/regress/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/regress0/nl/nta/tan-rewrite.smt2
index 0def708063214dd78c2e3d334bdc23dd16f91990..353ed74eb56e34fcd13c8f4578ed837587ef685b 100644 (file)
--- a/test/regress/regress0/nl/nta/tan-rewrite.smt2
+++ b/test/regress/regress0/nl/nta/tan-rewrite.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress0/parser/shadow_fun_symbol_all.smt2 b/test/regress/regress0/parser/shadow_fun_symbol_all.smt2
new file mode 100644 (file)
index 0000000..22f8abf
--- /dev/null
+++ b/test/regress/regress0/parser/shadow_fun_symbol_all.smt2
@@ -0,0 +1,5 @@
+; EXPECT: Symbol `sin' is shadowing a theory function symbol
+; SCRUBBER: grep -o "Symbol `sin' is shadowing a theory function symbol"
+; EXIT: 1
+(set-logic ALL)
+(declare-fun sin (Real) Real)

diff --git a/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2 b/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2
new file mode 100644 (file)
index 0000000..8e54749
--- /dev/null
+++ b/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2
@@ -0,0 +1,5 @@
+; EXPECT: Symbol `exp' is shadowing a theory function symbol
+; SCRUBBER: grep -o "Symbol `exp' is shadowing a theory function symbol"
+; EXIT: 1
+(set-logic NIRAT)
+(declare-fun exp (Real) Real)

diff --git a/test/regress/regress1/nl/NAVIGATION2.smt2 b/test/regress/regress1/nl/NAVIGATION2.smt2
index 445b8a21ea0fd203e98671aa6cf48eb1c19decb1..64f92d9a6c361c7aeacce1f77224316ab458314a 100644 (file)
--- a/test/regress/regress1/nl/NAVIGATION2.smt2
+++ b/test/regress/regress1/nl/NAVIGATION2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :source |printed by MathSAT|)
 (declare-fun X () Real)
 

diff --git a/test/regress/regress1/nl/arctan2-expdef.smt2 b/test/regress/regress1/nl/arctan2-expdef.smt2
index 8a84948738913c3faf2c58ab3ed43556772d9a46..7834088897c5da8e0ae05d47787603da202e74e1 100644 (file)
--- a/test/regress/regress1/nl/arctan2-expdef.smt2
+++ b/test/regress/regress1/nl/arctan2-expdef.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (set-option :arith-no-partial-fun true)
 (declare-fun lat1 () Real)

diff --git a/test/regress/regress1/nl/arrowsmith-050317.smt2 b/test/regress/regress1/nl/arrowsmith-050317.smt2
index 04b06e1f5ed1ea55e51f1a1aec0534f03af18bcf..e24df9d23486e901ab59c3de9d3ff75475cdd30f 100644 (file)
--- a/test/regress/regress1/nl/arrowsmith-050317.smt2
+++ b/test/regress/regress1/nl/arrowsmith-050317.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.location.0__AT0@0 () Bool)

diff --git a/test/regress/regress1/nl/bad-050217.smt2 b/test/regress/regress1/nl/bad-050217.smt2
index 3b9310748ffca3d0dbbee357d7b9b357a6191b4d..69a0330017123cf6aa7753029ef1693a93c08c11 100644 (file)
--- a/test/regress/regress1/nl/bad-050217.smt2
+++ b/test/regress/regress1/nl/bad-050217.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.y__AT0@0 () Real)

diff --git a/test/regress/regress1/nl/cos-bound.smt2 b/test/regress/regress1/nl/cos-bound.smt2
index e19260d63132ab98c8d5059ec4f6fefb62621bf1..d5052f675b1db59f10e5fbbc698057f860015f35 100644 (file)
--- a/test/regress/regress1/nl/cos-bound.smt2
+++ b/test/regress/regress1/nl/cos-bound.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (declare-fun x () Real)
 (assert (> (cos x) 1.0))
 (check-sat)

diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2
index 3bf15c384d4b58418e4d1b4b0d7c14f92c9ae100..4b911e576dcd1090084835e90e776cc5dcea9644 100644 (file)
--- a/test/regress/regress1/nl/cos1-tc.smt2
+++ b/test/regress/regress1/nl/cos1-tc.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
 ; EXPECT: unknown
-(set-logic UFNRA)
+(set-logic UFNRAT)
 (declare-fun f (Real) Real)
 
 (assert (= (f 0.0) (cos 1)))

diff --git a/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 b/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
index 5dce6ddca9bdc3e4ded65ad4cde97d66f2c94113..5f70bcf22248dde0b93772359b7effdfc1d626fc 100644 (file)
--- a/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
+++ b/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.y__AT0@0 () Real)
 (declare-fun instance.x__AT0@0 () Real)

diff --git a/test/regress/regress1/nl/exp-4.5-lt.smt2 b/test/regress/regress1/nl/exp-4.5-lt.smt2
index b0d39ff44416217cc847c9ae703f0d4af4399c35..55689d8ac75978daad6ff36aedf4ea4f47afd06d 100644 (file)
--- a/test/regress/regress1/nl/exp-4.5-lt.smt2
+++ b/test/regress/regress1/nl/exp-4.5-lt.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun x () Real)
 
 (assert (> (exp x) 2000.0))

diff --git a/test/regress/regress1/nl/exp1-lb.smt2 b/test/regress/regress1/nl/exp1-lb.smt2
index b0bc3079cb06159cfff917b4d16ac36c5e883521..c287b51692b5fb3a2e47013a45b9303538bb4510 100644 (file)
--- a/test/regress/regress1/nl/exp1-lb.smt2
+++ b/test/regress/regress1/nl/exp1-lb.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/exp_monotone.smt2 b/test/regress/regress1/nl/exp_monotone.smt2
index a1360dc220442c07b969cb509850fa9e4813ad4e..0d754dadab8d5c34a02d396ee343d9fb7430e771 100644 (file)
--- a/test/regress/regress1/nl/exp_monotone.smt2
+++ b/test/regress/regress1/nl/exp_monotone.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (declare-fun y () Real)

diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2
index 21fd61f9f6a772dc86b1420f224aade8211c5735..0b341ac6a1e763bcd9995aaac07da08087d8b076 100644 (file)
--- a/test/regress/regress1/nl/mirko-050417.smt2
+++ b/test/regress/regress1/nl/mirko-050417.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun t@0 () Real)
 (declare-fun y2@0 () Real)

diff --git a/test/regress/regress1/nl/sin-compare-across-phase.smt2 b/test/regress/regress1/nl/sin-compare-across-phase.smt2
index f5d7fe32def141b0dfcd81ed7fafa0d1236c549f..c4c28f527e269dc7caaaf6c674c001b81f28beca 100644 (file)
--- a/test/regress/regress1/nl/sin-compare-across-phase.smt2
+++ b/test/regress/regress1/nl/sin-compare-across-phase.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --nl-ext-tplanes
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (< (sin 3.1) (sin 3.3)))

diff --git a/test/regress/regress1/nl/sin-compare.smt2 b/test/regress/regress1/nl/sin-compare.smt2
index 790d7037ff9f4dbe71c8f6628f5f213050168402..d22cec0b9ec204edc6dacf315248609ba26222e8 100644 (file)
--- a/test/regress/regress1/nl/sin-compare.smt2
+++ b/test/regress/regress1/nl/sin-compare.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --nl-ext-tplanes
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (or (> (sin 0.1) (sin 0.2)) (> (sin 6.4) (sin 6.5)))) 

diff --git a/test/regress/regress1/nl/sin-init-tangents.smt2 b/test/regress/regress1/nl/sin-init-tangents.smt2
index e71ab231f2bf21126885fe13823e277dfde23320..fa29cd911a45d05b4084f8220568ffc312a96174 100644 (file)
--- a/test/regress/regress1/nl/sin-init-tangents.smt2
+++ b/test/regress/regress1/nl/sin-init-tangents.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (assert (or (> (sin 0.8) 0.9) (< (sin (- 0.7)) (- 0.75)) (= (sin 3.0) 0.8)))
 (check-sat)

diff --git a/test/regress/regress1/nl/sin-sign.smt2 b/test/regress/regress1/nl/sin-sign.smt2
index 9b05a3d520c5dc5be428f84ed5ca151cad4f8083..df2a56b32cbb93851f5f87c16ba036cc5e9002b6 100644 (file)
--- a/test/regress/regress1/nl/sin-sign.smt2
+++ b/test/regress/regress1/nl/sin-sign.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --nl-ext-tplanes
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (or (< (sin 0.2) (- 0.1)) (> (sin (- 0.05)) 0.05))) 

diff --git a/test/regress/regress1/nl/sin-sym2.smt2 b/test/regress/regress1/nl/sin-sym2.smt2
index 2e5d4eac2ce0c1577e434ae5ba6e1791f8620090..45d86dcac91f79ad54402e428dc04dbafa998a7e 100644 (file)
--- a/test/regress/regress1/nl/sin-sym2.smt2
+++ b/test/regress/regress1/nl/sin-sym2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --nl-ext-tplanes
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (declare-fun y () Real)

diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2
index 4c8302e9f3733a1721026ba9aafa5dc5208028cd..d9e12c7b42121ec7440b88750341b6a0b63fef8d 100644 (file)
--- a/test/regress/regress1/nl/sin1-deq-sat.smt2
+++ b/test/regress/regress1/nl/sin1-deq-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/sin1-lb.smt2 b/test/regress/regress1/nl/sin1-lb.smt2
index f8070cdb8fec1edb017c89a78d1aedbc1bf57f10..1aefde5ff205e910498441d96ed43ff037bd3b02 100644 (file)
--- a/test/regress/regress1/nl/sin1-lb.smt2
+++ b/test/regress/regress1/nl/sin1-lb.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2
index d45fd1453ae35d0ea1cbc4aa662a1b181d67c22a..d2a21fa60be64575251058883a8f5da6a0be783d 100644 (file)
--- a/test/regress/regress1/nl/sin1-sat.smt2
+++ b/test/regress/regress1/nl/sin1-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/sin1-ub.smt2 b/test/regress/regress1/nl/sin1-ub.smt2
index 47d322a77a3235aa04dfb7d2193e69d74ba099e5..0b04bc5fe4551932ced8e4beab244f725c497fa3 100644 (file)
--- a/test/regress/regress1/nl/sin1-ub.smt2
+++ b/test/regress/regress1/nl/sin1-ub.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/sin2-lb.smt2 b/test/regress/regress1/nl/sin2-lb.smt2
index 686708230e47e5999013616853295ba683e96c7a..da1ea0996be2b0c389cc4cb3381eac8b2760d520 100644 (file)
--- a/test/regress/regress1/nl/sin2-lb.smt2
+++ b/test/regress/regress1/nl/sin2-lb.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/sin2-ub.smt2 b/test/regress/regress1/nl/sin2-ub.smt2
index 51c9eb8a95ee8c8a15e4bee16d22aeb285736d42..4557ba5c8f839d751108271e076d633605623158 100644 (file)
--- a/test/regress/regress1/nl/sin2-ub.smt2
+++ b/test/regress/regress1/nl/sin2-ub.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/regress/regress1/nl/sugar-ident-2.smt2 b/test/regress/regress1/nl/sugar-ident-2.smt2
index 84c22471514da3ac0faf8fc808754f99a1ef751d..f3c1febbb8073ccfe09c10e7a72bd2564785f9a2 100644 (file)
--- a/test/regress/regress1/nl/sugar-ident-2.smt2
+++ b/test/regress/regress1/nl/sugar-ident-2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x1 () Real)
 (declare-fun x2 () Real)

diff --git a/test/regress/regress1/nl/sugar-ident-3.smt2 b/test/regress/regress1/nl/sugar-ident-3.smt2
index ab50bcb1da6d464b9fd057d77b3446e5107db027..e83cf3420b120b30a745ab952d260eb360833fa1 100644 (file)
--- a/test/regress/regress1/nl/sugar-ident-3.smt2
+++ b/test/regress/regress1/nl/sugar-ident-3.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun a6 () Bool)
 (assert (= a6 (> (* (csc 1.0) (sin 1.0)) 1.0)))

diff --git a/test/regress/regress1/nl/sugar-ident.smt2 b/test/regress/regress1/nl/sugar-ident.smt2
index 95dbbc5fce9993a3c81833ded596fedbeffe3e31..5d242cee6d3d34005b3b2f84f7d1caceff3ce2c5 100644 (file)
--- a/test/regress/regress1/nl/sugar-ident.smt2
+++ b/test/regress/regress1/nl/sugar-ident.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x1 () Real)
 (declare-fun x2 () Real)

diff --git a/test/regress/regress1/nl/tan-rewrite2.smt2 b/test/regress/regress1/nl/tan-rewrite2.smt2
index af39f7559e354a9de82fb831f42afdbec8eced20..601021a7f64292065659df8f125f6a11192af719 100644 (file)
--- a/test/regress/regress1/nl/tan-rewrite2.smt2
+++ b/test/regress/regress1/nl/tan-rewrite2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index b70adc6885f221ac7b1223d07d8199bfcc3da47a..e2e59ba49c49bb208609d4c07e8eaaf4a21c3033 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -322,6 +322,7 @@ public:
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -339,6 +340,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -355,6 +357,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -372,6 +375,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -389,6 +393,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -406,6 +411,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -424,6 +430,7 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -495,6 +502,7 @@ public:
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
     TS_ASSERT( !info.isLinear() );
 
     TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
@@ -561,6 +569,7 @@ public:
     TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
+    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
 
     // check copy is unchanged
     info = info.getUnlockedCopy();
@@ -580,6 +589,7 @@ public:
     TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
+    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
 
     // check all-included logic
     info = info.getUnlockedCopy();
@@ -600,6 +610,7 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
 
     // check copy is unchanged
     info = info.getUnlockedCopy();
@@ -619,6 +630,7 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
   }
 
   void eq(const LogicInfo& logic1, const LogicInfo& logic2) const {
@@ -966,6 +978,7 @@ public:
     lt("QF_IDL", "QF_UFIDL");
     lt("QF_IDL", "QF_NIA");
     nc("QF_IDL", "QF_NRA");
+    nc("QF_IDL", "QF_NRAT");
     lt("QF_IDL", "QF_AUFNIRA");
     nc("QF_IDL", "LRA");
     nc("QF_IDL", "NRA");
@@ -1075,6 +1088,7 @@ public:
     nc("QF_NRA", "AUFLIA");
     nc("QF_NRA", "AUFLIRA");
     lt("QF_NRA", "AUFNIRA");
+    lt("QF_NRA", "QF_NRAT");
 
     gt("QF_AUFNIRA", "QF_UF");
     gt("QF_AUFNIRA", "QF_LRA");
@@ -1100,6 +1114,7 @@ public:
     nc("QF_AUFNIRA", "AUFLIA");
     nc("QF_AUFNIRA", "AUFLIRA");
     lt("QF_AUFNIRA", "AUFNIRA");
+    lt("QF_AUFNIRA", "QF_AUFNIRAT");
 
     nc("LRA", "QF_UF");
     gt("LRA", "QF_LRA");
@@ -1300,6 +1315,7 @@ public:
     gt("AUFNIRA", "AUFLIA");
     gt("AUFNIRA", "AUFLIRA");
     eq("AUFNIRA", "AUFNIRA");
+    lt("AUFNIRA", "AUFNIRAT");
   }
 
 };/* class LogicInfoWhite */