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.

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