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, 37 insertions, 1 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 4418ea18f..3efc315cc 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -54,6 +54,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
 }
 
 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
+  checkDeclaration(name, CHECK_DECLARED, type);
   Assert( isDeclared(name, type) );
 
   switch( type ) {
@@ -77,12 +78,14 @@ Expr Parser::getFunction(const std::string& name) {
 
 Type Parser::getType(const std::string& var_name,
                      SymbolType type) {
+  checkDeclaration(var_name, CHECK_DECLARED, type);
   Assert( isDeclared(var_name, type) );
   Type t = getSymbol(var_name, type).getType();
   return t;
 }
 
 Type Parser::getSort(const std::string& name) {
+  checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
   Type t = d_declScope->lookupType(name);
   return t;
@@ -90,12 +93,14 @@ Type Parser::getSort(const std::string& name) {
 
 Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
+  checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
   Type t = d_declScope->lookupType(name, params);
   return t;
 }
 
 size_t Parser::getArity(const std::string& sort_name){
+  checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(sort_name, SYM_SORT) );
   return d_declScope->lookupArity(sort_name);
 }
@@ -236,7 +241,7 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
 SortConstructorType
 Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                     size_t arity) {
-  SortConstructorType unresolved = mkSortConstructor(name,arity);
+  SortConstructorType unresolved = mkSortConstructor(name, arity);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
@@ -325,6 +330,37 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
   return types;
 }
 
+DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds) {
+  DatatypeType& dtt = d_recordTypes[typeIds];
+  if(dtt.isNull()) {
+    Datatype dt("__cvc4_record");
+Debug("datatypes") << "make new record_ctor" << std::endl;
+    DatatypeConstructor c("__cvc4_record_ctor");
+    for(std::vector< std::pair<std::string, Type> >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) {
+      c.addArg((*i).first, (*i).second);
+    }
+    dt.addConstructor(c);
+    dtt = d_exprManager->mkDatatypeType(dt);
+  } else {
+Debug("datatypes") << "use old record_ctor" << std::endl;
+}
+  return dtt;
+}
+
+DatatypeType Parser::mkTupleType(const std::vector<Type>& types) {
+  DatatypeType& dtt = d_tupleTypes[types];
+  if(dtt.isNull()) {
+    Datatype dt("__cvc4_tuple");
+    DatatypeConstructor c("__cvc4_tuple_ctor");
+    for(std::vector<Type>::const_iterator i = types.begin(); i != types.end(); ++i) {
+      c.addArg("__cvc4_tuple_stor", *i);
+    }
+    dt.addConstructor(c);
+    dtt = d_exprManager->mkDatatypeType(dt);
+  }
+  return dtt;
+}
+
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE: