diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_builder.h | 53 | ||||
-rw-r--r-- | src/expr/node_value.h | 6 | ||||
-rw-r--r-- | src/main/main.cpp | 6 | ||||
-rw-r--r-- | src/util/configuration.cpp | 12 | ||||
-rw-r--r-- | src/util/configuration.h | 1 | ||||
-rw-r--r-- | src/util/configuration_private.h | 17 |
6 files changed, 69 insertions, 26 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 95f7c0437..252cba43e 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -459,9 +459,9 @@ public: inline const_iterator begin() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - CheckArgument(getKind() != kind::UNDEFINED_KIND, - "Iterators over NodeBuilder<> are undefined " - "until a Kind is set"); + Assert(getKind() != kind::UNDEFINED_KIND, + "Iterators over NodeBuilder<> are undefined " + "until a Kind is set"); return d_nv->begin< NodeTemplate<true> >(); } @@ -469,9 +469,9 @@ public: inline const_iterator end() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - CheckArgument(getKind() != kind::UNDEFINED_KIND, - "Iterators over NodeBuilder<> are undefined " - "until a Kind is set"); + Assert(getKind() != kind::UNDEFINED_KIND, + "Iterators over NodeBuilder<> are undefined " + "until a Kind is set"); return d_nv->end< NodeTemplate<true> >(); } @@ -486,9 +486,9 @@ public: inline kind::MetaKind getMetaKind() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - CheckArgument(getKind() != kind::UNDEFINED_KIND, - "The metakind of a NodeBuilder<> is undefined " - "until a Kind is set"); + Assert(getKind() != kind::UNDEFINED_KIND, + "The metakind of a NodeBuilder<> is undefined " + "until a Kind is set"); return d_nv->getMetaKind(); } @@ -496,19 +496,40 @@ public: inline unsigned getNumChildren() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - CheckArgument(getKind() != kind::UNDEFINED_KIND, - "The number of children of a NodeBuilder<> is undefined " - "until a Kind is set"); + Assert(getKind() != kind::UNDEFINED_KIND, + "The number of children of a NodeBuilder<> is undefined " + "until a Kind is set"); return d_nv->getNumChildren(); } - /** Access to children of this Node-under-construction. */ + /** + * Access to the operator of this Node-under-construction. Only + * allowed if this NodeBuilder is unused, and has a defined kind + * that is of PARAMETERIZED metakind. + */ + inline Node getOperator() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + Assert(getKind() != kind::UNDEFINED_KIND, + "NodeBuilder<> operator access is not permitted " + "until a Kind is set"); + Assert(getMetaKind() == kind::metakind::PARAMETERIZED, + "NodeBuilder<> operator access is only permitted " + "on parameterized kinds, not `%s'", + kind::kindToString(getKind()).c_str()); + return Node(d_nv->getOperator()); + } + + /** + * Access to children of this Node-under-construction. Only allowed + * if this NodeBuilder is unused and has a defined kind. + */ inline Node getChild(int i) const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - CheckArgument(getKind() != kind::UNDEFINED_KIND, - "NodeBuilder<> child access is not permitted " - "until a Kind is set"); + Assert(getKind() != kind::UNDEFINED_KIND, + "NodeBuilder<> child access is not permitted " + "until a Kind is set"); Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(), "index out of range for NodeBuilder::getChild()"); return Node(d_nv->getChild(i)); diff --git a/src/expr/node_value.h b/src/expr/node_value.h index f2da42731..2c11b58d5 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -290,6 +290,7 @@ public: template <class T> inline const T& getConst() const; + NodeValue* getOperator() const; NodeValue* getChild(int i) const; void printAst(std::ostream& out, int indent = 0) const; @@ -432,6 +433,11 @@ inline bool NodeValue::isBeingDeleted() const { NodeManager::currentNM()->isCurrentlyDeleting(this); } +inline NodeValue* NodeValue::getOperator() const { + Assert(getMetaKind() == kind::metakind::PARAMETERIZED); + return d_children[0]; +} + inline NodeValue* NodeValue::getChild(int i) const { if(getMetaKind() == kind::metakind::PARAMETERIZED) { ++i; diff --git a/src/main/main.cpp b/src/main/main.cpp index 9c2464b8d..c21a7bdac 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -281,11 +281,7 @@ int runCvc4(int argc, char* argv[]) { Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); if(Configuration::isSubversionBuild()) { - Message() << " [subversion " << Configuration::getSubversionBranchName() - << " r" << Configuration::getSubversionRevision() - << (Configuration::hasSubversionModifications() ? - " (with modifications)" : "") - << "]"; + Message() << " [" << Configuration::getSubversionId() << "]"; } Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") << " assertions:" diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index db3c5520e..aa3e6bf6b 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -19,6 +19,7 @@ **/ #include <string> +#include <sstream> #include "util/configuration.h" #include "util/configuration_private.h" @@ -124,4 +125,15 @@ bool Configuration::hasSubversionModifications() { return SUBVERSION_HAS_MODIFICATIONS; } +string Configuration::getSubversionId() { + if(! isSubversionBuild()) { + return ""; + } + + stringstream ss; + ss << "subversion " << getSubversionBranchName() << " r" << getSubversionRevision() + << ( ::CVC4::Configuration::hasSubversionModifications() ? " (with modifications)" : "" ); + return ss.str(); +} + }/* CVC4 namespace */ diff --git a/src/util/configuration.h b/src/util/configuration.h index 258431114..31a2ca3d4 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -87,6 +87,7 @@ public: static const char* getSubversionBranchName(); static unsigned getSubversionRevision(); static bool hasSubversionModifications(); + static std::string getSubversionId(); };/* class Configuration */ diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 4f7501a08..0421273ca 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -20,6 +20,9 @@ #ifndef __CVC4__CONFIGURATION_PRIVATE_H #define __CVC4__CONFIGURATION_PRIVATE_H +#include <string> +#include "util/configuration.h" + namespace CVC4 { #ifdef CVC4_DEBUG @@ -100,14 +103,18 @@ namespace CVC4 { # define USING_TLS false #endif /* TLS */ -#define CVC4_ABOUT_STRING string("\ -This is CVC4 version " CVC4_RELEASE_STRING "\n\n\ +#define CVC4_ABOUT_STRING ( ::std::string("\ +This is CVC4 version " CVC4_RELEASE_STRING ) + \ + ( ::CVC4::Configuration::isSubversionBuild() \ + ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \ + : ::std::string("") \ + ) + "\n\n\ Copyright (C) 2009, 2010, 2011\n\ The ACSys Group\n\ Courant Institute of Mathematical Sciences\n\ New York University\n\ - New York, NY 10012 USA\n\n") + \ - (IS_CLN_BUILD ? "\ + New York, NY 10012 USA\n\n" + \ + ( IS_CLN_BUILD ? "\ This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\ CVC4 is open-source and is covered by the BSD license (modified).\n\ However, CLN, the Class Library for Numbers, is covered by the GPL. Thus\n\ @@ -116,7 +123,7 @@ consult the CVC4 documentation for instructions about building a version\n\ of CVC4 that links against GMP, and can be used in such applications.\n" : \ "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\ CVC4 is open-source and is covered by the BSD license (modified).\n\n\ -THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n") +THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n" ) ) }/* CVC4 namespace */ |