1 files changed, 2 insertions, 103 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 3f180e951..1458101ca 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -2,10 +2,10 @@
 /*! \file expr_manager_template.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
+ **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -28,12 +28,6 @@
 
 ${includes}
 
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 36 "${template}"
-
 namespace CVC4 {
 
 namespace api {
@@ -65,11 +59,6 @@ class CVC4_PUBLIC ExprManager {
   NodeManager* getNodeManager() const;
 
   /**
-   * Check some things about a newly-created DatatypeType.
-   */
-  void checkResolvedDatatype(DatatypeType dtt) const;
-
-  /**
    * SmtEngine will use all the internals, so it will grab the
    * NodeManager.
    */
@@ -84,10 +73,6 @@ class CVC4_PUBLIC ExprManager {
   // undefined, private copy constructor and assignment op (disallow copy)
   ExprManager(const ExprManager&) = delete;
   ExprManager& operator=(const ExprManager&) = delete;
-
-  /** A list of datatypes owned by this expr manager. */
-  std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
-
   /** Creates an expression manager. */
   ExprManager();
  public:
@@ -346,18 +331,6 @@ class CVC4_PUBLIC ExprManager {
   FunctionType mkPredicateType(const std::vector<Type>& sorts);
 
   /**
-   * Make a tuple type with types from
-   * <code>types[0..types.size()-1]</code>.  <code>types</code> must
-   * have at least one element.
-   */
-  DatatypeType mkTupleType(const std::vector<Type>& types);
-
-  /**
-   * Make a record type with types from the rec parameter.
-   */
-  DatatypeType mkRecordType(const Record& rec);
-
-  /**
    * Make a symbolic expressiontype with types from
    * <code>types[0..types.size()-1]</code>.  <code>types</code> may
    * have any number of elements.
@@ -379,73 +352,6 @@ class CVC4_PUBLIC ExprManager {
   /** Make the type of sequence with the given parameterization. */
   SequenceType mkSequenceType(Type elementType) const;
 
-  /** Bits for use in mkDatatypeType() flags.
-   *
-   * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
-   * out as a definition, for example, in models or during dumping.
-   */
-  enum
-  {
-    DATATYPE_FLAG_NONE = 0,
-    DATATYPE_FLAG_PLACEHOLDER = 1
-  }; /* enum */
-
-  /** Make a type representing the given datatype. */
-  DatatypeType mkDatatypeType(Datatype& datatype,
-                              uint32_t flags = DATATYPE_FLAG_NONE);
-
-  /**
-   * Make a set of types representing the given datatypes, which may be
-   * mutually recursive.
-   */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(
-      std::vector<Datatype>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
-
-  /**
-   * Make a set of types representing the given datatypes, which may
-   * be mutually recursive.  unresolvedTypes is a set of SortTypes
-   * that were used as placeholders in the Datatypes for the Datatypes
-   * of the same name.  This is just a more complicated version of the
-   * above mkMutualDatatypeTypes() function, but is required to handle
-   * complex types.
-   *
-   * For example, unresolvedTypes might contain the single sort "list"
-   * (with that name reported from SortType::getName()).  The
-   * datatypes list might have the single datatype
-   *
-   *   DATATYPE
-   *     list = cons(car:ARRAY INT OF list, cdr:list) | nil;
-   *   END;
-   *
-   * To represent the Type of the array, the user had to create a
-   * placeholder type (an uninterpreted sort) to stand for "list" in
-   * the type of "car".  It is this placeholder sort that should be
-   * passed in unresolvedTypes.  If the datatype was of the simpler
-   * form:
-   *
-   *   DATATYPE
-   *     list = cons(car:list, cdr:list) | nil;
-   *   END;
-   *
-   * then no complicated Type needs to be created, and the above,
-   * simpler form of mkMutualDatatypeTypes() is enough.
-   */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(
-      std::vector<Datatype>& datatypes,
-      std::set<Type>& unresolvedTypes,
-      uint32_t flags = DATATYPE_FLAG_NONE);
-
-  /**
-   * Make a type representing a constructor with the given parameterization.
-   */
-  ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
-
-  /** Make a type representing a selector with the given parameterization. */
-  SelectorType mkSelectorType(Type domain, Type range) const;
-
-  /** Make a type representing a tester with the given parameterization. */
-  TesterType mkTesterType(Type domain) const;
-
   /** Bits for use in mkSort() flags. */
   enum {
     SORT_FLAG_NONE = 0,
@@ -578,13 +484,6 @@ class CVC4_PUBLIC ExprManager {
    * maximal arity as the maximal possible number of children of a node.
    **/
   static bool isNAryKind(Kind fun);
-
-  /**
-   * Return the datatype at the given index owned by this class. Type nodes are
-   * associated with datatypes through the DatatypeIndexConstant class. The
-   * argument index is intended to be a value taken from that class.
-   */
-  const Datatype& getDatatypeForIndex(unsigned index) const;
 };/* class ExprManager */
 
 ${mkConst_instantiations}