Merge remote-tracking branch 'upstream/master' into sets

42 files changed, 1013 insertions, 443 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 27d1249a1..427282490 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1189,7 +1189,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
 
   // Set up the datatype specifications.
   for(unsigned i = 0; i < names.size(); ++i) {
-    CVC4::Datatype dt(names[i]);
+    CVC4::Datatype dt(names[i], false);
     CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size");
     CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size");
     for(unsigned j = 0; j < constructors[i].size(); ++j) {
diff --git a/src/cvc4.i b/src/cvc4.i
index c0042b513..fcd5a8470 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -71,7 +71,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %template(vectorString) std::vector< std::string >;
 %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
 %template(pairStringType) std::pair< std::string, CVC4::Type >;
-%template(setType) std::set< CVC4::Type >;
+%template(setOfType) std::set< CVC4::Type >;
 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
 // This is unfortunate, but seems to be necessary; if we leave NULL
diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index 43c3395a4..8860e717b 100644
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -30,7 +30,7 @@
 
 /* otherwise, we have to define it */
 
-#if defined(__WIN32__) && !defined(__WIN64__)
+#if defined(__WIN32__) && !defined(_W64)
 
 #ifdef __cplusplus
 extern "C" {
@@ -45,12 +45,12 @@ struct timespec {
 }/* extern "C" */
 #endif /* __cplusplus */
 
-#else /* !__WIN32__ || __WIN64__ */
+#else /* !__WIN32__ || _W64 */
 
 /* get timespec from <time.h> */
 #include <time.h>
 
-#endif /* __WIN32__ && !__WIN64__ */
+#endif /* __WIN32__ && !_W64 */
 
 #ifdef __cplusplus
 extern "C" {
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 792c3cf9d..f9055f5db 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2018,7 +2018,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
         params.push_back( t ); }
       )* RBRACKET
     )?
-    { datatypes.push_back(Datatype(id, params));
+    { datatypes.push_back(Datatype(id, params, false));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
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:
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 659fc97d9..8dcebc5ee 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -344,6 +344,28 @@ command returns [CVC4::Command* cmd = NULL]
       Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
       $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
+  | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { /* add variables to parser state before parsing term */
+      Debug("parser") << "define const: '" << name << "'" << std::endl;
+      PARSER_STATE->pushScope(true);
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVarNames.begin(), iend = sortedVarNames.end();
+          i != iend;
+          ++i) {
+        terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
+      }
+    }
+    term[expr, expr2]
+    { PARSER_STATE->popScope();
+      // declare the name down here (while parsing term, signature
+      // must not be extended with the name itself; no recursion
+      // permitted)
+      Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
+      $cmd = new DefineFunctionCommand(name, func, terms, expr);
+    }
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
@@ -464,17 +486,8 @@ extendedCommand[CVC4::Command*& cmd]
 }
     /* Extended SMT-LIB set of commands syntax, not permitted in
      * --smtlib2 compliance mode. */
-  : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { /* open a scope to keep the UnresolvedTypes contained */
-      PARSER_STATE->pushScope(true); }
-    LPAREN_TOK /* parametric sorts */
-      ( symbol[name,CHECK_UNDECLARED,SYM_SORT] {
-        sorts.push_back( PARSER_STATE->mkSort(name) ); }
-      )*
-    RPAREN_TOK
-    LPAREN_TOK ( LPAREN_TOK datatypeDef[dts, sorts] RPAREN_TOK )+ RPAREN_TOK
-    { PARSER_STATE->popScope();
-      cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+  : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
+  | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
   | /* get model */
     GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetModelCommand(); }
@@ -496,7 +509,7 @@ extendedCommand[CVC4::Command*& cmd]
     sortSymbol[t,CHECK_DECLARED]
     { Expr c = PARSER_STATE->mkVar(name, t);
       $cmd = new DeclareFunctionCommand(name, c, t); }
-
+      
   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
@@ -603,6 +616,26 @@ extendedCommand[CVC4::Command*& cmd]
     { cmd = new SimplifyCommand(e); }
   ;
 
+
+datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
+@declarations {
+  std::vector<CVC4::Datatype> dts;
+  std::string name;
+  std::vector<Type> sorts;
+}
+  : { PARSER_STATE->checkThatLogicIsSet(); 
+    /* open a scope to keep the UnresolvedTypes contained */
+    PARSER_STATE->pushScope(true); }
+  LPAREN_TOK /* parametric sorts */
+  ( symbol[name,CHECK_UNDECLARED,SYM_SORT] {
+    sorts.push_back( PARSER_STATE->mkSort(name) ); }
+  )*
+  RPAREN_TOK
+  LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
+  { PARSER_STATE->popScope();
+  cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+  ;
+
 rewriterulesCommand[CVC4::Command*& cmd]
 @declarations {
   std::vector<std::pair<std::string, Type> > sortedVarNames;
@@ -1530,7 +1563,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals]
 /**
  * Parses a datatype definition
  */
-datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params]
+datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params]
 @init {
   std::string id;
 }
@@ -1548,7 +1581,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& p
         params.push_back( t ); }
       )* ']'
     )?*/ //AJR: this isn't necessary if we use z3's style
-    { datatypes.push_back(Datatype(id,params));
+    { datatypes.push_back(Datatype(id,params,isCo));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
@@ -1623,6 +1656,7 @@ AS_TOK : 'as';
 
 // extended commands
 DECLARE_DATATYPES_TOK : 'declare-datatypes';
+DECLARE_CODATATYPES_TOK : 'declare-codatatypes';
 GET_MODEL_TOK : 'get-model';
 ECHO_TOK : 'echo';
 REWRITE_RULE_TOK : 'assert-rewrite';
@@ -1633,6 +1667,7 @@ DECLARE_FUNS_TOK : 'declare-funs';
 DECLARE_PREDS_TOK : 'declare-preds';
 DEFINE_TOK : 'define';
 DECLARE_CONST_TOK : 'declare-const';
+DEFINE_CONST_TOK : 'define-const';
 SIMPLIFY_TOK : 'simplify';
 INCLUDE_TOK : 'include';
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 64b321613..e9e6ba857 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) {
     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
     Parser::addOperator(kind::APPLY_TESTER);
     Parser::addOperator(kind::APPLY_SELECTOR);
+    Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
     break;
 
   case THEORY_STRINGS:
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 4d784c383..63529c2a5 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::APPLY_CONSTRUCTOR:
     case kind::APPLY_SELECTOR:
+    case kind::APPLY_SELECTOR_TOTAL:
     case kind::APPLY_TESTER:
       toStream(op, n.getOperator(), depth, types, false);
       break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ea335f2e5..1250bc659 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_TESTER:
   case kind::APPLY_CONSTRUCTOR:
   case kind::APPLY_SELECTOR:
+  case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
     break;
 
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 4555aac51..c779af4ff 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -46,7 +46,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
   d_varCache(smt.d_userContext),
   d_termCache(smt.d_userContext),
   d_typeCache(),
-  d_datatypeCache() {
+  d_datatypeCache(),
+  d_datatypeReverseCache() {
 
   // set up our "false" and "true" conversions based on command-line option
   if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
@@ -116,6 +117,10 @@ static inline bool isBoolean(TNode top, unsigned i) {
 // to be for model-substitution, so the "in" is a Boolean-term-converted
 // node, and "as" is the original.  See how it's used in function
 // handling, below.
+//
+// Note this isn't the case any longer, and parts of what's below have
+// been repurposed for *forward* conversion, meaning this works in either
+// direction.
 Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
   if(in.getType() == as) {
     return in;
@@ -133,7 +138,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
     }
     Assert(as.isDatatype());
     const Datatype* dt2 = &as.getDatatype();
-    const Datatype* dt1 = d_datatypeCache[dt2];
+    const Datatype* dt1;
+    if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
+      dt1 = d_datatypeCache[dt2];
+    } else {
+      dt1 = d_datatypeReverseCache[dt2];
+    }
     Assert(dt1 != NULL, "expected datatype in cache");
     Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
     Node out;
@@ -142,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
       appctorb << (*dt2)[i].getConstructor();
       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
       }
       Node appctor = appctorb;
       if(i == 0) {
@@ -165,7 +175,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
       toParams.push_back(as[i + 1]);
     }
-    const Datatype* dt1 = d_datatypeCache[dt2];
+    const Datatype* dt1;
+    if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
+      dt1 = d_datatypeCache[dt2];
+    } else {
+      dt1 = d_datatypeReverseCache[dt2];
+    }
     Assert(dt1 != NULL, "expected datatype in cache");
     Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
     Node out;
@@ -176,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
         TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
         asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
-        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType);
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType);
       }
       Node appctor = appctorb;
       if(i == 0) {
@@ -213,9 +228,9 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
         }
         vector<Datatype> newDtVector;
         if(dt.isParametric()) {
-          newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters()));
+          newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false));
         } else {
-          newDtVector.push_back(Datatype(dt.getName() + "'"));
+          newDtVector.push_back(Datatype(dt.getName() + "'", false));
         }
         Datatype& newDt = newDtVector.front();
         Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
@@ -259,11 +274,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
           }
         }
         out = &newD;
