Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 32 insertions, 0 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 70bd45c31..405e397b8 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -142,6 +142,20 @@ 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;
 
@@ -399,6 +413,16 @@ 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
@@ -494,6 +518,14 @@ public:
     }
   }
 
+  inline void useDeclarationsFrom(DeclarationScope* scope) {
+    d_declScope = scope;
+  }
+
+  inline DeclarationScope* getDeclarationScope() const {
+    return d_declScope;
+  }
+
   /**
    * Gets the current declaration level.
    */