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.

2 files changed, 26 insertions, 3 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 8d70e4ffc..4d45d9148 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -36,6 +36,7 @@ namespace CVC4 {
 namespace expr {
   namespace attr {
     struct DatatypeIndexTag {};
+    struct DatatypeConsIndexTag {};
     struct DatatypeFiniteTag {};
     struct DatatypeWellFoundedTag {};
     struct DatatypeFiniteComputedTag {};
@@ -45,6 +46,7 @@ namespace expr {
 }/* CVC4::expr namespace */
 
 typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
+typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
 typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
 typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr;
 typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
@@ -81,6 +83,20 @@ size_t Datatype::indexOf(Expr item) {
   }
 }
 
+size_t Datatype::cindexOf(Expr item) {
+  ExprManagerScope ems(item);
+  CheckArgument(item.getType().isSelector(),
+                item,
+                "arg must be a datatype selector");
+  TNode n = Node::fromExpr(item);
+  if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
+    return cindexOf( item[0] );
+  }else{
+    Assert(n.hasAttribute(DatatypeConsIndexAttr()));
+    return n.getAttribute(DatatypeConsIndexAttr());
+  }
+}
+
 void Datatype::resolve(ExprManager* em,
                        const std::map<std::string, DatatypeType>& resolutions,
                        const std::vector<Type>& placeholders,
@@ -103,7 +119,7 @@ void Datatype::resolve(ExprManager* em,
   d_resolved = true;
   size_t index = 0;
   for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
-    (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements);
+    (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index);
     Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
   }
@@ -401,7 +417,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::vector<Type>& placeholders,
                                   const std::vector<Type>& replacements,
                                   const std::vector< SortConstructorType >& paramTypes,
-                                  const std::vector< DatatypeType >& paramReplacements)
+                                  const std::vector< DatatypeType >& paramReplacements, size_t cindex)
   throw(IllegalArgumentException, DatatypeResolutionException) {
 
   CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
@@ -447,6 +463,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
       }
       (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
     }
+    Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex);
     Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
     (*i).d_resolved = true;
   }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 99a303950..02e0b6be8 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -191,7 +191,7 @@ private:
                const std::vector<Type>& placeholders,
                const std::vector<Type>& replacements,
                const std::vector< SortConstructorType >& paramTypes,
-               const std::vector< DatatypeType >& paramReplacements)
+               const std::vector< DatatypeType >& paramReplacements, size_t cindex)
     throw(IllegalArgumentException, DatatypeResolutionException);
   friend class Datatype;
 
@@ -434,6 +434,12 @@ public:
    */
   static size_t indexOf(Expr item) CVC4_PUBLIC;
 
+  /**
+   * Get the index of constructor corresponding to selector.  (Zero is
+   * always the first index.)
+   */
+  static size_t cindexOf(Expr item) CVC4_PUBLIC;
+
   /** The type for iterators over constructors. */
   typedef DatatypeConstructorIterator iterator;
   /** The (const) type for iterators over constructors. */