From c431410d0bd4a688d5d446f906d80634424dcd53 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
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/parser/smt1/smt1.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/parser')

diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index f96a4e810..c19b0f872 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -84,7 +84,8 @@ public:
     THEORY_REALS,
     THEORY_REALS_INTS,
     THEORY_STRINGS,
-    THEORY_QUANTIFIERS
+    THEORY_QUANTIFIERS,
+    THEORY_CARDINALITY_CONSTRAINT
   };
 
 private:
-- 
cgit v1.2.3