diff options
Diffstat (limited to 'src/theory/logic_info.h')
| -rw-r--r-- | src/theory/logic_info.h | 7 |
1 files changed, 7 insertions, 0 deletions
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. */ |