+        d_datatypeReverseCache[&newD] = &dt;
         return newD;
       }
     }
   }
 
+  // this is identity; don't need the reverse cache
   out = &dt;
   return dt;
 
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index b289e3469..bdd9ff839 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -69,6 +69,8 @@ class BooleanTermConverter {
   BooleanTermTypeCache d_typeCache;
   /** The cache used during Boolean term datatype conversion */
   BooleanTermDatatypeCache d_datatypeCache;
+  /** A (reverse) cache for Boolean term datatype conversion */
+  BooleanTermDatatypeCache d_datatypeReverseCache;
 
   Node rewriteAs(TNode in, TypeNode as) throw();
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8586bc9da..36f9866f4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1112,7 +1112,7 @@ void SmtEngine::setDefaults() {
   if(!options::decisionMode.wasSetByUser()) {
     decision::DecisionMode decMode =
       // ALL_SUPPORTED
-      d_logic.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL :
+      d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
       ( // QF_BV
         (not d_logic.isQuantified() &&
           d_logic.isPure(THEORY_BV)
@@ -1153,9 +1153,7 @@ void SmtEngine::setDefaults() {
         // QF_LRA
         (not d_logic.isQuantified() &&
          d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
-         ) ||
-        // Quantifiers
-        d_logic.isQuantified()
+         )
         ? true : false
       );
 
@@ -1172,12 +1170,17 @@ void SmtEngine::setDefaults() {
       options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
     }
   }
-  if ( options::fmfBoundInt() ){
+  if( d_logic.hasCardinalityConstraints() ){
+    //must have finite model finding on
+    options::finiteModelFind.set( true );
+  }
+  if( options::fmfBoundInt() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
-    if( options::mbqiMode()!=quantifiers::MBQI_NONE &&
-        options::mbqiMode()!=quantifiers::MBQI_FMC &&
-        options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){
+    if( ! options::mbqiMode.wasSetByUser() ||
+        ( options::mbqiMode()!=quantifiers::MBQI_NONE &&
+          options::mbqiMode()!=quantifiers::MBQI_FMC &&
+          options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){
       //if bounded integers are set, use no MBQI by default
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index a731ff024..4c218b48c 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -57,10 +57,11 @@ void SmtEngine::checkProof() {
 
   Chat() << "checking proof..." << endl;
 
-  if(!d_logic.isPure(theory::THEORY_BOOL) &&
-     !d_logic.isPure(theory::THEORY_UF)) {
+  if( ! ( d_logic.isPure(theory::THEORY_BOOL) ||
+          ( d_logic.isPure(theory::THEORY_UF) &&
+            ! d_logic.hasCardinalityConstraints() ) ) ) {
     // no checking for these yet
-    Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl;
+    Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl;
     return;
   }
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index b3383e6c4..d140d1990 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -302,6 +302,7 @@ variable SKOLEM "skolem var"
 operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
+operator MU 2 "mu"
 
 parameterized CHAIN CHAIN_OP 2: "chained operator"
 constant CHAIN_OP \
@@ -334,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
+typerule MU ::CVC4::theory::builtin::MuTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 0ebcb31e8..3c8953e15 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -164,6 +164,24 @@ public:
   }
 };/* class LambdaTypeRule */
 
+class MuTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    if( n[0].getType(check) != nodeManager->boundVarListType() ) {
+      std::stringstream ss;
+      ss << "expected a bound var list for MU expression, got `"
+         << n[0].getType().toString() << "'";
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+    std::vector<TypeNode> argTypes;
+    for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) {
+      argTypes.push_back((*i).getType());
+    }
+    TypeNode rangeType = n[1].getType(check);
+    return nodeManager->mkFunctionType(argTypes, rangeType);
+  }
+};/* class MuTypeRule */
+
 class ChainTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 37a656555..dc85d0cd6 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -88,7 +88,7 @@ public:
       const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
       return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
     }
-    if(in.getKind() == kind::APPLY_SELECTOR &&
+    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
        (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) {
       // These strange (half-tuple-converted) terms can be created by
       // the system if you have something like "foo.1" for a tuple
@@ -118,7 +118,7 @@ public:
       Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl;
       return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
     }
-    if(in.getKind() == kind::APPLY_SELECTOR &&
+    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
        in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
       // Have to be careful not to rewrite well-typed expressions
       // where the selector doesn't match the constructor,
@@ -138,26 +138,25 @@ public:
                                    << std::endl;
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       }else{
-        if( options::dtRewriteErrorSel() ){
-          Node gt;
-          if( in.getType().isSort() ){
-            TypeEnumerator te(in.getType());
-            gt = *te;
-          }else{
-            gt = in.getType().mkGroundTerm();
-          }
-          TypeNode gtt = gt.getType();
-          //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
-          if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
-            gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                  NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
-          }
-          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                     << "Rewrite trivial selector " << in
-                                     << " to distinguished ground term "
-                                     << in.getType().mkGroundTerm() << std::endl;
-          return RewriteResponse(REWRITE_DONE,gt );
+        //typically should not be called
+        Node gt;
+        if( in.getType().isSort() ){
+          TypeEnumerator te(in.getType());
+          gt = *te;
+        }else{
+          gt = in.getType().mkGroundTerm();
         }
+        TypeNode gtt = gt.getType();
+        //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+        if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
+          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+        }
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial selector " << in
+                                   << " to distinguished ground term "
+                                   << in.getType().mkGroundTerm() << std::endl;
+        return RewriteResponse(REWRITE_DONE,gt );
       }
     }
     if(in.getKind() == kind::TUPLE_SELECT &&
@@ -204,11 +203,17 @@ public:
       return RewriteResponse(REWRITE_DONE,
                              NodeManager::currentNM()->mkConst(true));
     }
-    if(in.getKind() == kind::EQUAL &&
-       checkClash(in[0], in[1])) {
-      Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl;
-      return RewriteResponse(REWRITE_DONE,
-                             NodeManager::currentNM()->mkConst(false));
+    if(in.getKind() == kind::EQUAL ) {
+      std::vector< Node > rew;
+      if( checkClash(in[0], in[1], rew) ){
+        Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl;
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
+      }else if( rew.size()==1 && rew[0]!=in ){
+        Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl;
+        return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] );
+      }else{
+        Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in << " " << in[0].getKind() << " " << in[1].getKind() << std::endl;
+      }
     }
 
     return RewriteResponse(REWRITE_DONE, in);
@@ -222,7 +227,7 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
-  static bool checkClash( Node n1, Node n2 ) {
+  static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
     if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
         (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
         (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
@@ -231,21 +236,73 @@ public:
       } else {
         Assert( n1.getNumChildren() == n2.getNumChildren() );
         for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
-          if( checkClash( n1[i], n2[i] ) ) {
+          if( checkClash( n1[i], n2[i], rew ) ) {
             return true;
           }
         }
       }
-    }else if( !isTermDatatype( n1 ) ){
-      //also check for clashes between non-datatypes
-      Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
-      eq = Rewriter::rewrite( eq );
-      if( eq==NodeManager::currentNM()->mkConst(false) ){
+    }else if( n1!=n2 ){
+      if( n1.isConst() && n2.isConst() ){
+        return true;        
+      }else{
+        Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+        rew.push_back( eq );
+      }
+    }
+    return false;
+  }
+  /** get instantiate cons */
+  static Node getInstCons( Node n, const Datatype& dt, int index, bool mkVar = false ) {
+    Type tspec;
+    if( dt.isParametric() ){
+      tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
+    }
+    std::vector< Node > children;
+    children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
+    for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
+      Node nc = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n );
+      if( mkVar ){
+        TypeNode tn = nc.getType();
+        if( dt.isParametric() ){
+          tn = TypeNode::fromType( tspec )[i];
+        }
+        nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" );
+      }
+      children.push_back( nc );
+    }
+    Node n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+    //add type ascription for ambiguous constructor types
+    if(!n_ic.getType().isComparableTo(n.getType())) {
+      Assert( dt.isParametric() );
+      Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
+      Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
+      Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
+      Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl;
+      children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                     NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] );
+      n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+      Assert( n_ic.getType()==n.getType() );
+    }
+    Assert( isInstCons( n_ic, dt, index ) );
+    //n_ic = Rewriter::rewrite( n_ic );
+    return n_ic;
+  }
+  static bool isInstCons( Node n, const Datatype& dt, int index ){
+    if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
+      const DatatypeConstructor& c = dt[index];
+      if( n.getOperator()==Node::fromExpr( c.getConstructor() ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( n[i].getKind()!=kind::APPLY_SELECTOR_TOTAL ||
+              n[i].getOperator()!=Node::fromExpr( c[i].getSelector() ) ){
+            return false;
+          }
+        }
         return true;
       }
     }
     return false;
   }
+
   /** is this term a datatype */
   static bool isTermDatatype( Node n ){
     TypeNode tn = n.getType();
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index bb6fd4373..b222738ae 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -39,6 +39,7 @@ cardinality TESTER_TYPE \
 parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application"
 
 parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application"
+parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)"
 
 parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
 
@@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \
 
 typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
+typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
 typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule
 typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule
 
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 1daa30981..fcf36648d 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -9,8 +9,8 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # then we do not rewrite such a selector term to an arbitrary ground term.  
 # For example, by default cvc4 considers cdr( nil ) = nil.  If this option is set, then
 # cdr( nil ) has no set value.
-expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
- disable rewriting incorrectly applied selectors to arbitrary ground term
+expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false
+ rewrite incorrectly applied selectors to arbitrary ground term
 option dtForceAssignment /--dt-force-assignment bool :default false :read-write
  force the datatypes solver to give specific values to all datatypes terms before answering sat
  
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8396e563e..eef25ca80 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -50,12 +50,15 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_labels( c ),
   d_selector_apps( c ),
   d_conflict( c, false ),
-  d_collectTermsCache( c ){
+  d_collectTermsCache( c ),
+  d_consTerms( c ),
+  d_selTerms( c ){
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
+  d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -123,13 +126,19 @@ void TheoryDatatypes::check(Effort e) {
 
   if( e == EFFORT_FULL ) {
     //check for cycles
-    checkCycles();
-    if( d_conflict ){
-      return;
-    }
+    bool addedFact;
+    do {
+      checkCycles();
+      addedFact = !d_pending.empty() || !d_pending_merge.empty();
+      flushPendingFacts();
+      if( d_conflict ){
+        return;
+      }
+    }while( addedFact );
+
     //check for splits
     Debug("datatypes-split") << "Check for splits " << e << endl;
-    bool addedFact = false;
+    addedFact = false;
     do {
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       while( !eqcs_i.isFinished() ){
@@ -141,61 +150,63 @@ void TheoryDatatypes::check(Effort e) {
           if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) {
             Trace("datatypes-debug") << "No constructor..." << std::endl;
             const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
-            //if only one constructor, then this term must be this constructor
-            if( dt.getNumConstructors()==1 ){
-              Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n );
-              d_pending.push_back( t );
-              d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true );
-              Trace("datatypes-infer") << "DtInfer : " << t << ", trivial" << std::endl;
-              d_infer.push_back( t );
-            }else{
-              std::vector< bool > pcons;
-              getPossibleCons( eqc, n, pcons );
-              //std::cout << "pcons " << n << " = ";
-              //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
-              //std::cout << std::endl;
-              //check if we do not need to resolve the constructor type for this equivalence class.
-              // this is if there are no selectors for this equivalence class, its possible values are infinite,
-              //  and we are not producing a model, then do not split.
-              int consIndex = -1;
-              bool needSplit = true;
-              for( unsigned int j=0; j<pcons.size(); j++ ) {
-                if( pcons[j] ) {
-                  if( consIndex==-1 ){
-                    consIndex = j;
-                  }
-                  if( !dt[ j ].isFinite() && !eqc->d_selectors ) {
-                    needSplit = false;
-                  }
+
+            std::vector< bool > pcons;
+            getPossibleCons( eqc, n, pcons );
+            //std::cout << "pcons " << n << " = ";
+            //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
+            //std::cout << std::endl;
+            //check if we do not need to resolve the constructor type for this equivalence class.
+            // this is if there are no selectors for this equivalence class, its possible values are infinite,
+            //  and we are not producing a model, then do not split.
+            int consIndex = -1;
+            bool needSplit = true;
+            for( unsigned int j=0; j<pcons.size(); j++ ) {
+              if( pcons[j] ) {
+                if( consIndex==-1 ){
+                  consIndex = j;
                 }
-              }
-              /*
-              if( !needSplit && mustSpecifyAssignment() ){
-                //for the sake of termination, we must choose the constructor of a ground term
-                //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
-                // TODO: this is probably not good enough, actually need fair enumeration strategy
-                Node groundTerm = n.getType().mkGroundTerm();
-                int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
-                if( pcons[index] ){
-                  consIndex = index;
+                if( !dt[ j ].isFinite() && !eqc->d_selectors ) {
+                  needSplit = false;
                 }
-                needSplit = true;
               }
-              */
-              if( needSplit && consIndex!=-1 ) {
-                Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
-                Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
-                test = Rewriter::rewrite( test );
-                NodeBuilder<> nb(kind::OR);
-                nb << test << test.notNode();
-                Node lemma = nb;
-                d_out->lemma( lemma );
-                d_out->requirePhase( test, true );
-                return;
+            }
+            /*
+            if( !needSplit && mustSpecifyAssignment() ){
+              //for the sake of termination, we must choose the constructor of a ground term
+              //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
+              // TODO: this is probably not good enough, actually need fair enumeration strategy
+              Node groundTerm = n.getType().mkGroundTerm();
+              int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
+              if( pcons[index] ){
+                consIndex = index;
+              }
+              needSplit = true;
+            }
+            */
+            if( needSplit && consIndex!=-1 ) {
+              //if only one constructor, then this term must be this constructor
+              if( dt.getNumConstructors()==1 ){
+                Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n );
+                d_pending.push_back( t );
+                d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true );
+                Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
+                d_infer.push_back( t );
               }else{
-                Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl;
+                  Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
+                  Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
+                  test = Rewriter::rewrite( test );
+                  NodeBuilder<> nb(kind::OR);
+                  nb << test << test.notNode();
+                  Node lemma = nb;
+                  d_out->lemma( lemma );
+                  d_out->requirePhase( test, true );
+                  return;
               }
+            }else{
+              Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
             }
+
           }else{
             Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
           }
@@ -318,6 +329,51 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
   flushPendingFacts();
 }
 
+Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
+  switch( n.getKind() ){
+  case kind::APPLY_SELECTOR: {
+    Node selector = n.getOperator();
+    Expr selectorExpr = selector.toExpr();
+    Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
+    if( options::dtRewriteErrorSel() ){
+      return sel;
+    }else{
+      size_t selectorIndex = Datatype::cindexOf(selectorExpr);
+      const Datatype& dt = Datatype::datatypeOf(selectorExpr);
+      const DatatypeConstructor& c = dt[selectorIndex];
+      Expr tester = c.getTester();
+      Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
+      tst = Rewriter::rewrite( tst );
+      Node n_ret;
+      if( tst==NodeManager::currentNM()->mkConst( true ) ){
+        n_ret = sel;
+      }else{
+        if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
+          std::stringstream ss;
+          ss << selector << "_uf";
+          d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
+                                            NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) );
+        }
+        Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
+        if( tst==NodeManager::currentNM()->mkConst( false ) ){
+          n_ret = sk;
+        }else{
+          n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk );
+        }
+      }
+      //n_ret = Rewriter::rewrite( n_ret );
+      Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl;
+      return n_ret;
+    }
+  }
+    break;
+  default:
+    return n;
+    break;
+  }
+  Unreachable();
+}
+
 void TheoryDatatypes::presolve() {
   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 }
@@ -332,7 +388,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     }
     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
   } else if(in.getKind() == kind::RECORD_SELECT) {
     TypeNode t = in[0].getType();
     if(t.hasAttribute(expr::DatatypeRecordAttr())) {
@@ -340,7 +396,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     }
     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
   }
 
   TypeNode t = in.getType();
@@ -361,6 +417,19 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
         NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
       }
     }
+
+    if( in.getKind()==EQUAL ){
+      Node nn;
+      std::vector< Node > rew;
+      if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
+        nn = NodeManager::currentNM()->mkConst(false);
+      }else{
+        nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) :
+                  ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+      }
+      return nn;
+    }
+
     // nothing to do
     return in;
   }
@@ -404,7 +473,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
         b << in[1];
         Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
       } else {
-        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]);
+        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]);
         Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
       }
     }
@@ -414,6 +483,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
 
   Assert(!n.isNull());
 
+
   Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
 
   return n;
@@ -452,21 +522,37 @@ bool TheoryDatatypes::propagate(TNode literal){
   return ok;
 }
 
+void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) {
+  for( unsigned i=0; i<tassumptions.size(); i++ ){
+    if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
+      assumptions.push_back( tassumptions[i] );
+    }
+  }
+}
+
+void TheoryDatatypes::explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ) {
+  if( a!=b ){
+    std::vector<TNode> tassumptions;
+    d_equalityEngine.explainEquality(a, b, polarity, tassumptions);
+    addAssumptions( assumptions, tassumptions );
+  }
+}
+
+void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ) {
+  std::vector<TNode> tassumptions;
+  d_equalityEngine.explainPredicate(p, polarity, tassumptions);
+  addAssumptions( assumptions, tassumptions );
+}
+
 /** explain */
 void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
   Debug("datatypes-explain") << "Explain " << literal << std::endl;
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
-  std::vector<TNode> tassumptions;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
+    explainEquality( atom[0], atom[1], polarity, assumptions );
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
-  }
-  for( unsigned i=0; i<tassumptions.size(); i++ ){
-    if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
-      assumptions.push_back( tassumptions[i] );
-    }
+    explainPredicate( atom, polarity, assumptions );
   }
 }
 
@@ -544,7 +630,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
                 Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
                 d_pending.push_back( eq );
                 d_pending_exp[ eq ] = unifEq;
-                Trace("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl;
+                Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
                 d_infer.push_back( eq );
                 d_infer_exp.push_back( unifEq );
               }
