Tuples and records merge. Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

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

1 files changed, 0 insertions, 24 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index eb76900d2..eed8531a5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -141,20 +141,6 @@ class CVC4_PUBLIC Parser {
   /** Are we only parsing? */
   bool d_parseOnly;
 
-  /**
-   * We might see the same record type multiple times; we have
-   * to match always to the same Type.  This map contains all the
-   * record types we have.
-   */
-  std::map<std::vector< std::pair<std::string, Type> >, DatatypeType> d_recordTypes;
-
-  /**
-   * We might see the same tuple type multiple times; we have
-   * to match always to the same Type.  This map contains all the
-   * tuple types we have.
-   */
-  std::map<std::vector<Type>, DatatypeType> d_tupleTypes;
-
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
@@ -420,16 +406,6 @@ public:
   mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
 
   /**
-   * Create a record type, or if there's already a matching one, return that one.
-   */
-  DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds);
-
-  /**
-   * Create a tuple type, or if there's already a matching one, return that one.
-   */
-  DatatypeType mkTupleType(const std::vector<Type>& types);
-
-  /**
    * Add an operator to the current legal set.
    *
    * @param kind the built-in operator to add