post failed attempts at getting the incremental solver to work

11 files changed, 59 insertions, 42 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index fa2a8d1f2..9edc77e39 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -703,8 +703,12 @@ Expr SimplifyCommand::getTerm() const throw() {
 }
 
 void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
-  d_result = smtEngine->simplify(d_term);
-  d_commandStatus = CommandSuccess::instance();
+  try {
+    d_result = smtEngine->simplify(d_term);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 Expr SimplifyCommand::getResult() const throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 342aec5ff..9877044fb 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -401,7 +401,7 @@ public:
 
 /**
  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
- *  via the syntax (! expr :atrr)
+ *  via the syntax (! expr :attr)
  */
 class CVC4_PUBLIC SetUserAttributeCommand : public Command {
 protected:
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index b353ec5dc..f5df63f8c 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -654,6 +654,11 @@ public:
         l = options::defaultExprDepth();
       }
       if(l == 0) {
+        // if called from outside the library, we may not have options
+        // available to us at this point (or perhaps the output language
+        // is not set in Options).  Default to something reasonable, but
+        // don't set "l" since that would make it "sticky" for this
+        // stream.
         return s_defaultPrintDepth;
       }
     }
@@ -797,7 +802,17 @@ public:
     if(l == 0) {
       // set the default dag setting on this ostream
       // (offset by one to detect whether default has been set yet)
-      l = s_defaultDag + 1;
+      if(&Options::current() != NULL) {
+        l = options::defaultDagThresh() + 1;
+      }
+      if(l == 0) {
+        // if called from outside the library, we may not have options
+        // available to us at this point (or perhaps the output language
+        // is not set in Options).  Default to something reasonable, but
+        // don't set "l" since that would make it "sticky" for this
+        // stream.
+        return s_defaultDag + 1;
+      }
     }
     return static_cast<size_t>(l - 1);
   }
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 5134d561e..ca89dfc91 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -2,7 +2,7 @@
 #
 # mkexpr
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create {expr,expr_manager}.{h,cpp}
 # from template files and a list of theory kinds.  Basically it just
@@ -15,7 +15,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -23,7 +23,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 786d6187b..f8432466d 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -2,7 +2,7 @@
 #
 # mkkind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create kind.h (and also
 # type_properties.h) from a template and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -22,7 +22,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 47ffc77f9..160a74eac 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -2,7 +2,7 @@
 #
 # mkmetakind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create metakind.h from a template
 # and a list of theory kinds.