@@ -696,7 +782,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
         //conflict because equivalence class contains a constructor
         std::vector< TNode > assumptions;
         explain( t, assumptions );
-        explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions );
+        explainEquality( eqc->d_constructor.get(), tt[0], true, assumptions );
         d_conflictNode = mkAnd( assumptions );
         Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
         d_out->conflict( d_conflictNode );
@@ -767,7 +853,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
           Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
           d_pending.push_back( t_concl );
           d_pending_exp[ t_concl ] = t_concl_exp;
-          Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl;
+          Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
           d_infer.push_back( t_concl );
           d_infer_exp.push_back( t_concl_exp );
           return;
@@ -781,7 +867,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
     std::vector< TNode > assumptions;
     explain( j, assumptions );
     explain( t, assumptions );
-    explain( jt[0].eqNode( tt[0] ), assumptions );
+    explainEquality( jt[0], tt[0], true, assumptions );
     d_conflictNode = mkAnd( assumptions );
     Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
     d_out->conflict( d_conflictNode );
@@ -825,7 +911,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
           Node n = *i;
           std::vector< TNode > assumptions;
           explain( *i, assumptions );
-          explain( c.eqNode( (*i)[0][0] ), assumptions );
+          explainEquality( c, (*i)[0][0], true, assumptions );
           d_conflictNode = mkAnd( assumptions );
           Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
           d_out->conflict( d_conflictNode );
@@ -848,7 +934,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
-  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c );
+  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
   Node rr = Rewriter::rewrite( r );
   //if( r!=rr ){
     //Node eq_exp = NodeManager::currentNM()->mkConst(true);
@@ -860,7 +946,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
 
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = eq_exp;
-    Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl;
+    Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl;
     d_infer.push_back( eq );
     d_infer_exp.push_back( eq_exp );
   }
@@ -881,7 +967,49 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
 }
 
 void TheoryDatatypes::computeCareGraph(){
-  Theory::computeCareGraph();
+  Trace("dt-cg") << "Compute graph for dt..." << std::endl;
+  vector< pair<TNode, TNode> > currentPairs;
+  for( unsigned r=0; r<2; r++ ){
+    unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
+    for( unsigned i=0; i<functionTerms; i++ ){
+      TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i];
+      for( unsigned j=i+1; j<functionTerms; j++ ){
+        TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
+        if( f1.getOperator()==f2.getOperator() && !areEqual( f1, f2 ) ){
+          Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
+          bool somePairIsDisequal = false;
+          currentPairs.clear();
+          for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
+            TNode x = f1[k];
+            TNode y = f2[k];
+            if( areDisequal(x, y) ){
+              somePairIsDisequal = true;
+              break;
+            }else if( !areEqual( x, y ) ){
+              Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
+              //check if they are definately disequal
+              
+              if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
+                TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
+                TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
+                Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
+                //EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
+                //if( eqStatus!=EQUALITY_UNKNOWN ){
+                currentPairs.push_back(make_pair(x_shared, y_shared));
+              }
+            }
+          } 
+          if (!somePairIsDisequal) {
+            for (unsigned c = 0; c < currentPairs.size(); ++ c) {
+              Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
+              addCarePair(currentPairs[c].first, currentPairs[c].second);
+            }
+          }
+        }
+      }
+    }
+  }
+  Trace("dt-cg") << "Done Compute graph for dt." << std::endl;
 }
 
 void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
@@ -889,14 +1017,48 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
   Trace("dt-model") << std::endl;
+
+  /*
+  bool eq_merged = false;
+  std::vector< Node > all_eqc;
+  eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs1_i.isFinished() ){
+    Node eqc = (*eqcs1_i);
+    all_eqc.push_back( eqc );
+    ++eqcs1_i;
+  }
+  //check if equivalence classes have merged
+  for( unsigned i=0; i<all_eqc.size(); i++ ){
+    for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
+      if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
+        Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
+        eq_merged = true;
+      }
+    }
+  }
+  Assert( !eq_merged );
+  */
+
+  //combine the equality engine
   m->assertEqualityEngine( &d_equalityEngine );
-/*
-  std::vector< TypeEnumerator > vec;
-  std::map< TypeNode, int > tes;
+
+  /*
+  //check again if equivalence classes have merged
+  for( unsigned i=0; i<all_eqc.size(); i++ ){
+    for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
+      if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
+        Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
+        eq_merged = true;
+      }
+    }
+  }
+  Assert( !eq_merged );
   */
+
   //get all constructors
   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
   std::vector< Node > cons;
+  std::vector< Node > nodes;
   while( !eqccs_i.isFinished() ){
     Node eqc = (*eqccs_i);
     //for all equivalence classes that are datatypes
@@ -904,28 +1066,14 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
       EqcInfo* ei = getOrMakeEqcInfo( eqc );
       if( !ei->d_constructor.get().isNull() ){
         cons.push_back( ei->d_constructor.get() );
-      }
-    }
-    ++eqccs_i;
-  }
-
-  //must choose proper representatives
-  std::vector< Node > nodes;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    //for all equivalence classes that are datatypes
-    if( DatatypesRewriter::isTermDatatype( eqc ) ){
-      EqcInfo* ei = getOrMakeEqcInfo( eqc );
-      if( !ei->d_constructor.get().isNull() ){
-        //specify that we should use the constructor as the representative
-        //m->assertRepresentative( ei->d_constructor.get() );
       }else{
         nodes.push_back( eqc );
       }
     }
-    ++eqcs_i;
+    ++eqccs_i;
   }
+ 
+  unsigned orig_size = nodes.size();
   unsigned index = 0;
   while( index<nodes.size() ){
     Node eqc = nodes[index];
@@ -942,21 +1090,24 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         neqc = *te;
         Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
         ++te;
-        for( unsigned i=0; i<cons.size(); i++ ){
-          //check if it is modulo equality the same
-          if( cons[i].getOperator()==neqc.getOperator() ){
-            bool diff = false;
-            for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
-              if( !m->areEqual( cons[i][j], neqc[j] ) ){
-                diff = true;
+        //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh
+        if( eqc.getType().getCardinality().isInfinite() || index<orig_size ){
+          for( unsigned i=0; i<cons.size(); i++ ){
+            //check if it is modulo equality the same
+            if( cons[i].getOperator()==neqc.getOperator() ){
+              bool diff = false;
+              for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+                if( !m->areEqual( cons[i][j], neqc[j] ) ){
+                  diff = true;
+                  break;
+                }
+              }
+              if( !diff ){
+                Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
+                success = false;
                 break;
               }
             }
-            if( !diff ){
-              Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
-              success = false;
-              break;
-            }
           }
         }
       }while( !success );
@@ -972,51 +1123,31 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
       }
       Trace("dt-cmi") << std::endl;
       /*
-      if( tes.find( eqc.getType() )==tes.end() ){
-        tes[eqc.getType()]=vec.size();
-        vec.push_back( TypeEnumerator( eqc.getType() ) );
-      }
-      bool success;
-      Node n;
-      do {
-        success = true;
-        Assert( !vec[tes[eqc.getType()]].isFinished() );
-        n = *vec[tes[eqc.getType()]];
-        ++vec[tes[eqc.getType()]];
-        Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl;
-        //check if it is consistent with labels
-        size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
-        if( constructorIndex<pcons.size() && pcons[constructorIndex] ){
-          for( unsigned i=0; i<cons.size(); i++ ){
-            //check if it is modulo equality the same
-            if( cons[i].getOperator()==n.getOperator() ){
-              bool diff = false;
-              for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
-                if( !m->areEqual( cons[i][j], n[j] ) ){
-                  diff = true;
-                  break;
-                }
-              }
-              if( !diff ){
-                Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
-                success = false;
-                break;
-              }
-            }
-          }
-        }else{
-          Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
-          success = false;
+      std::map< int, std::map< int, bool > > sels;
+      Trace("dt-cmi") << "Existing selectors : ";
+      NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
+      if( sel_i != d_selector_apps.end() ){
+        NodeList* sel = (*sel_i).second;
+        for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
+          Expr selectorExpr = (*j).getOperator().toExpr();
+          unsigned cindex = Datatype::cindexOf( selectorExpr );
+          unsigned index = Datatype::indexOf( selectorExpr );
+          sels[cindex][index] = true;
+          Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") ";
         }
-      }while( !success );
+      }
+      Trace("dt-cmi") << std::endl;
       */
+
       const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
       for( unsigned r=0; r<2; r++ ){
         if( neqc.isNull() ){
           for( unsigned i=0; i<pcons.size(); i++ ){
+            //must try the infinite ones first
             if( pcons[i] && (r==1)==dt[ i ].isFinite() ){
               neqc = getInstantiateCons( eqc, dt, i, false, false );
               for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
+                //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
                 if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
                   nodes.push_back( neqc[j] );
                 }
@@ -1030,6 +1161,24 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     Assert( !neqc.isNull() );
     Trace("dt-cmi") << "Assign : " << neqc << std::endl;
     m->assertEquality( eqc, neqc, true );
+    /*
+    for( unsigned kk=0; kk<all_eqc.size(); kk++ ){
+      for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){
+        if( m->areEqual( all_eqc[kk], all_eqc[ll] ) ){
+          Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl;
+          Node r = m->getRepresentative( all_eqc[kk] );
+          Trace("dt-cmi") << "  { ";
+          eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine );
+          while( !eqc_i.isFinished() ){
+            Trace("dt-cmi") << (*eqc_i) << " ";
+            ++eqc_i;
+          }
+          Trace("dt-cmi") << "} " << std::endl;
+        }
+        Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) );
+      }
+    }
+    */
     //m->assertRepresentative( neqc );
     cons.push_back( neqc );
     ++index;
@@ -1045,6 +1194,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
       collectTerms( n[i] );
     }
     if( n.getKind() == APPLY_CONSTRUCTOR ){
+      d_consTerms.push_back( n );
       /*
       //we must take into account subterm relation when checking for cycles
       for( int i=0; i<(int)n.getNumChildren(); i++ ) {
@@ -1059,7 +1209,8 @@ void TheoryDatatypes::collectTerms( Node n ) {
         //eqc->d_selectors = true;
       }
       */
-    }else if( n.getKind() == APPLY_SELECTOR ){
+    }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){
+      d_selTerms.push_back( n );
       //we must also record which selectors exist
       Debug("datatypes") << "  Found selector " << n << endl;
       if (n.getType().isBoolean()) {
@@ -1084,57 +1235,29 @@ void TheoryDatatypes::processNewTerm( Node n ){
     Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
-    Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl;
+    Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
     d_infer.push_back( eq );
   }
 }
 
 Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){
-  //if( !d_inst_map[n][index].isNull() ){
-  //  return d_inst_map[n][index];
-  //}else{
+  std::map< int, Node >::iterator it = d_inst_map[n].find( index );
+  if( it!=d_inst_map[n].end() ){
+    return it->second;
+  }else{
     //add constructor to equivalence class
-    Type tspec;
-    if( dt.isParametric() ){
-      tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
-    }
-    std::vector< Node > children;
-    children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
-    for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
-      Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n );
-      if( mkVar ){
-        TypeNode tn = nc.getType();
-        if( dt.isParametric() ){
-          tn = TypeNode::fromType( tspec )[i];
-        }
-        nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created during model gen" );
-      }
-      children.push_back( nc );
-      if( isActive ){
-        processNewTerm( nc );
-      }
-    }
-    Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+    Node n_ic = DatatypesRewriter::getInstCons( n, dt, index, mkVar );
     if( isActive ){
+      for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){
+        processNewTerm( n_ic[i] );
+      }
       collectTerms( n_ic );
     }
-    //add type ascription for ambiguous constructor types
-    if(!n_ic.getType().isComparableTo(n.getType())) {
-      Assert( dt.isParametric() );
-      Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
-      Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
-      Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
-      Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl;
-      children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                     NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] );
-      n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-      Assert( n_ic.getType()==n.getType() );
-    }
     n_ic = Rewriter::rewrite( n_ic );
     Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
