diff options
Diffstat (limited to 'src/theory/logic_info.h')
-rw-r--r-- | src/theory/logic_info.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index a0777ae70..1c4b69b15 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -52,6 +52,7 @@ class CVC4_PUBLIC LogicInfo { 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? */ bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */ @@ -175,6 +176,11 @@ public: CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); return d_differenceLogic; } + /** Does this logic allow cardinality constraints? */ + bool hasCardinalityConstraints() const { + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_cardinalityConstraints; + } // MUTATORS |