First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

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

1 files changed, 57 insertions, 53 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 10ca16001..57589ec9c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -277,66 +277,70 @@ bool Parser::isUnresolvedType(const std::string& name) {
 std::vector<DatatypeType>
 Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 
-  std::vector<DatatypeType> types =
-    d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
-
-  assert(datatypes.size() == types.size());
-
-  for(unsigned i = 0; i < datatypes.size(); ++i) {
-    DatatypeType t = types[i];
-    const Datatype& dt = t.getDatatype();
-    const std::string& name = dt.getName();
-    Debug("parser-idt") << "define " << name << " as " << t << std::endl;
-    if(isDeclared(name, SYM_SORT)) {
-      throw ParserException(name + " already declared");
-    }
-    if( t.isParametric() ) {
-      std::vector< Type > paramTypes = t.getParamTypes();
-      defineType(name, paramTypes, t );
-    } else {
-      defineType(name, t);
-    }
-    for(Datatype::const_iterator j = dt.begin(),
-          j_end = dt.end();
-        j != j_end;
-        ++j) {
-      const DatatypeConstructor& ctor = *j;
-      Expr::printtypes::Scope pts(Debug("parser-idt"), true);
-      Expr constructor = ctor.getConstructor();
-      Debug("parser-idt") << "+ define " << constructor << std::endl;
-      string constructorName = ctor.getName();
-      if(isDeclared(constructorName, SYM_VARIABLE)) {
-        throw ParserException(constructorName + " already declared");
+  try {
+    std::vector<DatatypeType> types =
+      d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+
+    assert(datatypes.size() == types.size());
+
+    for(unsigned i = 0; i < datatypes.size(); ++i) {
+      DatatypeType t = types[i];
+      const Datatype& dt = t.getDatatype();
+      const std::string& name = dt.getName();
+      Debug("parser-idt") << "define " << name << " as " << t << std::endl;
+      if(isDeclared(name, SYM_SORT)) {
+        throw ParserException(name + " already declared");
       }
-      defineVar(constructorName, constructor);
-      Expr tester = ctor.getTester();
-      Debug("parser-idt") << "+ define " << tester << std::endl;
-      string testerName = ctor.getTesterName();
-      if(isDeclared(testerName, SYM_VARIABLE)) {
-        throw ParserException(testerName + " already declared");
+      if( t.isParametric() ) {
+        std::vector< Type > paramTypes = t.getParamTypes();
+        defineType(name, paramTypes, t );
+      } else {
+        defineType(name, t);
       }
-      defineVar(testerName, tester);
-      for(DatatypeConstructor::const_iterator k = ctor.begin(),
-            k_end = ctor.end();
-          k != k_end;
-          ++k) {
-        Expr selector = (*k).getSelector();
-        Debug("parser-idt") << "+++ define " << selector << std::endl;
-        string selectorName = (*k).getName();
-        if(isDeclared(selectorName, SYM_VARIABLE)) {
-          throw ParserException(selectorName + " already declared");
+      for(Datatype::const_iterator j = dt.begin(),
+            j_end = dt.end();
+          j != j_end;
+          ++j) {
+        const DatatypeConstructor& ctor = *j;
+        Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+        Expr constructor = ctor.getConstructor();
+        Debug("parser-idt") << "+ define " << constructor << std::endl;
+        string constructorName = ctor.getName();
+        if(isDeclared(constructorName, SYM_VARIABLE)) {
+          throw ParserException(constructorName + " already declared");
+        }
+        defineVar(constructorName, constructor);
+        Expr tester = ctor.getTester();
+        Debug("parser-idt") << "+ define " << tester << std::endl;
+        string testerName = ctor.getTesterName();
+        if(isDeclared(testerName, SYM_VARIABLE)) {
+          throw ParserException(testerName + " already declared");
+        }
+        defineVar(testerName, tester);
+        for(DatatypeConstructor::const_iterator k = ctor.begin(),
+              k_end = ctor.end();
+            k != k_end;
+            ++k) {
+          Expr selector = (*k).getSelector();
+          Debug("parser-idt") << "+++ define " << selector << std::endl;
+          string selectorName = (*k).getName();
+          if(isDeclared(selectorName, SYM_VARIABLE)) {
+            throw ParserException(selectorName + " already declared");
+          }
+          defineVar(selectorName, selector);
         }
-        defineVar(selectorName, selector);
       }
     }
-  }
 
-  // These are no longer used, and the ExprManager would have
-  // complained of a bad substitution if anything is left unresolved.
-  // Clear out the set.
-  d_unresolved.clear();
+    // These are no longer used, and the ExprManager would have
+    // complained of a bad substitution if anything is left unresolved.
+    // Clear out the set.
+    d_unresolved.clear();
 
-  return types;
+    return types;
+  } catch(IllegalArgumentException& ie) {
+    throw ParserException(ie.getMessage());
+  }
 }
 
 bool Parser::isDeclared(const std::string& name, SymbolType type) {