diff options
Diffstat (limited to 'src/theory/logic_info.h')
-rw-r--r-- | src/theory/logic_info.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index c7b5c58f9..2448898c0 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -155,21 +155,25 @@ public: /** Are integers in this logic? */ bool areIntegersUsed() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); return d_integers; } /** Are reals in this logic? */ bool areRealsUsed() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); return d_reals; } /** Does this logic only linear arithmetic? */ bool isLinear() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); return d_linear || d_differenceLogic; } /** Does this logic only permit difference reasoning? (implies linear) */ bool isDifferenceLogic() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); return d_differenceLogic; } |