diff options
41 files changed, 163 insertions, 66 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index cdb799864..2c7dfb333 100644 --- 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 3def5696b..36c2479ad 100644 --- 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 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() { diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index cbb04604e..5eac6a3da 100644 --- 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 2ac299177..4a7267a60 100644 --- 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 e1baeed9c..7bd65b72b 100644 --- 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 33806cf75..25fca9f03 100644 --- 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 b0ea1b39e..defd35f9a 100644 --- 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 3b3a14c89..6608e6618 100644 --- 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 366906464..292f091ac 100644 --- 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 ade068152..59a0f46d2 100644 --- 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 0def70806..353ed74eb 100644 --- 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 index 000000000..22f8abfc4 --- /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 index 000000000..8e5474918 --- /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 445b8a21e..64f92d9a6 100644 --- 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 8a8494873..783408889 100644 --- 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 04b06e1f5..e24df9d23 100644 --- 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 3b9310748..69a033001 100644 --- 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 e19260d63..d5052f675 100644 --- 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 3bf15c384..4b911e576 100644 --- 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 5dce6ddca..5f70bcf22 100644 --- 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 b0d39ff44..55689d8ac 100644 --- 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 b0bc3079c..c287b5169 100644 --- 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 a1360dc22..0d754dada 100644 --- 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 21fd61f9f..0b341ac6a 100644 --- 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 f5d7fe32d..c4c28f527 100644 --- 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 790d7037f..d22cec0b9 100644 --- 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 e71ab231f..fa29cd911 100644 --- 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 9b05a3d52..df2a56b32 100644 --- 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 2e5d4eac2..45d86dcac 100644 --- 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 4c8302e9f..d9e12c7b4 100644 --- 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 f8070cdb8..1aefde5ff 100644 --- 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 d45fd1453..d2a21fa60 100644 --- 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 47d322a77..0b04bc5fe 100644 --- 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 686708230..da1ea0996 100644 --- 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 51c9eb8a9..4557ba5c8 100644 --- 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 84c224715..f3c1febbb 100644 --- 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 ab50bcb1d..e83cf3420 100644 --- 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 95dbbc5fc..5d242cee6 100644 --- 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 af39f7559..601021a7f 100644 --- 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 b70adc688..e2e59ba49 100644 --- 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 */ |