-    //d_inst_map[n][index] = n_ic;
+    d_inst_map[n][index] = n_ic;
     return n_ic;
-  //}
+  }
 }
 
 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
@@ -1155,14 +1278,14 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment()
     //instantiate this equivalence class
     eqc->d_inst = true;
-    Node tt_cons = getInstantiateCons( tt, dt, index );
+    Node tt_cons = getInstantiateCons( tt, dt, index, false, true );
     Node eq;
     if( tt!=tt_cons ){
       eq = tt.eqNode( tt_cons );
       Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
       d_pending.push_back( eq );
       d_pending_exp[ eq ] = exp;
-      Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl;
+      Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl;
       //eqc->d_inst.set( eq );
       d_infer.push_back( eq );
       d_infer_exp.push_back( exp );
@@ -1176,33 +1299,201 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
 
 void TheoryDatatypes::checkCycles() {
   Debug("datatypes-cycle-check") << "Check cycles" << std::endl;
+  std::vector< Node > cod_eqc;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
     if( DatatypesRewriter::isTermDatatype( eqc ) ) {
-      map< Node, bool > visited;
-      std::vector< TNode > expl;
-      Node cn = searchForCycle( eqc, eqc, visited, expl );
-      //if we discovered a different cycle while searching this one
-      if( !cn.isNull() && cn!=eqc ){
-        visited.clear();
-        expl.clear();
-        Node prev = cn;
-        cn = searchForCycle( cn, cn, visited, expl );
-        Assert( prev==cn );
-      }
+      const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
+      if( !dt.isCodatatype() ){
+        //do cycle checks
+        map< Node, bool > visited;
+        std::vector< TNode > expl;
+        Node cn = searchForCycle( eqc, eqc, visited, expl );
+        //if we discovered a different cycle while searching this one
+        if( !cn.isNull() && cn!=eqc ){
+          visited.clear();
+          expl.clear();
+          Node prev = cn;
+          cn = searchForCycle( cn, cn, visited, expl );
+          Assert( prev==cn );
+        }
 
-      if( !cn.isNull() ) {
-        Assert( expl.size()>0 );
-        d_conflictNode = mkAnd( expl );
-        Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
-        d_out->conflict( d_conflictNode );
-        d_conflict = true;
-        return;
+        if( !cn.isNull() ) {
+          Assert( expl.size()>0 );
+          d_conflictNode = mkAnd( expl );
+          Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
+          d_out->conflict( d_conflictNode );
+          d_conflict = true;
+          return;
+        }
+      }else{
+        //indexing
+        cod_eqc.push_back( eqc );
       }
     }
     ++eqcs_i;
   }
+  //process codatatypes
+  if( cod_eqc.size()>1 ){
+    std::vector< std::vector< Node > > part_out;
+    std::vector< TNode > exp;
+    std::map< Node, Node > cn;
+    std::map< Node, std::map< Node, int > > dni;
+    for( unsigned i=0; i<cod_eqc.size(); i++ ){
+      cn[cod_eqc[i]] = cod_eqc[i];
+    }
+    separateBisimilar( cod_eqc, part_out, exp, cn, dni, 0, false );
+    if( !part_out.empty() ){
+      for( unsigned i=0; i<part_out.size(); i++ ){
+        std::vector< Node > part;
+        part.push_back( part_out[i][0] );
+        for( unsigned j=1; j<part_out[i].size(); j++ ){
+          Trace("dt-cod") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl;
+          part.push_back( part_out[i][j] );
+          std::vector< std::vector< Node > > tpart_out;
+          exp.clear();
+          cn.clear();
+          cn[part_out[i][0]] = part_out[i][0];
+          cn[part_out[i][j]] = part_out[i][j];
+          dni.clear();
+          separateBisimilar( part, tpart_out, exp, cn, dni, 0, true );
+          Assert( tpart_out.size()==1 && tpart_out[0].size()==2 );
+          part.pop_back();
+          //merge based on explanation
+          Trace("dt-cod") << "  exp is : ";
+          for( unsigned k=0; k<exp.size(); k++ ){
+            Trace("dt-cod") << exp[k] << " ";
+          }
+          Trace("dt-cod") << std::endl;
+          Node eq = part_out[i][0].eqNode( part_out[i][j] );
+          Node eqExp = mkAnd( exp );
+          d_pending.push_back( eq );
+          d_pending_exp[ eq ] = eqExp;
+          Trace("datatypes-infer") << "DtInfer : cod-bisimilar : " << eq << " by " << eqExp << std::endl;
+          d_infer.push_back( eq );
+          d_infer_exp.push_back( eqExp );
+        }
+      }
+    }
+  }
+}
+
+//everything is in terms of representatives
+void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
+                                         std::vector< TNode >& exp,
+                                         std::map< Node, Node >& cn,
+                                         std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){
+  if( !mkExp ){
+    Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl;
+    for( unsigned i=0; i<part.size(); i++ ){
+      Trace("dt-cod-debug") << "   " << part[i] << ", current = " << cn[part[i]] << std::endl;
+    }
+  }
+  Assert( part.size()>1 );
+  std::map< Node, std::vector< Node > > new_part;
+  std::map< Node, std::vector< Node > > new_part_c;
+  std::map< int, std::vector< Node > > new_part_rec;
+
+  std::map< Node, Node > cn_cons;
+  for( unsigned j=0; j<part.size(); j++ ){
+    Node c = cn[part[j]];
+    std::map< Node, int >::iterator it_rec = dni[part[j]].find( c );
+    if( it_rec!=dni[part[j]].end() ){
+      //looped
+      if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
+      new_part_rec[ it_rec->second ].push_back( part[j] );
+    }else{
+      if( DatatypesRewriter::isTermDatatype( c ) ){
+        bool foundCons = false;
+        EqcInfo* eqc = getOrMakeEqcInfo( c, false );
+        if( eqc ){
+          Node ncons = eqc->d_constructor.get();
+          if( !ncons.isNull() ) {
+            foundCons = true;
+            Node cc = ncons.getOperator();
+            cn_cons[part[j]] = ncons;
+            if( mkExp ){
+              explainEquality( c, ncons, true, exp );
+            }
+            new_part[cc].push_back( part[j] );
+            if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is datatype " << ncons << "." << std::endl; }
+          }
+        }
+        if( !foundCons ){
+          new_part_c[c].push_back( part[j] );
+          if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is unspecified datatype." << std::endl; }
+        }
+      }else{
+        //add equivalences
+        if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is term " << c << "." << std::endl; }
+        new_part_c[c].push_back( part[j] );
+      }
+    }
+  }
+  //direct add for constants
+  for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){
+    if( it->second.size()>1 ){
+      std::vector< Node > vec;
+      vec.insert( vec.begin(), it->second.begin(), it->second.end() );
+      part_out.push_back( vec );
+    }
+  }
+  //direct add for recursive
+  for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){
+    if( it->second.size()>1 ){
+      std::vector< Node > vec;
+      vec.insert( vec.begin(), it->second.begin(), it->second.end() );
+      part_out.push_back( vec );
+    }else{
+      //add back : could match a datatype?
+    }
+  }
+  //recurse for the datatypes
+  for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){
+    if( it->second.size()>1 ){
+      //set dni to check for loops
+      std::map< Node, Node > dni_rem;
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node n = it->second[i];
+        dni[n][cn[n]] = dniLvl;
+        dni_rem[n] = cn[n];
+      }
+
+      //we will split based on the arguments of the datatype
+      std::vector< std::vector< Node > > split_new_part;
+      split_new_part.push_back( it->second );
+
+      unsigned nChildren = cn_cons[it->second[0]].getNumChildren();
+      //for each child of constructor
+      unsigned cindex = 0;
+      while( cindex<nChildren && !split_new_part.empty() ){
+        if( !mkExp ){ Trace("dt-cod-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; }
+        std::vector< std::vector< Node > > next_split_new_part;
+        for( unsigned j=0; j<split_new_part.size(); j++ ){
+          //set current node
+          for( unsigned k=0; k<split_new_part[j].size(); k++ ){
+            Node n = split_new_part[j][k];
+            cn[n] = getRepresentative( cn_cons[n][cindex] );
+            if( mkExp ){
+              explainEquality( cn[n], cn_cons[n][cindex], true, exp );
+            }
+          }
+          std::vector< std::vector< Node > > c_part_out;
+          separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp );
+          next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() );
+        }
+        split_new_part.clear();
+        split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() );
+        cindex++;
+      }
+      part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() );
+
+      for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){
+        dni[it2->first].erase( it2->second );
+      }
+    }
+  }
 }
 
 //postcondition: if cycle detected, explanation is why n is a subterm of on
