The Tuesday Afternoon Catch-All Commit (TACAC):

* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)

* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).

* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)

(this commit was certified error- and warning-free by the test-and-commit script.)

14 files changed, 207 insertions, 13 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8b61e92d3..99662cb99 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -960,7 +960,7 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
     d_commandStatus = new CommandFailure(e.what());
   }
   */
-  d_commandStatus = new CommandFailure("unsat cores not supported yet");
+  d_commandStatus = new CommandUnsupported();
 }
 
 void GetUnsatCoreCommand::printResult(std::ostream& out) const throw() {
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5e1ec0221..516930bcd 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -507,7 +507,7 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
 
 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( types.size() >= 2 );
+  Assert( types.size() >= 1 );
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);
@@ -515,6 +515,15 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 }
 
+SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
+  NodeManagerScope nms(d_nodeManager);
+  std::vector<TypeNode> typeNodes;
+  for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
+     typeNodes.push_back(*types[i].d_typeNode);
+  }
+  return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
+}
+
 BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
   NodeManagerScope nms(d_nodeManager);
   return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index e20edfb42..460e3f1dc 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -345,10 +345,17 @@ public:
   /**
    * Make a tuple type with types from
    * <code>types[0..types.size()-1]</code>.  <code>types</code> must
-   * have at least 2 elements.
+   * have at least one element.
    */
   TupleType mkTupleType(const std::vector<Type>& types);
 
+  /**
+   * Make a symbolic expressiontype with types from
+   * <code>types[0..types.size()-1]</code>.  <code>types</code> may
+   * have any number of elements.
+   */
+  SExprType mkSExprType(const std::vector<Type>& types);
+
   /** Make a type representing a bit-vector of the given size. */
   BitVectorType mkBitVectorType(unsigned size) const;
 
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 647c1af8e..4582bfeda 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -302,11 +302,6 @@ function register_metakind {
     exit 1
   fi
 
-  if [ $mk = OPERATOR -a $lb = 0 ]; then
-    echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
-    exit 1
-  fi
-
   metakind_lbchildren="${metakind_lbchildren}
     $lb, /* $k */"
   metakind_ubchildren="${metakind_ubchildren}
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 4a05b174d..8e61415e8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -711,14 +711,24 @@ public:
 
   /**
    * Make a tuple type with types from
-   * <code>types</code>. <code>types</code> must have at least two
-   * elements.
+   * <code>types</code>. <code>types</code> must have at least one
+   * element.
    *
    * @param types a vector of types
    * @returns the tuple type (types[0], ..., types[n])
    */
   inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
 
+  /**
+   * Make a symbolic expression type with types from
+   * <code>types</code>. <code>types</code> may have any number of
+   * elements.
+   *
+   * @param types a vector of types
+   * @returns the symbolic expression type (types[0], ..., types[n])
+   */
+  inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
+
   /** Make the type of bitvectors of size <code>size</code> */
   inline TypeNode mkBitVectorType(unsigned size);
 
@@ -1060,6 +1070,14 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
 }
 
+inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
+  std::vector<TypeNode> typeNodes;
+  for (unsigned i = 0; i < types.size(); ++ i) {
+    typeNodes.push_back(types[i]);
+  }
+  return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
+}
+
 inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
 }
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index b55d33dcf..5a00a538c 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -347,6 +347,19 @@ Type::operator TupleType() const throw(AssertionException) {
   return TupleType(*this);
 }
 
+/** Is this a symbolic expression type? */
+bool Type::isSExpr() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSExpr();
+}
+
+/** Cast to a symbolic expression type */
+Type::operator SExprType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isNull() || isSExpr());
+  return SExprType(*this);
+}
+
 /** Is this an array type? */
 bool Type::isArray() const {
   NodeManagerScope nms(d_nodeManager);
@@ -441,6 +454,18 @@ vector<Type> TupleType::getTypes() const {
   return types;
 }
 
+vector<Type> SExprType::getTypes() const {
+  NodeManagerScope nms(d_nodeManager);
+  vector<Type> types;
+  vector<TypeNode> typeNodes = d_typeNode->getSExprTypes();
+  vector<TypeNode>::iterator it = typeNodes.begin();
+  vector<TypeNode>::iterator it_end = typeNodes.end();
+  for(; it != it_end; ++ it) {
+    types.push_back(makeType(*it));
+  }
+  return types;
+}
+
 string SortType::getName() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->getAttribute(expr::VarNameAttr());
@@ -533,6 +558,11 @@ TupleType::TupleType(const Type& t) throw(AssertionException) :
   Assert(isNull() || isTuple());
 }
 
+SExprType::SExprType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isNull() || isSExpr());
+}
+
 ArrayType::ArrayType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isNull() || isArray());
diff --git a/src/expr/type.h b/src/expr/type.h
index 513a4d60a..caaf256f5 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -57,6 +57,7 @@ class SelectorType;
 class TesterType;
 class FunctionType;
 class TupleType;
+class SExprType;
 class SortType;
 class SortConstructorType;
 class PredicateSubtype;
@@ -319,6 +320,18 @@ public:
   operator TupleType() const throw(AssertionException);
 
   /**
+   * Is this a symbolic expression type?
+   * @return true if the type is a symbolic expression type
+   */
+  bool isSExpr() const;
+
+  /**
+   * Cast this type to a symbolic expression type
+   * @return the SExprType
+   */
+  operator SExprType() const throw(AssertionException);
+
+  /**
    * Is this an array type?
    * @return true if the type is a array type
    */