@@ -17,13 +17,14 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 cat <<EOF
 /*********************                                                        */
 /** metakind.h
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index f6aa1920d..5f813dbe8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file node_builder.h
  ** \verbatim
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking, cconway
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com>
+ ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>
+ ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Christopher L. Conway <christopherleeconway@gmail.com>
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -277,7 +277,9 @@ class NodeBuilder {
    * double-decremented later (on destruction/clear).
    */
   inline void realloc() {
-    realloc(d_nvMaxChildren * 2);
+    size_t newSize = 2 * size_t(d_nvMaxChildren);
+    size_t hardLimit = (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
+    realloc(EXPECT_FALSE( newSize > hardLimit ) ? hardLimit : newSize);
   }
 
   /**
@@ -662,6 +664,7 @@ public:
     expr::NodeValue* nv = n.d_nv;
     nv->inc();
     d_nv->d_children[d_nv->d_nchildren++] = nv;
+    Assert(d_nv->d_nchildren <= d_nvMaxChildren);
     return *this;
   }
 
@@ -674,6 +677,7 @@ public:
     expr::NodeValue* nv = typeNode.d_nv;
     nv->inc();
     d_nv->d_children[d_nv->d_nchildren++] = nv;
+    Assert(d_nv->d_nchildren <= d_nvMaxChildren);
     return *this;
   }
 
@@ -771,6 +775,9 @@ template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
   Assert( toSize > d_nvMaxChildren,
           "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
+  Assert( toSize < (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
+          "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
+          toSize, (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
 
   if(EXPECT_FALSE( nvIsAllocated() )) {
     // Ensure d_nv is not modified on allocation failure
@@ -783,6 +790,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
       throw std::bad_alloc();
     }
     d_nvMaxChildren = toSize;
+    Assert(d_nvMaxChildren == toSize);//overflow check
     // Here, the copy (between two heap-allocated buffers) has already
     // been done for us by the std::realloc().
     d_nv = newBlock;
@@ -795,6 +803,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
       throw std::bad_alloc();
     }
     d_nvMaxChildren = toSize;
+    Assert(d_nvMaxChildren == toSize);//overflow check
 
     d_nv = newBlock;
     d_nv->d_id = d_inlineNv.d_id;
@@ -1276,10 +1285,14 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
     return;
   }
 
+  bool realloced CVC4_UNUSED = false;
   if(nb.d_nvMaxChildren > d_nvMaxChildren) {
+    realloced = true;
     realloc(nb.d_nvMaxChildren);
   }
 
+  Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
+  Assert(nb.d_nv->nv_end() - nb.d_nv->nv_begin() <= d_nvMaxChildren, "realloced:%s, d_nvMax:%u, size:%u, nc:%u", realloced ? "true" : "false", d_nvMaxChildren, nb.d_nv->nv_end() - nb.d_nv->nv_begin(), nb.d_nv->getNumChildren());
   std::copy(nb.d_nv->nv_begin(),
             nb.d_nv->nv_end(),
             d_nv->nv_begin());
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 59d23c6ea..a3c968158 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -412,6 +412,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dt.addConstructor(c);
       dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
       Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
+      dtt.setAttribute(DatatypeTupleAttr(), t);
     } else {
       const Record& rec = t.getRecord();
       Datatype dt("__cvc4_record");
@@ -422,8 +423,8 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dt.addConstructor(c);
       dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
       Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
+      dtt.setAttribute(DatatypeRecordAttr(), t);
     }
-    dtt.setAttribute(DatatypeRecordAttr(), t);
   } else {
     Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
   }
diff --git a/src/expr/options b/src/expr/options
index cd59e4875..223189d1b 100644
--- a/src/expr/options
+++ b/src/expr/options
@@ -5,9 +5,9 @@
 
 module EXPR "expr/options.h" Expression package
 
-option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
+option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
  print exprs to depth N (0 == default, -1 == no limit)
-option - default-dag-thresh --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h"
+option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h"
  dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
 option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
  print types with variables when printing exprs
diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h
index 7a1d73c36..57c4d1aa4 100644
--- a/src/expr/options_handlers.h
+++ b/src/expr/options_handlers.h
@@ -39,8 +39,7 @@ inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) {
   // intentionally exclude Dump stream from this list
 }
 
-inline void setDefaultDagThresh(std::string option, std::string optarg, SmtEngine* smt) {
-  int dag = atoi(optarg.c_str());
+inline void setDefaultDagThresh(std::string option, int dag, SmtEngine* smt) {
   if(dag < 0) {
     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
   }
diff --git a/src/expr/type.i b/src/expr/type.i
index 870cb228c..e227cca23 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -14,24 +14,6 @@
 %rename(greater) CVC4::Type::operator>(const Type&) const;
 %rename(greaterEqual) CVC4::Type::operator>=(const Type&) const;
 
-%rename(toBooleanType) CVC4::Type::operator BooleanType() const;
-%rename(toIntegerType) CVC4::Type::operator IntegerType() const;
-%rename(toRealType) CVC4::Type::operator RealType() const;
-%rename(toStringType) CVC4::Type::operator StringType() const;
-%rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
-%rename(toFunctionType) CVC4::Type::operator FunctionType() const;
-%rename(toTupleType) CVC4::Type::operator TupleType() const;
-%rename(toSExprType) CVC4::Type::operator SExprType() const;
-%rename(toArrayType) CVC4::Type::operator ArrayType() const;
-%rename(toDatatypeType) CVC4::Type::operator DatatypeType() const;
-%rename(toConstructorType) CVC4::Type::operator ConstructorType() const;
-%rename(toSelectorType) CVC4::Type::operator SelectorType() const;
-%rename(toTesterType) CVC4::Type::operator TesterType() const;
-%rename(toSortType) CVC4::Type::operator SortType() const;
-%rename(toSortConstructorType) CVC4::Type::operator SortConstructorType() const;
-%rename(toPredicateSubtype) CVC4::Type::operator PredicateSubtype() const;
-%rename(toSubrangeType) CVC4::Type::operator SubrangeType() const;
-
 namespace CVC4 {
   namespace expr {
     %ignore exportTypeInternal;