@@ -1215,8 +1506,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on,
   if( !firstTime ){
     nn = getRepresentative( n );
     if( nn==on ){
-      Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn );
-      explain( lit, explanation );
+      explainEquality( n, nn, true, explanation );
       return on;
     }
   }else{
@@ -1236,8 +1526,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on,
             //}
             //add explanation for why the constructor is connected
             if( n != ncons ) {
-              Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons );
-              explain( lit, explanation );
+              explainEquality( n, ncons, true, explanation );
             }
             return on;
           }else if( !cn.isNull() ){
@@ -1249,7 +1538,13 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on,
     visited.erase( nn );
     return Node::null();
   }else{
-    return nn;
+    if( DatatypesRewriter::isTermDatatype( nn ) ) {
+      const Datatype& dt = ((DatatypeType)(nn.getType()).toType()).getDatatype();
+      if( !dt.isCodatatype() ){
+        return nn;
+      }
+    }
+    return Node::null();
   }
 }
 
@@ -1303,11 +1598,11 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   return false;
 }
 
-bool TheoryDatatypes::hasTerm( Node a ){
+bool TheoryDatatypes::hasTerm( TNode a ){
   return d_equalityEngine.hasTerm( a );
 }
 
-bool TheoryDatatypes::areEqual( Node a, Node b ){
+bool TheoryDatatypes::areEqual( TNode a, TNode b ){
   if( a==b ){
     return true;
   }else if( hasTerm( a ) && hasTerm( b ) ){
@@ -1317,7 +1612,7 @@ bool TheoryDatatypes::areEqual( Node a, Node b ){
   }
 }
 
-bool TheoryDatatypes::areDisequal( Node a, Node b ){
+bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
   if( a==b ){
     return false;
   }else if( hasTerm( a ) && hasTerm( b ) ){
@@ -1327,7 +1622,7 @@ bool TheoryDatatypes::areDisequal( Node a, Node b ){
   }
 }
 
-Node TheoryDatatypes::getRepresentative( Node a ){
+Node TheoryDatatypes::getRepresentative( TNode a ){
   if( hasTerm( a ) ){
     return d_equalityEngine.getRepresentative( a );
   }else{
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 3a29433f8..eb86c3f76 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -166,6 +166,12 @@ private:
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
   std::vector< Node > d_pending_merge;
+  /** expand definition skolem functions */
+  std::map< Node, Node > d_exp_def_skolem;
+  /** All the constructor terms that the theory has seen */
+  context::CDList<TNode> d_consTerms;
+  /** All the selector terms that the theory has seen */
+  context::CDList<TNode> d_selTerms;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -193,6 +199,9 @@ public:
   /** propagate */
   bool propagate(TNode literal);
   /** explain */
+  void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions );
+  void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
+  void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
   void explain( TNode literal, std::vector<TNode>& assumptions );
   Node explain( TNode literal );
   /** Conflict when merging two constants */
@@ -208,6 +217,7 @@ public:
 
   void check(Effort e);
   void preRegisterTerm(TNode n);
+  Node expandDefinition(LogicRequest &logicRequest, Node n);
   Node ppRewrite(TNode n);
   void presolve();
   void addSharedTerm(TNode t);
@@ -233,10 +243,15 @@ private:
   Node searchForCycle( Node n, Node on,
                        std::map< Node, bool >& visited,
                        std::vector< TNode >& explanation, bool firstTime = true );
+  /** for checking whether two codatatype terms must be equal */
+  void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
+                          std::vector< TNode >& exp,
+                          std::map< Node, Node >& cn,
+                          std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp );
   /** collect terms */
   void collectTerms( Node n );
   /** get instantiate cons */
-  Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true );
+  Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive );
   /** process new term that was created internally */
   void processNewTerm( Node n );
   /** check instantiate */
@@ -250,10 +265,10 @@ private:
   bool mustCommunicateFact( Node n, Node exp );
 private:
   //equality queries
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  Node getRepresentative( Node a );
+  bool hasTerm( TNode a );
+  bool areEqual( TNode a, TNode b );
+  bool areDisequal( TNode a, TNode b );
+  Node getRepresentative( TNode a );
 public:
   /** get equality engine */
   eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 527d110e0..d08b511dd 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule {
 struct DatatypeSelectorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate) {
-    Assert(n.getKind() == kind::APPLY_SELECTOR);
+    Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL );
     TypeNode selType = n.getOperator().getType(check);
     Type t = selType[0].toType();
     Assert( t.isDatatype() );
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);
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
 
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index d815e0ee8..098a7819a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
   Node curr;
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
-    Node v = getRepresentative( d_models[op]->d_value[i] );
+    Node v = d_models[op]->d_value[i];
+    if( !hasTerm( v ) ){
+      //can happen when the model basis term does not exist in ground assignment
+      TypeNode tn = v.getType();
+      if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
+        //see full_model_check.cpp line 366
+        v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
+      }else{
+        Assert( false );
+      }
+    }
+    v = getRepresentative( v );
     if( curr.isNull() ){
       curr = v;
     }else{
@@ -656,6 +667,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       Node cond = d_models[op]->d_cond[i];
       std::vector< Node > children;
       for( unsigned j=0; j<cond.getNumChildren(); j++) {
+        TypeNode tn = vars[j].getType();
         if (isInterval(cond[j])){
           if( !isStar(cond[j][0]) ){
             children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) );
@@ -663,7 +675,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
           if( !isStar(cond[j][1]) ){
             children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
           }
-        }else if (!isStar(cond[j])){
+        }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground eqc of this type
+                   d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
           Node c = getUsedRepresentative( cond[j] );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }
@@ -673,6 +686,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
     }
   }
+  Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
   curr = Rewriter::rewrite( curr );
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 3b6c8e492..0f3e53827 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
 void FullModelChecker::doNegate( Def & dc ) {
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
     if (!dc.d_value[i].isNull()) {
-      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;
+      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] );
     }
   }
 }
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index 10185914e..8bd97a8a7 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -79,8 +79,8 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m
 
 std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
   switch(mode) {
-  case theory::quantifiers::MBQI_DEFAULT:
-    out << "MBQI_DEFAULT";
+  case theory::quantifiers::MBQI_GEN_EVAL:
+    out << "MBQI_GEN_EVAL";
     break;
   case theory::quantifiers::MBQI_NONE:
     out << "MBQI_NONE";
@@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode)
   case theory::quantifiers::MBQI_INTERVAL:
     out << "MBQI_INTERVAL";
     break;