@@ -514,6 +527,20 @@ public:
 };/* class TupleType */
 
 /**
+ * Class encapsulating a tuple type.
+ */
+class CVC4_PUBLIC SExprType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SExprType(const Type& type = Type()) throw(AssertionException);
+
+  /** Get the constituent types */
+  std::vector<Type> getTypes() const;
+};/* class SExprType */
+
+/**
  * Class encapsulating an array type.
  */
 class CVC4_PUBLIC ArrayType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index e35d55e28..2676fd6b2 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -144,7 +144,6 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
-/** Is this a tuple type? */
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
   vector<TypeNode> types;
@@ -154,6 +153,15 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   return types;
 }
 
+vector<TypeNode> TypeNode::getSExprTypes() const {
+  Assert(isSExpr());
+  vector<TypeNode> types;
+  for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
+    types.push_back((*this)[i]);
+  }
+  return types;
+}
+
 /** Is this an instantiated datatype type */
 bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() == kind::DATATYPE_TYPE) {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index af0734575..a0397e0bd 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -541,6 +541,12 @@ public:
   /** Get the constituent types of a tuple type */
   std::vector<TypeNode> getTupleTypes() const;
 
+  /** Is this a symbolic expression type? */
+  bool isSExpr() const;
+
+  /** Get the constituent types of a symbolic expression type */
+  std::vector<TypeNode> getSExprTypes() const;
+
   /** Is this a bit-vector type */
   bool isBitVector() const;
 
@@ -873,6 +879,12 @@ inline bool TypeNode::isTuple() const {
     ( isPredicateSubtype() && getSubtypeBaseType().isTuple() );
 }
 
+/** Is this a symbolic expression type? */
+inline bool TypeNode::isSExpr() const {
+  return getKind() == kind::SEXPR_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isSExpr() );
+}
+
 /** Is this a sort kind */
 inline bool TypeNode::isSort() const {
   return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 4ac137ef1..20b4c2bc2 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -314,5 +314,16 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   if(opts[options::statistics]) {
     cmdExecutor.flushStatistics(*opts[options::err]);
   }
+
+#ifdef CVC4_DEBUG
+  if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
+    _exit(returnValue);
+  }
+#else /* CVC4_DEBUG */
+  if(opts[options::earlyExit]) {
+    _exit(returnValue);
+  }
+#endif /* CVC4_DEBUG */
+
   return returnValue;
 }
diff --git a/src/main/options b/src/main/options
index 47d8da598..58ea5e544 100644
--- a/src/main/options
+++ b/src/main/options
@@ -19,6 +19,9 @@ option - --show-debug-tags void :handler CVC4::main::showDebugTags :handler-incl
 option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-include "main/options_handlers.h"
  show all available tags for tracing
 
+expert-option earlyExit --early-exit bool :default true
+ do not run destructors at exit; default on except in debug mode
+
 # portfolio options
 option printWinner bool
  enable printing the winning thread (pcvc4 only)
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 4f214ddd1..7d5dd56c9 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -288,7 +288,7 @@ inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) th
 
 inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
   if(value) {
-    throw OptionException("CVC4 does not yet have support for unsatisfiable cores");
+    throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores");
   }
 }
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 8eff22ed4..86efac2f0 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -290,6 +290,7 @@ variable VARIABLE "variable"
 variable BOUND_VARIABLE "bound variable"
 variable SKOLEM "skolem var"
 operator TUPLE 1: "a tuple"
+operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
 
@@ -313,6 +314,14 @@ well-founded TUPLE_TYPE \
     "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
     "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
+operator SEXPR_TYPE 0: "symbolic expression type"
+cardinality SEXPR_TYPE \
+    "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
+well-founded SEXPR_TYPE \
+    "::CVC4::theory::builtin::SExprProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
 
 # These will eventually move to a theory of strings.
 #
@@ -335,6 +344,7 @@ typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
+typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 97af23f67..939c52f31 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -117,7 +117,6 @@ public:
   }
 };/* class DistinctTypeRule */
 
-
 class TupleTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
@@ -131,6 +130,19 @@ public:
   }
 };/* class TupleTypeRule */
 
+class SExprTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    std::vector<TypeNode> types;
+    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+        child_it != child_it_end;
+        ++child_it) {
+      types.push_back((*child_it).getType(check));
+    }
+    return nodeManager->mkSExprType(types);
+  }
+};/* class SExprTypeRule */
+
 class UninterpretedConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
@@ -300,6 +312,58 @@ public:
   }
 };/* class TupleProperties */
 
+class SExprProperties {
+public:
+  inline static Cardinality computeCardinality(TypeNode type) {
+    // Don't assert this; allow other theories to use this cardinality
+    // computation.
+    //
+    // Assert(type.getKind() == kind::SEXPR_TYPE);
+
+    Cardinality card(1);
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      card *= (*i).getCardinality();
+    }
+
+    return card;
+  }
+
+  inline static bool isWellFounded(TypeNode type) {
+    // Don't assert this; allow other theories to use this
+    // wellfoundedness computation.
+    //
+    // Assert(type.getKind() == kind::SEXPR_TYPE);
+
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      if(! (*i).isWellFounded()) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::SEXPR_TYPE);
+
+    std::vector<Node> children;
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      children.push_back((*i).mkGroundTerm());
+    }
+
+    return NodeManager::currentNM()->mkNode(kind::SEXPR, children);
+  }
+};/* class SExprProperties */
+
 class SubtypeProperties {
 public: