diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/fp/fp_converter.cpp | 6 | ||||
| -rw-r--r-- | src/theory/logic_info.cpp | 21 |
2 files changed, 17 insertions, 10 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index a69cf8c96..fbdce8cd5 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -157,17 +157,17 @@ symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); }; symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); }; void traits::precondition(const bool b) { - Assert(b); + AlwaysAssert(b); return; } void traits::postcondition(const bool b) { - Assert(b); + AlwaysAssert(b); return; } void traits::invariant(const bool b) { - Assert(b); + AlwaysAssert(b); return; } diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 1712bb30a..e21d1f630 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -17,9 +17,10 @@ **/ #include "theory/logic_info.h" -#include <string> #include <cstring> +#include <iostream> #include <sstream> +#include <string> #include "base/cvc4_assert.h" #include "expr/kind.h" @@ -207,13 +208,15 @@ bool LogicInfo::operator==(const LogicInfo& other) const { PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); + bool res = d_cardinalityConstraints == other.d_cardinalityConstraints + && d_higherOrder == other.d_higherOrder; if(isTheoryEnabled(theory::THEORY_ARITH)) { 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; + && d_differenceLogic == other.d_differenceLogic && res; } else { - return true; + return res; } } @@ -227,13 +230,15 @@ bool LogicInfo::operator<=(const LogicInfo& other) const { } PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); + bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints) + && (!d_higherOrder || other.d_higherOrder); if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { 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); + && (d_differenceLogic || !other.d_differenceLogic) && res; } else { - return true; + return res; } } @@ -247,13 +252,15 @@ bool LogicInfo::operator>=(const LogicInfo& other) const { } PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); + bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints) + && (d_higherOrder || !other.d_higherOrder); if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { 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); + && (!d_differenceLogic || other.d_differenceLogic) && res; } else { - return true; + return res; } } |