diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 10:31:47 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 10:33:24 -0500 |
commit | c431410d0bd4a688d5d446f906d80634424dcd53 (patch) | |
tree | 8b13a5598a0ed201744e0a44669f8ade1eac2af3 /src/theory/logic_info.h | |
parent | fccff6adcc0a69273a54110596214f7927a96033 (diff) |
Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
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 |