diff options
author | lianah <lianahady@gmail.com> | 2013-03-13 13:44:33 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-13 13:44:33 -0400 |
commit | 3fcdb18fe92e5213aa708285c0d7d5e55633492b (patch) | |
tree | bbbd57efd9a8063a976a55afa7c384fb67db9b17 /src/expr | |
parent | 267ad0ceb6808bd4c05d7c4bb04a7886efc19eab (diff) | |
parent | 9817df56827b4ee0ee67a33361f8619c5d1df6ed (diff) |
post failed attempts at getting the incremental solver to work
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 8 | ||||
-rw-r--r-- | src/expr/command.h | 2 | ||||
-rw-r--r-- | src/expr/expr_template.h | 17 | ||||
-rwxr-xr-x | src/expr/mkexpr | 7 | ||||
-rwxr-xr-x | src/expr/mkkind | 7 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 7 | ||||
-rw-r--r-- | src/expr/node_builder.h | 25 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/options | 4 | ||||
-rw-r--r-- | src/expr/options_handlers.h | 3 | ||||
-rw-r--r-- | src/expr/type.i | 18 |
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; |