From c431410d0bd4a688d5d446f906d80634424dcd53 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Apr 2014 10:31:47 -0500 Subject: 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. --- src/theory/logic_info.h | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/theory/logic_info.h') 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 -- cgit v1.2.3