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.)

1 files changed, 20 insertions, 2 deletions

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)));
 }