From 45a138c326da72890bf889a3670aad503ef4aa1e Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 1 Mar 2012 14:48:04 +0000
Subject: 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!
---
 src/parser/parser.h | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'src/parser/parser.h')

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;
 
@@ -398,6 +412,16 @@ public:
   std::vector<DatatypeType>
   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.
    *
@@ -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.
    */
-- 
cgit v1.2.3