From: Morgan Deters Date: Thu, 30 Jun 2011 03:56:58 +0000 (+0000) Subject: some things I had laying around in a directory but never got committed; minor fix... X-Git-Tag: cvc5-1.0.0~8529 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c64799a735cc9fecb8e618b2c66b252d7cda549d;p=cvc5.git some things I had laying around in a directory but never got committed; minor fix-ups to documentation and some node stuff --- 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 >(); } @@ -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 >(); } @@ -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 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 +#include #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 +#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 */ diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 320d4ddbe..c084c4ecb 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -96,9 +96,11 @@ public: /* default size tests */ NodeBuilder<> def; TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(def.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(def.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(def.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(def.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(def.begin(), AssertionException); + TS_ASSERT_THROWS(def.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); @@ -108,9 +110,11 @@ public: NodeBuilder<> from_nm(d_nm); TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(from_nm.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(from_nm.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(from_nm.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(from_nm.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(from_nm.begin(), AssertionException); + TS_ASSERT_THROWS(from_nm.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> from_nm_kind(d_nm, specKind); TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind); @@ -122,9 +126,11 @@ public: NodeBuilder ws; TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(ws.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(ws.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(ws.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(ws.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(ws.begin(), AssertionException); + TS_ASSERT_THROWS(ws.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder ws_kind(specKind); TS_ASSERT_EQUALS(ws_kind.getKind(), specKind); @@ -134,9 +140,11 @@ public: NodeBuilder ws_from_nm(d_nm); TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(ws_from_nm.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(ws_from_nm.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(ws_from_nm.begin(), AssertionException); + TS_ASSERT_THROWS(ws_from_nm.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder ws_from_nm_kind(d_nm, specKind); TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind); @@ -153,27 +161,35 @@ public: NodeBuilder<> copy(def); TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(copy.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(copy.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(copy.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(copy.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(copy.begin(), AssertionException); + TS_ASSERT_THROWS(copy.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder cp_ws(ws); TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(cp_ws.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(cp_ws.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(cp_ws.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(cp_ws.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(cp_ws.begin(), AssertionException); + TS_ASSERT_THROWS(cp_ws.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder cp_from_larger(ws); TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(cp_from_larger.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(cp_from_larger.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(cp_from_larger.begin(), AssertionException); + TS_ASSERT_THROWS(cp_from_larger.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder cp_from_smaller(ws); TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(cp_from_smaller.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(cp_from_smaller.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(cp_from_smaller.begin(), AssertionException); + TS_ASSERT_THROWS(cp_from_smaller.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testDestructor() { @@ -284,7 +300,9 @@ public: Node x( d_nm->mkVar( *d_integerType ) ); NodeBuilder<> nb; - TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException); +#endif /* CVC4_ASSERTIONS */ nb << PLUS << x << x; TS_ASSERT_EQUALS(nb.getNumChildren(), 2u); @@ -294,7 +312,9 @@ public: Node n = nb;// avoid warning on clear() nb.clear(); - TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException); +#endif /* CVC4_ASSERTIONS */ nb.clear(PLUS); TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); nb << x << x << x; @@ -368,9 +388,11 @@ public: NodeBuilder<> nb; TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(nb.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(nb.begin(), AssertionException); + TS_ASSERT_THROWS(nb.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ nb << specKind; push_back(nb, K); @@ -383,9 +405,11 @@ public: nb.clear(); TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(nb.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(nb.begin(), AssertionException); + TS_ASSERT_THROWS(nb.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ nb << specKind; push_back(nb, K); @@ -406,9 +430,11 @@ public: nb.clear(); TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); - TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException); - TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException); - TS_ASSERT_THROWS(nb.end(), IllegalArgumentException); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException); + TS_ASSERT_THROWS(nb.begin(), AssertionException); + TS_ASSERT_THROWS(nb.end(), AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testStreamInsertionKind() {