+  case theory::quantifiers::MBQI_TRUST:
+    out << "MBQI_TRUST";
+    break;
   default:
     out << "MbqiMode!UNKNOWN";
   }
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 89e10b175..80534c8b0 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -58,13 +58,13 @@ typedef enum {
 } AxiomInstMode;
 
 typedef enum {
-  /** default, mbqi from CADE 24 paper */
-  MBQI_DEFAULT,
+  /** mbqi from CADE 24 paper */
+  MBQI_GEN_EVAL,
   /** no mbqi */
   MBQI_NONE,
   /** implementation that mimics inst-gen */
   MBQI_INST_GEN,
-  /** mbqi from Section 5.4.2 of AJR thesis */
+  /** default, mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
   /** mbqi with integer intervals */
   MBQI_FMC_INTERVAL,
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 0865f2c0b..e733764f0 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -67,11 +67,13 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false
 
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
+option instMaxLevel --inst-max-level=N int :default -1
+ maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
  
-option fullSaturateQuant --full-saturate-quant bool :default true
+option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
@@ -95,7 +97,7 @@ option internalReps /--disable-quant-internal-reps bool :default true
 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
  use finite model finding heuristic for quantifier instantiation
 
-option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
+option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
 option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for mbqi
@@ -112,7 +114,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
-option fmfBoundInt --fmf-bound-int bool :default false :read-write
+option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
 
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e9c754d4a..b7e624a66 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -82,8 +82,8 @@ static const std::string mbqiModeHelp = "\
 Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
 \n\
 default \n\
-+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper.\n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
+  Modulo Theories.\n\
 \n\
 none \n\
 + Disable model-based quantifier instantiation.\n\
@@ -91,12 +91,12 @@ none \n\
 instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
-fmc \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
-  Modulo Theories.\n\
+gen-ev \n\
++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper based on generalizing evaluations.\n\
 \n\
 fmc-interval \n\
-+ Same as fmc, but with intervals for models of integer functions.\n\
++ Same as default, but with intervals for models of integer functions.\n\
 \n\
 interval \n\
 + Use algorithm that abstracts domain elements as intervals. \n\
@@ -131,9 +131,6 @@ conflict \n\
 partial \n\
 + Apply QCF algorithm to instantiate heuristically as well. \n\
 \n\
-partial \n\
-+ Apply QCF to instantiate heuristically as well. \n\
-\n\
 mc \n\
 + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
 \n\
@@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar
 }
 
 inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default") {
-    return MBQI_DEFAULT;
-  } else if(optarg ==  "none") {
+  if(optarg == "gen-ev") {
+    return MBQI_GEN_EVAL;
+  } else if(optarg == "none") {
     return MBQI_NONE;
-  } else if(optarg ==  "instgen") {
+  } else if(optarg == "instgen") {
     return MBQI_INST_GEN;
-  } else if(optarg ==  "fmc") {
+  } else if(optarg == "default" || optarg ==  "fmc") {
     return MBQI_FMC;
-  } else if(optarg ==  "fmc-interval") {
+  } else if(optarg == "fmc-interval") {
     return MBQI_FMC_INTERVAL;
-  } else if(optarg ==  "interval") {
+  } else if(optarg == "interval") {
     return MBQI_INTERVAL;
-  } else if(optarg ==  "trust") {
+  } else if(optarg == "trust") {
     return MBQI_TRUST;
-  } else if(optarg ==  "help") {
+  } else if(optarg == "help") {
     puts(mbqiModeHelp.c_str());
     exit(1);
   } else {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c0b318f23..e27d438be 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 

 bool MatchGen::isHandledUfTerm( TNode n ) {

   return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||

-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;

+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;

 }

 

 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cf183dd18..3168d21a0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) {
     }
     d_par_op_map[op][tn1][tn2] = n;
     return n;
-  }else if( n.getKind()==APPLY_UF ){
+  }else if( inst::Trigger::isAtomicTrigger( n ) ){
     return n.getOperator();
   }else{
     return Node::null();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 6912c9e89..3de12b9c9 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 
 bool Trigger::isAtomicTrigger( Node n ){
   return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE ||
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;
+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
 }
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index eaf5e8228..63697f5e7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -319,7 +319,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
       Trace("inst") << "   " << terms[i];
       Trace("inst") << std::endl;
     }
-    //uint64_t maxInstLevel = 0;
     if( options::cbqi() ){
       for( int i=0; i<(int)terms.size(); i++ ){
         if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
@@ -328,22 +327,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
             Debug("inst") << "   " << terms[i] << std::endl;
           }
           Unreachable("Bad instantiation");
-        }else{
-          Trace("inst") << "   " << terms[i];
-          //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
-          Trace("inst") << std::endl;
-          //if( terms[i].hasAttribute(InstLevelAttribute()) ){
-            //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-            //  maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
-            //}
-          //}else{
-            //setInstantiationLevelAttr( terms[i], 0 );
-          //}
         }
       }
     }
+    if( options::instMaxLevel()!=-1 ){
+      uint64_t maxInstLevel = 0;
+      for( int i=0; i<(int)terms.size(); i++ ){
+        if( terms[i].hasAttribute(InstLevelAttribute()) ){
+          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+          }
+        }
+      }
+      setInstantiationLevelAttr( body, maxInstLevel+1 );
+    }
     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
-    //setInstantiationLevelAttr( body, maxInstLevel+1 );
     ++(d_statistics.d_instantiations);
     return true;
   }else{
@@ -504,6 +502,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   }
   Trace("inst-add-debug") << std::endl;
 
+  if( options::instMaxLevel()!=-1 ){
+    for( unsigned i=0; i<terms.size(); i++ ){
+      if( terms[i].hasAttribute(InstLevelAttribute()) &&
+          (int)terms[i].getAttribute(InstLevelAttribute())>options::instMaxLevel() ){
+        Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute());
+        Trace("inst-add-debug") << ", which is more than maximum allowed level " << options::instMaxLevel() << std::endl;
+        return false;
+      }
+    }
+  }
+
   //check for duplication
   ///*
   bool alreadyExists = false;
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 8c07b679d..16bb7e694 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -41,10 +41,6 @@ RegExpOpr::RegExpOpr() {
 	d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );

 	std::vector< Node > nvec;

     d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );

-	// All Charactors = all printable ones 32-126

-	//d_char_start = 'a';//' ';

-	//d_char_end = 'c';//'~';

-	//d_sigma = mkAllExceptOne( '\0' );

 	d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );

 	d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );

 	d_card = 256;

@@ -896,15 +892,13 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
 			}

 			case kind::REGEXP_CONCAT: {

 				//TODO: rewrite empty

+				Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);

 				Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());

 				Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);

 				Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),

 							NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );

-				Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());

-				Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());

-				Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);

-				Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));

-				Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));

+				Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1));

+				Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)));

 				Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();

 				if(r[0].getKind() == kind::STRING_TO_REGEXP) {

 					s1r1 = s1.eqNode(r[0][0]).negate();

@@ -928,8 +922,6 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
 				}

 

 				conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);

-				conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);

-				conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);

 				conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);

 				conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);

 				break;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ac5a97167..d44f38bc3 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -65,7 +65,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_curr_cardinality(c, 0)
 {
     // The kinds we are treating as function application in congruence
-    //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
+    d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
     d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
@@ -418,7 +418,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 		break;
 	case kind::STRING_IN_REGEXP:
 		//do not add trigger here
-		//d_equalityEngine.addTriggerPredicate(n);
+		d_equalityEngine.addTriggerPredicate(n);
 		break;
 	case kind::STRING_SUBSTR_TOTAL: {
 		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
@@ -560,7 +560,7 @@ void TheoryStrings::check(Effort e) {
 	//must record string in regular expressions
 	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
 		addMembership(assertion);
-		//d_equalityEngine.assertPredicate(atom, polarity, fact);
+		d_equalityEngine.assertPredicate(atom, polarity, fact);
 	} else if (atom.getKind() == kind::STRING_STRCTN) {
 		if(polarity) {
 			d_str_pos_ctn.push_back( atom );
@@ -1232,18 +1232,37 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 									Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
 									Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
 									antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-									Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-										NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-									//split the string
-									Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
-									Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false );
-									d_pending_req_phase[ eq1 ] = true;
-									conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-									Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
-
-									Node ant = mkExplain( antec );
-									sendLemma( ant, conc, "CST-SPLIT" );
-									++(d_statistics.d_eq_splits);
+									//Opt
+									bool optflag = false;
+									if( normal_forms[nconst_k].size() > nconst_index_k + 1 &&
+										normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+										CVC4::String stra = const_str.getConst<String>();
+										CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
+										CVC4::String fc = strb.substr(0, 1);
+										if( stra.find(fc) == std::string::npos ||
+											(stra.find(strb) == std::string::npos &&
+											 !stra.overlap(strb)) ) {
+											Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" );
+											Node eq = other_str.eqNode( mkConcat(const_str, sk) );
+											Node ant = mkExplain( antec );
+											sendLemma(ant, eq, "CST-EPS");
+											optflag = true;
+										}
+									}
+									if(!optflag){
+										Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+											NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+										//split the string
+										Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
+										Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false );
+										d_pending_req_phase[ eq1 ] = true;
+										conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+										Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+
+										Node ant = mkExplain( antec );
+										sendLemma( ant, conc, "CST-SPLIT" );
+										++(d_statistics.d_eq_splits);
+									}
 									return true;
 								} else {
 									std::vector< Node > antec_new_lits;
@@ -1785,10 +1804,7 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
 }
 
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
-	std::vector< Node > c;
-	c.push_back( n1 );
-	c.push_back( n2 );
-	return mkConcat( c );
+	return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 );
 }
 
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
@@ -2888,6 +2904,11 @@ void TheoryStrings::addMembership(Node assertion) {
 	d_regexp_memberships.push_back( assertion );
 }
 
