diff options
Diffstat (limited to 'src/theory/logic_info.h')
-rw-r--r-- | src/theory/logic_info.h | 35 |
1 files changed, 29 insertions, 6 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index a502041f5..dc88cc9f4 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -47,12 +47,18 @@ class CVC4_PUBLIC LogicInfo { std::vector<bool> d_theories; /**< set of active theories */ size_t d_sharingTheories; /**< count of theories that need sharing */ - // for arithmetic - bool d_integers; /**< are integers used in this logic? */ - bool d_reals; /**< are reals used in this logic? */ - bool d_linear; /**< linear-only arithmetic in this logic? */ - bool d_differenceLogic; /**< difference-only arithmetic in this logic? */ - bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */ + /** are integers used in this logic? */ + bool d_integers; + /** are reals used in this logic? */ + bool d_reals; + /** linear-only arithmetic in this logic? */ + bool d_linear; + /** difference-only arithmetic in this logic? */ + bool d_differenceLogic; + /** cardinality constraints in this logic? */ + bool d_cardinalityConstraints; + /** higher-order constraints in this logic? */ + bool d_higherOrder; bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */ @@ -141,6 +147,9 @@ public: /** Does this logic allow cardinality constraints? */ bool hasCardinalityConstraints() const; + /** Is this a higher order logic? */ + bool isHigherOrder() const; + // MUTATORS /** @@ -204,6 +213,20 @@ public: /** Permit nonlinear arithmetic in this logic. */ void arithNonLinear(); + // for cardinality constraints + + /** Enable the use of cardinality constraints in this logic. */ + void enableCardinalityConstraints(); + /** Disable the use of cardinality constraints in this logic. */ + void disableCardinalityConstraints(); + + // for higher-order + + /** Enable the use of higher-order in this logic. */ + void enableHigherOrder(); + /** Disable the use of higher-order in this logic. */ + void disableHigherOrder(); + // LOCKING FUNCTIONALITY /** Lock this LogicInfo, disabling further mutation and allowing queries */ |