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, 10 insertions, 0 deletions

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index c079eecf9..78f4996b8 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -37,6 +37,7 @@ LogicInfo::LogicInfo() :
   d_reals(true),
   d_linear(true),// for now, "everything enabled" doesn't include non-linear arith
   d_differenceLogic(false),
+  d_cardinalityConstraints(false),
   d_locked(false) {
 
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
@@ -52,6 +53,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
   d_reals(false),
   d_linear(false),
   d_differenceLogic(false),
+  d_cardinalityConstraints(false),
   d_locked(false) {
 
   setLogicString(logicString);
@@ -66,6 +68,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) :
   d_reals(false),
   d_linear(false),
   d_differenceLogic(false),
+  d_cardinalityConstraints(false),
   d_locked(false) {
 
   setLogicString(logicString);
@@ -97,6 +100,9 @@ std::string LogicInfo::getLogicString() const {
         ss << "UF";
         ++seen;
       }
+      if( d_cardinalityConstraints ){
+        ss << "C";
+      }
       if(d_theories[THEORY_BV]) {
         ss << "BV";
         ++seen;
@@ -191,6 +197,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_UF);
         p += 2;
       }
+      if(!strncmp(p, "C", 1 )) {
+        d_cardinalityConstraints = true;
+        p += 1;
+      }
       // allow BV or DT in either order
       if(!strncmp(p, "BV", 2)) {
         enableTheory(THEORY_BV);