+Node TheoryStrings::instantiateSymRegExp(Node r) {
+	//TODO:
+	return r;
+}
+
 //// Finite Model Finding
 
 Node TheoryStrings::getNextDecisionRequest() {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 9f99012df..33283d1cf 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -272,8 +272,8 @@ protected:
 	void sendInfer( Node eq_exp, Node eq, const char * c );
 	void sendSplit( Node a, Node b, const char * c, bool preq = true );
 	/** mkConcat **/
-	Node mkConcat( Node n1, Node n2 );
-	Node mkConcat( std::vector< Node >& c );
+	inline Node mkConcat( Node n1, Node n2 );
+	inline Node mkConcat( std::vector< Node >& c );
 	/** mkExplain **/
 	Node mkExplain( std::vector< Node >& a );
 	Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
@@ -323,6 +323,7 @@ private:
 	bool splitRegExp( Node x, Node r, Node ant );
 	bool addMembershipLength(Node atom);
 	void addMembership(Node assertion);
+	Node instantiateSymRegExp(Node r);
 
 
 	// Finite Model Finding
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 405fceb6f..f207bdb8e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc
   d_equalityEngine->addFunctionKind(kind::SELECT);
   // d_equalityEngine->addFunctionKind(kind::STORE);
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_eeContext->push();
 }
@@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t
 
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
-  return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR);
+  return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
 }
 
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9db32f894..57cf9001b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -101,7 +101,12 @@ void TheoryUF::check(Effort level) {
     if (atom.getKind() == kind::EQUAL) {
       d_equalityEngine.assertEquality(atom, polarity, fact);
     } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
-      // do nothing
+      if( d_thss == NULL ){
+        std::stringstream ss;
+        ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl;
+        ss << "Try using a logic containing \"UFC\"." << std::endl;
+        throw Exception( ss.str() );
+      }
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
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..a8f3b404a 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. */
@@ -442,6 +448,7 @@ public:
 private:
   std::string d_name;
   std::vector<Type> d_params;
+  bool d_isCo;
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
@@ -488,13 +495,13 @@ private:
 public:
 
   /** Create a new Datatype of the given name. */
-  inline explicit Datatype(std::string name);
+  inline explicit Datatype(std::string name, bool isCo = false);
 
   /**
    * Create a new Datatype of the given name, with the given
    * parameterization.
    */
-  inline Datatype(std::string name, const std::vector<Type>& params);
+  inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
 
   /**
    * Add a constructor to this Datatype.  Constructor names need not
@@ -520,6 +527,9 @@ public:
   /** Get parameters */
   inline std::vector<Type> getParameters() const;
 
+  /** is this a co-datatype? */
+  inline bool isCodatatype() const;
+
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
@@ -656,18 +666,20 @@ inline std::string DatatypeUnresolvedType::getName() const throw() {
   return d_name;
 }
 
-inline Datatype::Datatype(std::string name) :
+inline Datatype::Datatype(std::string name, bool isCo) :
   d_name(name),
   d_params(),
+  d_isCo(isCo),
   d_constructors(),
   d_resolved(false),
   d_self(),
   d_card(CardinalityUnknown()) {
 }
 
-inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
+inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) :
   d_name(name),
   d_params(params),
+  d_isCo(isCo),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -701,6 +713,10 @@ inline std::vector<Type> Datatype::getParameters() const {
   return d_params;
 }
 
+inline bool Datatype::isCodatatype() const {
+  return d_isCo;
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index b6db624d5..3bc17b050 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -23,6 +23,71 @@ using namespace std;
 

 namespace CVC4 {

 

+void String::toInternal(const std::string &s) {

+  d_str.clear();

+  unsigned i=0;

+  while(i < s.size()) {

+	  if(s[i] == '\\') {

+		  i++;

+		  if(i < s.size()) {

+			  switch(s[i]) {

+				  case 'n':  {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;

+				  case 't':  {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;

+				  case 'v':  {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;

+				  case 'b':  {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;

+				  case 'r':  {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;

+				  case 'f':  {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;

+				  case 'a':  {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;

+				  case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;

+				  case 'x': {

+					  if(i + 2 < s.size()) {

+						if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) &&

+						   (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) {

+							d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );

+							i += 3;

+						} else {

+							throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );

+						}

+					  } else {

+						throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );

+					  }

+				  }

+				  break;

+				  default: {

+					  if(isdigit(s[i])) {

+						  int num = (int)s[i] - (int)'0';

+						  bool flag = num < 4;

+						  if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {

+							  num = num * 8 + (int)s[i+1] - (int)'0';

+							  if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {

+								  num = num * 8 + (int)s[i+2] - (int)'0';

+								  d_str.push_back( convertCharToUnsignedInt((char)num) );

+								  i += 3;

+							  } else {

+								  d_str.push_back( convertCharToUnsignedInt((char)num) );

+								  i += 2;

+							  }

+						  } else {

+							  d_str.push_back( convertCharToUnsignedInt((char)num) );

+							  i++;

+						  }

+					  } else {

+						  d_str.push_back( convertCharToUnsignedInt(s[i]) );

+						  i++;

+					  }

+				  }

+			  }

+		  } else {

+			  throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );

+			  //d_str.push_back( convertCharToUnsignedInt('\\') );

+		  }

+	  } else {

+		  d_str.push_back( convertCharToUnsignedInt(s[i]) );

+		  i++;

+	  }

+  }

+}

+

 void String::getCharSet(std::set<unsigned int> &cset) const {

 	for(std::vector<unsigned int>::const_iterator itr = d_str.begin();

 		itr != d_str.end(); itr++) {

@@ -30,6 +95,21 @@ void String::getCharSet(std::set<unsigned int> &cset) const {
 		}

 }

 

+bool String::overlap(String &y) const {

+	unsigned n = y.size();

+	if(d_str.size() < y.size()) {

+		n = d_str.size();

+	}

+	for(unsigned i=1; i<n; i++) {

+		String s = suffix(i);

+		String p = y.prefix(i);

+		if(s == p) {

+			return true;

+		}

+	}

+	return false;

+}

+

 std::string String::toString() const {

 	std::string str;

 	for(unsigned int i=0; i<d_str.size(); ++i) {

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 8c4a3922d..2bb2b5c4c 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -70,70 +70,7 @@ private:
 	  }
   }
 
-  void toInternal(const std::string &s) {
-	  d_str.clear();
-	  unsigned i=0;
-	  while(i < s.size()) {
-		  if(s[i] == '\\') {
-			  i++;
-			  if(i < s.size()) {
-				  switch(s[i]) {
-					  case 'n':  {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;
-					  case 't':  {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;
-					  case 'v':  {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;
-					  case 'b':  {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;
-					  case 'r':  {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;
-					  case 'f':  {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;
-					  case 'a':  {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;
-					  case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;
-					  case 'x': {
-						  if(i + 2 < s.size()) {
-							if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) &&
-							   (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) {
-								d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
-								i += 3;
-							} else {
-								throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
-							}
-						  } else {
-							throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
-						  }
-					  }
-					  break;
-					  default: {
-						  if(isdigit(s[i])) {
-							  int num = (int)s[i] - (int)'0';
-							  bool flag = num < 4;
-							  if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {
-								  num = num * 8 + (int)s[i+1] - (int)'0';
-								  if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {
-									  num = num * 8 + (int)s[i+2] - (int)'0';
-									  d_str.push_back( convertCharToUnsignedInt((char)num) );
-									  i += 3;
-								  } else {
-									  d_str.push_back( convertCharToUnsignedInt((char)num) );
-									  i += 2;
-								  }
-							  } else {
-								  d_str.push_back( convertCharToUnsignedInt((char)num) );
-								  i++;
-							  }
-						  } else {
-							  d_str.push_back( convertCharToUnsignedInt(s[i]) );
-							  i++;
-						  }
-					  }
-				  }
-			  } else {
-				  throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
-				  //d_str.push_back( convertCharToUnsignedInt('\\') );
-			  }
-		  } else {
-			  d_str.push_back( convertCharToUnsignedInt(s[i]) );
-			  i++;
-		  }
-	  }
-  }
+  void toInternal(const std::string &s);
 
 public:
   String() {}
@@ -316,6 +253,15 @@ public:
     ret_vec.insert( ret_vec.end(), itr, itr + j );
     return String(ret_vec);
   }
+
+  String prefix(unsigned i) const {
+	  return substr(0, i);
+  }
+  String suffix(unsigned i) const {
+	  return substr(d_str.size() - i, i);
+  }
+  bool overlap(String &y) const;
+
   bool isNumber() const {
 	 if(d_str.size() == 0) return false;
 	 for(unsigned int i=0; i<d_str.size(); ++i) {