diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-06-04 18:55:22 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-06-04 18:55:22 +0000 |
| commit | a460f751e8345e61c4989386765d84bb76fe37d6 (patch) | |
| tree | 08bc3c035b5bd8f220853e06dc90fb939c55b2ed | |
| parent | febba49895125f4f3489e7dff283a000ae9965b3 (diff) | |
** Don't fear the files-changed list, almost all changes are in the **
** file-level documentation at the top of the sources. **
This is the "make bugzilla stop bugging me" bugfix commit.
* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
Updated documentation in the file. Resolves bug #99.
* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
moved into a separate file. Partially resolves bug #100.
* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
namespace) instead of metakind.h (where it was in CVC4::metakind).
This clears up a warning (private #inclusion) from the SMT and SMT2
parsers, and maybe makes more sense anyways, since this is based on
the kind (and not the metakind) of an operator.
* Documentation improvement; doxygen top-level \file gestures, \brief
gestures for files, etc. Changed contrib/update-copyright.pl for
this change, and post-processed to add \brief. Resolves bug #98.
* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
They no longer made sense. Resolves bug #91.
172 files changed, 1876 insertions, 1224 deletions
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index dce453346..cf02e1ece 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -28,7 +28,9 @@ # the license.) my $excluded_directories = '^(minisat|CVS|generated)$'; -my $excluded_paths = '^(src/parser/bounded_token_buffer\.(h|cpp))|(src/parser/antlr_input_imports.cpp)$'; +# re-include bounded_token_buffer.{h,cpp} +#my $excluded_paths = '^(src/parser/bounded_token_buffer\.(h|cpp))|(src/parser/antlr_input_imports.cpp)$'; +my $excluded_paths = '^src/parser/antlr_input_imports.cpp$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. @@ -40,7 +42,7 @@ my $standard_template = <<EOF; ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\\endverbatim EOF my $public_template = <<EOF; @@ -49,7 +51,7 @@ my $public_template = <<EOF; ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\\endverbatim EOF ## end config ## @@ -125,11 +127,12 @@ sub recurse { } elsif($file =~ /\.g$/) { # avoid javadoc-style comment here; antlr complains print $OUT "/* ******************* */\n"; - print $OUT "/* $file\n"; + print $OUT "/*! \\file $file\n"; } else { print $OUT "/********************* */\n"; - print $OUT "/** $file\n"; + print $OUT "/*! \\file $file\n"; } + print $OUT " ** \\verbatim\n"; print $OUT " ** Original author: $author\n"; print $OUT " ** Major contributors: $major_contributors\n"; print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; @@ -143,21 +146,25 @@ sub recurse { print "adding\n"; if($file =~ /\.(y|yy|ypp|Y)$/) { print $OUT "%{/******************* */\n"; - print $OUT "/** $file\n"; + print $OUT "/*! \\file $file\n"; } elsif($file =~ /\.g$/) { # avoid javadoc-style comment here; antlr complains print $OUT "/* ******************* */\n"; - print $OUT "/* $file\n"; + print $OUT "/*! \\file $file\n"; } else { print $OUT "/********************* */\n"; - print $OUT "/** $file\n"; + print $OUT "/*! \\file $file\n"; } + print $OUT " ** \\verbatim\n"; print $OUT " ** Original author: $author\n"; print $OUT " ** Major contributors: $major_contributors\n"; print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; print $OUT $standard_template; print $OUT " **\n"; - print $OUT " ** [[ Add file-specific comments here ]]\n"; + print $OUT " ** \brief [[ Add one-line brief description here ]]\n"; + print $OUT " **\n"; + print $OUT " ** [[ Add lengthier description here ]]\n"; + print $OUT " ** \\todo document this file\n"; print $OUT " **/\n\n"; print $OUT $line; if($file =~ /\.(y|yy|ypp|Y)$/) { diff --git a/src/context/cdlist.h b/src/context/cdlist.h index a2abc08d8..e3bf4d56b 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -1,5 +1,6 @@ /********************* */ -/** cdlist.h +/*! \file cdlist.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): barrett, taking @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Context-dependent list class. ** ** Context-dependent list class. **/ diff --git a/src/context/cdmap.h b/src/context/cdmap.h index b0ffc91a4..28be629c4 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -1,14 +1,17 @@ /********************* */ -/** cdmap.h +/*! \file cdmap.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Context-dependent map class. ** ** Context-dependent map class. Generic templated class for a map ** which must be saved and restored as contexts are pushed and diff --git a/src/context/cdo.h b/src/context/cdo.h index ead43b2e8..20c512fbc 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -1,5 +1,6 @@ /********************* */ -/** cdo.h +/*! \file cdo.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): barrett @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A context-dependent object. ** ** A context-dependent object. **/ diff --git a/src/context/cdset.h b/src/context/cdset.h index f51e689d5..40d504cad 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -1,5 +1,6 @@ /********************* */ -/** cdset.h +/*! \file cdset.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Context-dependent set class. ** ** Context-dependent set class. **/ diff --git a/src/context/context.cpp b/src/context/context.cpp index b003571c1..994f644a7 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -1,14 +1,17 @@ /********************* */ -/** context.cpp +/*! \file context.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: barrett - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of base context operations. ** ** Implementation of base context operations. **/ diff --git a/src/context/context.h b/src/context/context.h index caa5fa57b..12d7c4673 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -1,5 +1,6 @@ /********************* */ -/** context.h +/*! \file context.h + ** \verbatim ** Original author: mdeters ** Major contributors: barrett ** Minor contributors (to current version): taking, dejan @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Context class and context manager. ** ** Context class and context manager. **/ diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index a202edf19..6a277245e 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -1,5 +1,6 @@ /********************* */ -/** context_mm.cpp +/*! \file context_mm.cpp + ** \verbatim ** Original author: barrett ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,9 +9,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim ** - ** Implementation of Context Memory Manaer + ** \brief Implementation of Context Memory Manager. + ** + ** Implementation of Context Memory Manager **/ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 5920859e1..1eb452113 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -1,5 +1,6 @@ /********************* */ -/** context_mm.h +/*! \file context_mm.h + ** \verbatim ** Original author: barrett ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Region-based memory manager with stack-based push and pop. ** ** Region-based memory manager with stack-based push and pop. Designed ** for use by ContextManager. diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index c3c3fccf6..cacae45ce 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -12,6 +12,7 @@ libexpr_la_SOURCES = \ type_node.cpp \ builtin_type_rules.h \ node_builder.h \ + convenience_node_builders.h \ @srcdir@/expr.h \ type.h \ type.cpp \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index bc724cdd1..5aaa7393a 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -1,14 +1,17 @@ /********************* */ -/** attribute.cpp +/*! \file attribute.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief AttributeManager implementation. ** ** AttributeManager implementation. **/ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 619f60a6c..2ef34a771 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -1,14 +1,17 @@ /********************* */ -/** attribute.h +/*! \file attribute.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): cconway, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Node attributes. ** ** Node attributes. **/ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 4ac89afec..b5ccb6f79 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -1,14 +1,17 @@ /********************* */ -/** attribute_internals.h +/*! \file attribute_internals.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan, taking, cconway + ** Minor contributors (to current version): taking, dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Node attributes' internals. ** ** Node attributes' internals. **/ diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h index e0ad0b038..afd206260 100644 --- a/src/expr/builtin_type_rules.h +++ b/src/expr/builtin_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** builtin_type_rules.cpp +/*! \file builtin_type_rules.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none ** This file is part of the CVC4 prototype. @@ -7,7 +8,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add brief comments here ]] + ** + ** [[ Add file-specific comments here ]] **/ #include "cvc4_private.h" diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 5fc9dee20..6c466a74c 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1,5 +1,6 @@ /********************* */ -/** command.cpp +/*! \file command.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of command objects. ** ** Implementation of command objects. **/ diff --git a/src/expr/command.h b/src/expr/command.h index 5061722f6..388ad62e6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -1,14 +1,17 @@ /********************* */ -/** command.h +/*! \file command.h + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of the command pattern on SmtEngines. ** ** Implementation of the command pattern on SmtEngines. Command ** objects are generated by the parser (typically) to implement the diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h new file mode 100644 index 000000000..655accde3 --- /dev/null +++ b/src/expr/convenience_node_builders.h @@ -0,0 +1,401 @@ +/********************* */ +/*! \file convenience_node_builders.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Convenience node builders. + ** + ** These are convenience node builders for building AND, OR, PLUS, + ** and MULT expressions. + ** + ** \todo These should be moved into theory code (say, + ** src/theory/booleans/node_builders.h and + ** src/theory/arith/node_builders.h), but for now they're here + ** because their design requires CVC4::NodeBuilder to friend them. + **/ + +// TODO: add templatized NodeTemplate<ref_count> to all these inlines +// for 'const [T]Node&' arguments? Technically a lot of time is spent +// in the TNode conversion and copy constructor, but this should be +// optimized into a simple pointer copy (?) +// TODO: double-check this. + +#include "cvc4_private.h" + +#ifndef __CVC4__CONVENIENCE_NODE_BUILDERS_H +#define __CVC4__CONVENIENCE_NODE_BUILDERS_H + +#include "expr/node_builder.h" + +namespace CVC4 { + +class AndNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::AND); + } + + inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) { + d_eb << a << b; + } + + template <bool rc> + inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&); + + template <bool rc> + inline OrNodeBuilder operator||(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class AndNodeBuilder */ + +class OrNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::OR); + } + + inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) { + d_eb << a << b; + } + + template <bool rc> + inline AndNodeBuilder operator&&(const NodeTemplate<rc>&); + + template <bool rc> + inline OrNodeBuilder& operator||(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class OrNodeBuilder */ + +class PlusNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::PLUS); + } + + inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) { + d_eb << a << b; + } + + template <bool rc> + inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&); + + template <bool rc> + inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&); + + template <bool rc> + inline MultNodeBuilder operator*(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class PlusNodeBuilder */ + +class MultNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::MULT); + } + + inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) { + d_eb << a << b; + } + + template <bool rc> + inline PlusNodeBuilder operator+(const NodeTemplate<rc>&); + + template <bool rc> + inline PlusNodeBuilder operator-(const NodeTemplate<rc>&); + + template <bool rc> + inline MultNodeBuilder& operator*(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class MultNodeBuilder */ + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) { + return collapseTo(kind::AND).append(e); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) { + return collapseTo(kind::OR).append(e); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) { + return collapseTo(kind::PLUS).append(e); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) { + return collapseTo(kind::PLUS). + append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) { + return collapseTo(kind::MULT).append(e); +} + +template <bool rc> +inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +template <bool rc> +inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) { + return OrNodeBuilder(Node(d_eb), n); +} + +inline AndNodeBuilder& operator&&(AndNodeBuilder& a, + const AndNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline AndNodeBuilder& operator&&(AndNodeBuilder& a, + const OrNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder operator||(AndNodeBuilder& a, + const AndNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder operator||(AndNodeBuilder& a, + const OrNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) { + return AndNodeBuilder(Node(d_eb), n); +} + +template <bool rc> +inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +inline AndNodeBuilder operator&&(OrNodeBuilder& a, + const AndNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline AndNodeBuilder operator&&(OrNodeBuilder& a, + const OrNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder& operator||(OrNodeBuilder& a, + const AndNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder& operator||(OrNodeBuilder& a, + const OrNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +template <bool rc> +inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) { + d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n)); + return *this; +} + +template <bool rc> +inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) { + return MultNodeBuilder(Node(d_eb), n); +} + +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, + const PlusNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, + const MultNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, + const PlusNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, + const MultNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, + const PlusNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, + const MultNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { + return PlusNodeBuilder(Node(d_eb), n); +} + +template <bool rc> +inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) { + return PlusNodeBuilder(Node(d_eb), + NodeManager::currentNM()->mkNode(kind::UMINUS, n)); +} + +template <bool rc> +inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +inline PlusNodeBuilder operator+(MultNodeBuilder& a, + const PlusNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder operator+(MultNodeBuilder& a, + const MultNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, + const PlusNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, + const MultNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, + const PlusNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, + const MultNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc1, bool rc2> +inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return AndNodeBuilder(a, b); +} + +template <bool rc1, bool rc2> +inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return OrNodeBuilder(a, b); +} + +template <bool rc1, bool rc2> +inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return PlusNodeBuilder(a, b); +} + +template <bool rc1, bool rc2> +inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b)); +} + +template <bool rc1, bool rc2> +inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return MultNodeBuilder(a, b); +} + +template <bool rc> +inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, + const AndNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, + const OrNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, + const AndNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, + const OrNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, + const PlusNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, + const MultNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, + const PlusNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, + const MultNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, + const PlusNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, + const MultNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { + return NodeManager::currentNM()->mkNode(kind::UMINUS, a); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__CONVENIENCE_NODE_BUILDERS_H */ diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 6dc9453d2..761dd6d24 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -1,12 +1,17 @@ /********************* */ -/** declaration_scope.cpp +/*! \file declaration_scope.cpp + ** \verbatim ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Convenience class for scoping variable and type declarations (implementation). ** ** Convenience class for scoping variable and type declarations (implementation) **/ diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index e33aa25fa..a6947c536 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -1,12 +1,17 @@ /********************* */ -/** context.h +/*! \file declaration_scope.h + ** \verbatim ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Convenience class for scoping variable and type declarations. ** ** Convenience class for scoping variable and type declarations. **/ diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index 38f8fc787..cb983b006 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -1,9 +1,21 @@ -/* - * expr_manager_scope.h - * - * Created on: Apr 7, 2010 - * Author: dejan - */ +/********************* */ +/*! \file expr_manager_scope.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__EXPR_MANAGER_SCOPE_H #define __CVC4__EXPR_MANAGER_SCOPE_H diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index bf0e2f96e..3eb2a8109 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1,5 +1,6 @@ /********************* */ -/** expr_manager_template.cpp +/*! \file expr_manager_template.cpp + ** \verbatim ** Original author: dejan ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression manager interface, implementation. ** ** Public-facing expression manager interface, implementation. **/ @@ -71,17 +74,6 @@ BitVectorType ExprManager::bitVectorType(unsigned size) const { return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size))); } -Expr ExprManager::mkExpr(Kind kind) { - const unsigned n = 0; - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkNodePtr(kind)); -} - Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { const unsigned n = 1; CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, @@ -252,7 +244,7 @@ Expr ExprManager::mkVar(const Type& type) { Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { - CheckArgument( metakind::isAssociative(kind), kind, + CheckArgument( kind::isAssociative(kind), kind, "Illegal kind in mkAssociative: %s", kind::kindToString(kind).c_str()); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 4cde091ac..707d9a26e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -1,14 +1,17 @@ /********************* */ -/** expr_manager_template.h +/*! \file expr_manager_template.h + ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking, cconway + ** Major contributors: cconway, mdeters + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression manager interface. ** ** Public-facing expression manager interface. **/ @@ -101,13 +104,6 @@ public: BitVectorType bitVectorType(unsigned size) const; /** - * Make a unary expression of a given kind (TRUE, FALSE,...). - * @param kind the kind of expression - * @return the expression - */ - Expr mkExpr(Kind kind); - - /** * Make a unary expression of a given kind (NOT, BVNOT, ...). * @param child1 kind the kind of expression * @return the expression diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index edd49f032..b4359cf2a 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -1,14 +1,17 @@ /********************* */ -/** expr_template.cpp +/*! \file expr_template.cpp + ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): cconway, taking + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression interface, implementation. ** ** Public-facing expression interface, implementation. **/ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 6597d5f14..73aa666e6 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -1,5 +1,6 @@ /********************* */ -/** expr_template.h +/*! \file expr_template.h + ** \verbatim ** Original author: dejan ** Major contributors: mdeters ** Minor contributors (to current version): cconway, taking @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression interface. ** ** Public-facing expression interface. **/ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 96c34a02a..718fd58f4 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -1,5 +1,6 @@ /********************* */ -/** kind_template.h +/*! \file kind_template.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Template for the Node kind header. ** ** Template for the Node kind header. **/ @@ -57,6 +60,23 @@ ${kind_printers} return out; } +/** Returns true if the given kind is associative. This is used by ExprManager to + * decide whether it's safe to modify big expressions by changing the grouping of + * the arguments. */ +/* TODO: This could be generated. */ +inline bool isAssociative(::CVC4::Kind k) { + switch(k) { + case kind::AND: + case kind::OR: + case kind::MULT: + case kind::PLUS: + return true; + + default: + return false; + } +} + inline std::string kindToString(::CVC4::Kind k) { std::stringstream ss; ss << k; diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index fc0910893..079199359 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -1,14 +1,17 @@ /********************* */ -/** metakind_template.h +/*! \file metakind_template.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Template for the metakind header. ** ** Template for the metakind header. **/ @@ -294,23 +297,6 @@ ${metakind_ubchildren} return ubs[k]; } -/** Returns true if the given kind is associative. This is used by ExprManager to - * decide whether it's safe to modify big expressions by changing the grouping of - * the arguments. */ -/* TODO: This could be generated. */ -inline bool isAssociative(::CVC4::Kind k) { - switch(k) { - case kind::AND: - case kind::OR: - case kind::MULT: - case kind::PLUS: - return true; - - default: - return false; - } -} - }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ }/* CVC4 namespace */ diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 7ebea8a70..2b6417e8a 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,14 +1,17 @@ /********************* */ -/** node.cpp +/*! \file node.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ diff --git a/src/expr/node.h b/src/expr/node.h index 0daa3f58c..cfaab142d 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1,14 +1,17 @@ /********************* */ -/** node.h +/*! \file node.h + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway, taking + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ @@ -138,8 +141,8 @@ class NodeTemplate { friend class NodeTemplate<false>; friend class NodeManager; - template <class Builder> - friend class NodeBuilderBase; + template <unsigned nchild_thresh> + friend class NodeBuilder; friend class ::CVC4::expr::attr::AttributeManager; diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 877c50d82..d81190d7a 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,14 +1,17 @@ /********************* */ -/** node_builder.h +/*! \file node_builder.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): taking, dejan + ** Major contributors: dejan + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A builder interface for Nodes. ** ** A builder interface for Nodes. ** @@ -101,12 +104,12 @@ ** returned in a Node wrapper. ** ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper - ** temporary for the NodeValue in the NodeBuilderBase<>::operator - ** Node() member function. If we create a temporary (for example by - ** writing Debug("builder") << Node(nv) << endl), the NodeValue will - ** have its reference count incremented from zero to one, then - ** decremented, which makes it eligible for collection before the - ** builder has even returned it! So this is a no-no. + ** temporary for the NodeValue in the NodeBuilder<>::operator Node() + ** member function. If we create a temporary (for example by writing + ** Debug("builder") << Node(nv) << endl), the NodeValue will have its + ** reference count incremented from zero to one, then decremented, + ** which makes it eligible for collection before the builder has even + ** returned it! So this is a no-no. ** ** There are also two cases when the NodeBuilder is clear()'ed: ** @@ -131,32 +134,10 @@ ** d_nv is deallocated. ** ** Regarding the backing store (typically on the stack): the file - ** below provides three classes (two of them are templates): - ** - ** template <class Builder> class NodeBuilderBase; - ** - ** This is the base class for node builders. It can not be used - ** directly. It contains a shared implementation but is intended - ** to be subclassed. Derived classes supply its "in-line" buffer. - ** - ** class BackedNodeBuilder; - ** - ** This is the usable form for a user-supplied-backing-store node - ** builder. A user can allocate a buffer large enough for a - ** NodeValue with N children (say, on the stack), then pass a - ** pointer to this buffer, and the parameter N, to a - ** BackedNodeBuilder. It will use this buffer to build its - ** NodeValue until the number of children exceeds N; then it will - ** allocate d_nv on the heap. - ** - ** To ensure that the buffer is properly-sized, it is recommended - ** to use the makeStackNodeBuilder(b, N) macro to make a - ** BackedNodeBuilder "b" with a stack-allocated buffer large - ** enough to hold N children. + ** below provides the template: ** ** template <unsigned nchild_thresh> class NodeBuilder; ** - ** This is the conceptually easiest form of NodeBuilder to use. ** The default: ** ** NodeBuilder<> b; @@ -164,9 +145,7 @@ ** gives you a backing buffer with capacity for 10 children in ** the same place as the NodeBuilder<> itself is allocated. You ** can specify another size as a template parameter, but it must - ** be a compile-time constant (which is why the BackedNodeBuilder - ** creator-macro "makeStackNodeBuilder(b, N)" is sometimes - ** preferred). + ** be a compile-time constant. **/ #include "cvc4_private.h" @@ -185,8 +164,8 @@ namespace CVC4 { static const unsigned default_nchild_thresh = 10; - template <class Builder> - class NodeBuilderBase; + template <unsigned nchild_thresh> + class NodeBuilder; class NodeManager; }/* CVC4 namespace */ @@ -199,38 +178,31 @@ namespace CVC4 { namespace CVC4 { -template <class Builder> -inline std::ostream& operator<<(std::ostream&, const NodeBuilderBase<Builder>&); +template <unsigned nchild_thresh> +inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&); +/* see expr/convenience_node_builders.h */ class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; class MultNodeBuilder; /** - * A base class for NodeBuilders. When extending this class, use: - * - * class MyExtendedNodeBuilder : - * public NodeBuilderBase<MyExtendedNodeBuilder> { ... }; - * - * This ensures that certain member functions return the right - * (derived) class type. - * - * There are no virtual functions here, and that should remain the - * case! This class is just used for sharing of implementation. Two - * types derive from it: BackedNodeBuilder (which allows for an - * external buffer), and the NodeBuilder<> template, which requires - * that you give it a compile-time constant backing-store size. + * The main template NodeBuilder. */ -template <class Builder> -class NodeBuilderBase { -protected: - +template <unsigned nchild_thresh = default_nchild_thresh> +class NodeBuilder { /** - * A reference to an "in-line" stack-allocated buffer for use by the + * An "in-line" stack-allocated buffer for use by the * NodeBuilder. */ - expr::NodeValue& d_inlineNv; + expr::NodeValue d_inlineNv; + /** + * Space for the children of the node being constructed. This is + * never accessed directly, but rather through + * d_inlineNv.d_children[i]. + */ + expr::NodeValue* d_inlineNvChildSpace[nchild_thresh]; /** * A pointer to the "current" NodeValue buffer; either &d_inlineNv @@ -242,16 +214,13 @@ protected: NodeManager* d_nm; /** - * The maximum number of children that can be held in this "in-line" - * buffer. - */ - const uint16_t d_inlineNvMaxChildren; - - /** * The number of children allocated in d_nv. */ uint16_t d_nvMaxChildren; + template <unsigned N> + void internalCopy(const NodeBuilder<N>& nb); + /** * Returns whether or not this NodeBuilder has been "used"---i.e., * whether a Node has been extracted with operator Node(). @@ -267,7 +236,7 @@ protected: inline void setUsed() { Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!"); Assert(d_inlineNv.d_nchildren == 0 && - d_nvMaxChildren == d_inlineNvMaxChildren, + d_nvMaxChildren == nchild_thresh, "Internal error: bad `inline' state in NodeBuilder!"); d_nv = NULL; } @@ -279,7 +248,7 @@ protected: inline void setUnused() { Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!"); Assert(d_inlineNv.d_nchildren == 0 && - d_nvMaxChildren == d_inlineNvMaxChildren, + d_nvMaxChildren == nchild_thresh, "Internal error: bad `inline' state in NodeBuilder!"); d_nv = &d_inlineNv; } @@ -377,7 +346,7 @@ protected: } } - Builder& collapseTo(Kind k) { + NodeBuilder<nchild_thresh>& collapseTo(Kind k) { AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, @@ -389,27 +358,98 @@ protected: d_nv->d_kind = expr::NodeValue::kindToDKind(k); return append(n); } - return static_cast<Builder&>(*this); + return *this; + } + +public: + + inline NodeBuilder() : + d_nv(&d_inlineNv), + d_nm(NodeManager::currentNM()), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_nchildren = 0; } -protected: + inline NodeBuilder(Kind k) : + d_nv(&d_inlineNv), + d_nm(NodeManager::currentNM()), + d_nvMaxChildren(nchild_thresh) { - inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, - Kind k = kind::UNDEFINED_KIND); - inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, - NodeManager* nm, Kind k = kind::UNDEFINED_KIND); + Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); -private: - // disallow copy or assignment of these base classes directly (there - // would be no backing store!) - NodeBuilderBase(const NodeBuilderBase& nb); - NodeBuilderBase& operator=(const NodeBuilderBase& nb); + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; + } -public: + inline NodeBuilder(NodeManager* nm) : + d_nv(&d_inlineNv), + d_nm(nm), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_nchildren = 0; + } + + inline NodeBuilder(NodeManager* nm, Kind k) : + d_nv(&d_inlineNv), + d_nm(nm), + d_nvMaxChildren(nchild_thresh) { + + Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); - // Intentionally not virtual; we don't want a vtable. Don't - // override this in a derived class. - inline ~NodeBuilderBase(); + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; + } + + inline ~NodeBuilder() { + if(EXPECT_FALSE( nvIsAllocated() )) { + dealloc(); + } else if(EXPECT_FALSE( !isUsed() )) { + decrRefCounts(); + } + } + + // These implementations are identical, but we need to have both of + // these because the templatized version isn't recognized as a + // generalization of a copy constructor (and a default copy + // constructor will be generated [?]) + inline NodeBuilder(const NodeBuilder& nb) : + d_nv(&d_inlineNv), + d_nm(nb.d_nm), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = nb.d_nv->d_kind; + d_inlineNv.d_nchildren = 0; + + internalCopy(nb); + } + + // technically this is a conversion, not a copy + template <unsigned N> + inline NodeBuilder(const NodeBuilder<N>& nb) : + d_nv(&d_inlineNv), + d_nm(nb.d_nm), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = nb.d_nv->d_kind; + d_inlineNv.d_nchildren = 0; + + internalCopy(nb); + } typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator; typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator; @@ -485,9 +525,9 @@ public: * allocated, and decrements the reference counts of any currently * children in the NodeBuilder. * - * This should leave the BackedNodeBuilder in the state it was after + * This should leave the NodeBuilder in the state it was after * initial construction, except for Kind, which is set to the - * argument (if provided), or UNDEFINED_KIND. In particular, the + * argument, if provided, or UNDEFINED_KIND. In particular, the * associated NodeManager is not affected by clear(). */ void clear(Kind k = kind::UNDEFINED_KIND); @@ -495,7 +535,7 @@ public: // "Stream" expression constructor syntax /** Set the Kind of this Node-under-construction. */ - inline Builder& operator<<(const Kind& k) { + inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() == kind::UNDEFINED_KIND, @@ -505,7 +545,7 @@ public: k < kind::LAST_KIND, k, "illegal node-building kind"); d_nv->d_kind = expr::NodeValue::kindToDKind(k); - return static_cast<Builder&>(*this); + return *this; } /** @@ -514,7 +554,7 @@ public: * FIXME: do we really want that collapse behavior? We had agreed * on it but then never wrote code like that. */ - Builder& operator<<(TNode n) { + NodeBuilder<nchild_thresh>& operator<<(TNode n) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); /* FIXME: disable this "collapsing" for now.. @@ -527,7 +567,7 @@ public: } /** Append a sequence of children to this TypeNode-under-construction. */ - inline Builder& + inline NodeBuilder<nchild_thresh>& append(const std::vector<TypeNode>& children) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); @@ -536,7 +576,7 @@ public: /** Append a sequence of children to this Node-under-construction. */ template <bool ref_count> - inline Builder& + inline NodeBuilder<nchild_thresh>& append(const std::vector<NodeTemplate<ref_count> >& children) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); @@ -545,17 +585,17 @@ public: /** Append a sequence of children to this Node-under-construction. */ template <class Iterator> - Builder& append(const Iterator& begin, const Iterator& end) { + NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); for(Iterator i = begin; i != end; ++i) { append(*i); } - return static_cast<Builder&>(*this); + return *this; } /** Append a child to this Node-under-construction. */ - Builder& append(TNode n) { + NodeBuilder<nchild_thresh>& append(TNode n) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node"); @@ -563,11 +603,11 @@ public: expr::NodeValue* nv = n.d_nv; nv->inc(); d_nv->d_children[d_nv->d_nchildren++] = nv; - return static_cast<Builder&>(*this); + return *this; } /** Append a child to this Node-under-construction. */ - Builder& append(const TypeNode& typeNode) { + NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node"); @@ -575,7 +615,7 @@ public: expr::NodeValue* nv = typeNode.d_nv; nv->inc(); d_nv->d_children[d_nv->d_nchildren++] = nv; - return static_cast<Builder&>(*this); + return *this; } private: @@ -609,592 +649,38 @@ public: d_nv->toStream(out, depth); } - Builder& operator&=(TNode); - Builder& operator|=(TNode); - Builder& operator+=(TNode); - Builder& operator-=(TNode); - Builder& operator*=(TNode); + NodeBuilder<nchild_thresh>& operator&=(TNode); + NodeBuilder<nchild_thresh>& operator|=(TNode); + NodeBuilder<nchild_thresh>& operator+=(TNode); + NodeBuilder<nchild_thresh>& operator-=(TNode); + NodeBuilder<nchild_thresh>& operator*=(TNode); friend class AndNodeBuilder; friend class OrNodeBuilder; friend class PlusNodeBuilder; friend class MultNodeBuilder; -};/* class NodeBuilderBase */ - -/** - * Backing-store interface version for NodeBuilders. To construct one - * of these, you need to create a backing store (preferably on the - * stack) for it to hold its "inline" NodeValue. There's a - * convenience macro defined below, makeStackNodeBuilder(b, N), - * defined below to define a stack-allocated BackedNodeBuilder "b" - * with room for N children on the stack. - */ -class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> { -public: - inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, Kind k) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - inline BackedNodeBuilder(expr::NodeValue* buf, - unsigned maxChildren, - NodeManager* nm) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - inline BackedNodeBuilder(expr::NodeValue* buf, - unsigned maxChildren, - NodeManager* nm, - Kind k) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - // we don't want a vtable, so do not declare a dtor! - //inline ~BackedNodeBuilder(); - -private: - // disallow copy or assignment (there would be no backing store!) - BackedNodeBuilder(const BackedNodeBuilder& nb); - BackedNodeBuilder& operator=(const BackedNodeBuilder& nb); - -};/* class BackedNodeBuilder */ - -/** - * Stack-allocate a BackedNodeBuilder with a stack-allocated backing - * store of size __n. The BackedNodeBuilder will be named __v. - * - * __v must be a simple name. __n must be convertible to size_t, and - * will be evaluated only once. This macro may only be used where - * declarations are permitted. - */ -#define makeStackNodeBuilder(__v, __n) \ - const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \ - ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v \ - [1 + ( ( ( sizeof(::CVC4::expr::NodeValue) + \ - sizeof(::CVC4::expr::NodeValue*) + 1 ) / \ - sizeof(::CVC4::expr::NodeValue*) ) * \ - __cvc4_backednodebuilder_nchildren__ ## __v)]; \ - ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \ - __cvc4_backednodebuilder_nchildren__ ## __v) -// IF THE ABOVE ASSERTION FAILS, write another compiler-specific -// version of makeStackNodeBuilder() that works for your compiler -// (even if it's suboptimal, ignoring its __n argument, and just -// creates a NodeBuilder<10>). - - -/** - * Simple NodeBuilder interface. This is a template that requires - * that the number of children of the "inline"-allocated NodeValue be - * specified as a template parameter (which means it must be a - * compile-time constant). - */ -template <unsigned nchild_thresh = default_nchild_thresh> -class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > { - // This is messy: - // 1. This (anonymous) struct here must be a POD to avoid the - // compiler laying out things in a different way. - // 2. The layout is engineered carefully. We can't just - // stack-allocate enough bytes as a char[] because we break - // strict-aliasing rules. The first thing in the struct is a - // "NodeValue" so a pointer to this struct should be safely - // castable to a pointer to a NodeValue (same alignment). - struct BackingStore { - expr::NodeValue n; - expr::NodeValue* c[nchild_thresh]; - } d_backingStore; - - typedef NodeBuilderBase<NodeBuilder<nchild_thresh> > super; - - template <unsigned N> - void internalCopy(const NodeBuilder<N>& nb); - -public: - inline NodeBuilder() : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh) { - } - - inline NodeBuilder(Kind k) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - k) { - } - - inline NodeBuilder(NodeManager* nm) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nm) { - } - - inline NodeBuilder(NodeManager* nm, Kind k) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nm, - k) { - } - - // These implementations are identical, but we need to have both of - // these because the templatized version isn't recognized as a - // generalization of a copy constructor (and a default copy - // constructor will be generated [?]) - inline NodeBuilder(const NodeBuilder& nb) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nb.d_nm, - nb.getKind()) { - internalCopy(nb); - } - - // technically this is a conversion, not a copy - template <unsigned N> - inline NodeBuilder(const NodeBuilder<N>& nb) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nb.d_nm, - nb.getKind()) { - internalCopy(nb); - } - - // we don't want a vtable, so do not declare a dtor! - //inline ~NodeBuilder(); - // This is needed for copy constructors of different sizes to access // private fields template <unsigned N> friend class NodeBuilder; - };/* class NodeBuilder<> */ +}/* CVC4 namespace */ + // TODO: add templatized NodeTemplate<ref_count> to all above and // below inlines for 'const [T]Node&' arguments? Technically a lot of // time is spent in the TNode conversion and copy constructor, but // this should be optimized into a simple pointer copy (?) // TODO: double-check this. -class AndNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::AND); - } - - inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) { - d_eb << a << b; - } - - template <bool rc> - inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&); - - template <bool rc> - inline OrNodeBuilder operator||(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class AndNodeBuilder */ - -class OrNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::OR); - } - - inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) { - d_eb << a << b; - } - - template <bool rc> - inline AndNodeBuilder operator&&(const NodeTemplate<rc>&); - - template <bool rc> - inline OrNodeBuilder& operator||(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class OrNodeBuilder */ - -class PlusNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::PLUS); - } - - inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) { - d_eb << a << b; - } - - template <bool rc> - inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&); - - template <bool rc> - inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&); - - template <bool rc> - inline MultNodeBuilder operator*(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class PlusNodeBuilder */ - -class MultNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::MULT); - } - - inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) { - d_eb << a << b; - } - - template <bool rc> - inline PlusNodeBuilder operator+(const NodeTemplate<rc>&); - - template <bool rc> - inline PlusNodeBuilder operator-(const NodeTemplate<rc>&); - - template <bool rc> - inline MultNodeBuilder& operator*(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class MultNodeBuilder */ - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator&=(TNode e) { - return collapseTo(kind::AND).append(e); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator|=(TNode e) { - return collapseTo(kind::OR).append(e); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) { - return collapseTo(kind::PLUS).append(e); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) { - return collapseTo(kind::PLUS). - append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator*=(TNode e) { - return collapseTo(kind::MULT).append(e); -} - -template <bool rc> -inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -template <bool rc> -inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) { - return OrNodeBuilder(Node(d_eb), n); -} - -inline AndNodeBuilder& operator&&(AndNodeBuilder& a, - const AndNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline AndNodeBuilder& operator&&(AndNodeBuilder& a, - const OrNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder operator||(AndNodeBuilder& a, - const AndNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder operator||(AndNodeBuilder& a, - const OrNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) { - return AndNodeBuilder(Node(d_eb), n); -} - -template <bool rc> -inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -inline AndNodeBuilder operator&&(OrNodeBuilder& a, - const AndNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline AndNodeBuilder operator&&(OrNodeBuilder& a, - const OrNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder& operator||(OrNodeBuilder& a, - const AndNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder& operator||(OrNodeBuilder& a, - const OrNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -template <bool rc> -inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) { - d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n)); - return *this; -} - -template <bool rc> -inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) { - return MultNodeBuilder(Node(d_eb), n); -} - -inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, - const PlusNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder operator*(PlusNodeBuilder& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder operator*(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { - return PlusNodeBuilder(Node(d_eb), n); -} - -template <bool rc> -inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) { - return PlusNodeBuilder(Node(d_eb), - NodeManager::currentNM()->mkNode(kind::UMINUS, n)); -} - -template <bool rc> -inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -inline PlusNodeBuilder operator+(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder operator+(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder operator-(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder operator-(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder& operator*(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder& operator*(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc1, bool rc2> -inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return AndNodeBuilder(a, b); -} - -template <bool rc1, bool rc2> -inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return OrNodeBuilder(a, b); -} - -template <bool rc1, bool rc2> -inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return PlusNodeBuilder(a, b); -} - -template <bool rc1, bool rc2> -inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b)); -} - -template <bool rc1, bool rc2> -inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return MultNodeBuilder(a, b); -} - -template <bool rc> -inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, - const AndNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, - const OrNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, - const AndNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, - const OrNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, - const MultNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, - const PlusNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, - const MultNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, - const MultNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { - return NodeManager::currentNM()->mkNode(kind::UMINUS, a); -} - -}/* CVC4 namespace */ - #include "expr/node.h" #include "expr/node_manager.h" namespace CVC4 { -template <class Builder> -inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, - unsigned maxChildren, - Kind k) : - d_inlineNv(*buf), - d_nv(&d_inlineNv), - d_nm(NodeManager::currentNM()), - d_inlineNvMaxChildren(maxChildren), - d_nvMaxChildren(maxChildren) { - - Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); - - d_inlineNv.d_id = 0; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - d_inlineNv.d_nchildren = 0; -} - -template <class Builder> -inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, - unsigned maxChildren, - NodeManager* nm, - Kind k) : - d_inlineNv(*buf), - d_nv(&d_inlineNv), - d_nm(nm), - d_inlineNvMaxChildren(maxChildren), - d_nvMaxChildren(maxChildren) { - - Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); - - d_inlineNv.d_id = 0; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - d_inlineNv.d_nchildren = 0; -} - -template <class Builder> -inline NodeBuilderBase<Builder>::~NodeBuilderBase() { - if(EXPECT_FALSE( nvIsAllocated() )) { - dealloc(); - } else if(EXPECT_FALSE( !isUsed() )) { - decrRefCounts(); - } -} - -template <class Builder> -void NodeBuilderBase<Builder>::clear(Kind k) { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::clear(Kind k) { Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind"); if(EXPECT_FALSE( nvIsAllocated() )) { @@ -1214,8 +700,8 @@ void NodeBuilderBase<Builder>::clear(Kind k) { d_inlineNv.d_nchildren = 0; } -template <class Builder> -void NodeBuilderBase<Builder>::realloc(size_t toSize) { +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!" ); @@ -1258,8 +744,8 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) { } } -template <class Builder> -void NodeBuilderBase<Builder>::dealloc() { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::dealloc() { Assert( nvIsAllocated(), "Internal error: NodeBuilder: dealloc() called without a " "private NodeBuilder-allocated buffer" ); @@ -1272,11 +758,11 @@ void NodeBuilderBase<Builder>::dealloc() { free(d_nv); d_nv = &d_inlineNv; - d_nvMaxChildren = d_inlineNvMaxChildren; + d_nvMaxChildren = nchild_thresh; } -template <class Builder> -void NodeBuilderBase<Builder>::decrRefCounts() { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::decrRefCounts() { Assert( !nvIsAllocated(), "Internal error: NodeBuilder: decrRefCounts() called with a " "private NodeBuilder-allocated buffer" ); @@ -1291,48 +777,48 @@ void NodeBuilderBase<Builder>::decrRefCounts() { } -template <class Builder> -TypeNode NodeBuilderBase<Builder>::constructTypeNode() { +template <unsigned nchild_thresh> +TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() { return TypeNode(constructNV()); } -template <class Builder> -TypeNode NodeBuilderBase<Builder>::constructTypeNode() const { +template <unsigned nchild_thresh> +TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const { return TypeNode(constructNV()); } -template <class Builder> -Node NodeBuilderBase<Builder>::constructNode() { +template <unsigned nchild_thresh> +Node NodeBuilder<nchild_thresh>::constructNode() { return Node(constructNV()); } -template <class Builder> -Node NodeBuilderBase<Builder>::constructNode() const { +template <unsigned nchild_thresh> +Node NodeBuilder<nchild_thresh>::constructNode() const { return Node(constructNV()); } -template <class Builder> -Node* NodeBuilderBase<Builder>::constructNodePtr() { +template <unsigned nchild_thresh> +Node* NodeBuilder<nchild_thresh>::constructNodePtr() { return new Node(constructNV()); } -template <class Builder> -Node* NodeBuilderBase<Builder>::constructNodePtr() const { +template <unsigned nchild_thresh> +Node* NodeBuilder<nchild_thresh>::constructNodePtr() const { return new Node(constructNV()); } -template <class Builder> -NodeBuilderBase<Builder>::operator Node() { +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator Node() { return constructNode(); } -template <class Builder> -NodeBuilderBase<Builder>::operator Node() const { +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator Node() const { return constructNode(); } -template <class Builder> -expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { +template <unsigned nchild_thresh> +expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() != kind::UNDEFINED_KIND, @@ -1396,7 +882,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { if(EXPECT_TRUE( ! nvIsAllocated() )) { /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** supplied by the user (or derived class) **/ + ** allocated "inline" in this NodeBuilder. **/ // Lookup the expression value in the pool we already have expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); @@ -1490,7 +976,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { expr::NodeValue* nv = d_nv; nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading d_nv = &d_inlineNv; - d_nvMaxChildren = d_inlineNvMaxChildren; + d_nvMaxChildren = nchild_thresh; setUsed(); //poolNv = nv; @@ -1503,8 +989,8 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { } // CONST VERSION OF NODE EXTRACTOR -template <class Builder> -expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const { +template <unsigned nchild_thresh> +expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() != kind::UNDEFINED_KIND, @@ -1567,7 +1053,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const { if(EXPECT_TRUE( ! nvIsAllocated() )) { /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** supplied by the user (or derived class) **/ + ** allocated "inline" in this NodeBuilder. **/ // Lookup the expression value in the pool we already have expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); @@ -1683,30 +1169,30 @@ template <unsigned nchild_thresh> template <unsigned N> void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { if(nb.isUsed()) { - super::setUsed(); + setUsed(); return; } - if(nb.d_nvMaxChildren > super::d_nvMaxChildren) { - super::realloc(nb.d_nvMaxChildren); + if(nb.d_nvMaxChildren > d_nvMaxChildren) { + realloc(nb.d_nvMaxChildren); } std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), - super::d_nv->nv_begin()); + d_nv->nv_begin()); - super::d_nv->d_nchildren = nb.d_nv->d_nchildren; + d_nv->d_nchildren = nb.d_nv->d_nchildren; - for(expr::NodeValue::nv_iterator i = super::d_nv->nv_begin(); - i != super::d_nv->nv_end(); + for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); + i != d_nv->nv_end(); ++i) { (*i)->inc(); } } -template <class Builder> +template <unsigned nchild_thresh> inline std::ostream& operator<<(std::ostream& out, - const NodeBuilderBase<Builder>& b) { + const NodeBuilder<nchild_thresh>& b) { b.toStream(out, Node::setdepth::getDepth(out)); return out; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a1b5b771f..247348497 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,14 +1,17 @@ /********************* */ -/** node_manager.cpp +/*! \file node_manager.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan, taking + ** Major contributors: dejan + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Expression manager implementation. ** ** Expression manager implementation. ** diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5642a8372..2d96ac57a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,14 +1,17 @@ /********************* */ -/** node_manager.h +/*! \file node_manager.h + ** \verbatim ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): taking, dejan + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A manager for Nodes. ** ** A manager for Nodes. ** @@ -50,7 +53,7 @@ typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; }/* CVC4::expr namespace */ class NodeManager { - template <class Builder> friend class CVC4::NodeBuilderBase; + template <unsigned nchild_thresh> friend class CVC4::NodeBuilder; friend class NodeManagerScope; friend class expr::NodeValue; @@ -262,10 +265,6 @@ public: // general expression-builders - /** Create a node with no children. */ - Node mkNode(Kind kind); - Node* mkNodePtr(Kind kind); - /** Create a node with one child. */ Node mkNode(Kind kind, TNode child1); Node* mkNodePtr(Kind kind, TNode child1); @@ -740,15 +739,6 @@ inline TypeNode NodeManager::mkSort(const std::string& name) { return type; } -inline Node NodeManager::mkNode(Kind kind) { - return NodeBuilder<0>(this, kind); -} - -inline Node* NodeManager::mkNodePtr(Kind kind) { - NodeBuilder<0> nb(this, kind); - return nb.constructNodePtr(); -} - inline Node NodeManager::mkNode(Kind kind, TNode child1) { return NodeBuilder<1>(this, kind) << child1; } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 101be5187..c64a608fb 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -1,5 +1,6 @@ /********************* */ -/** node_value.cpp +/*! \file node_value.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): cconway @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An expression node. ** ** An expression node. ** diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 260a9daae..8b2056560 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,6 @@ /********************* */ -/** node_value.h +/*! \file node_value.h + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): cconway, taking @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An expression node. ** ** An expression node. ** @@ -35,7 +38,6 @@ namespace CVC4 { template <bool ref_count> class NodeTemplate; class TypeNode; -template <class Builder> class NodeBuilderBase; template <unsigned N> class NodeBuilder; class AndNodeBuilder; class OrNodeBuilder; @@ -103,7 +105,6 @@ class NodeValue { template <bool> friend class ::CVC4::NodeTemplate; friend class ::CVC4::TypeNode; - template <class Builder> friend class ::CVC4::NodeBuilderBase; template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder; friend class ::CVC4::NodeManager; diff --git a/src/expr/type.cpp b/src/expr/type.cpp index af333f9d3..3bacb4792 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -1,14 +1,17 @@ /********************* */ -/** type.cpp +/*! \file type.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of expression types . ** ** Implementation of expression types **/ diff --git a/src/expr/type.h b/src/expr/type.h index 137dbfff3..2d18c2fc8 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -1,14 +1,17 @@ /********************* */ -/** type.h +/*! \file type.h + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Interface for expression types. ** ** Interface for expression types **/ diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h index a847bc827..0f5b522b6 100644 --- a/src/expr/type_constant.h +++ b/src/expr/type_constant.h @@ -1,13 +1,17 @@ /********************* */ -/** type_constant.h +/*! \file type_constant.h + ** \verbatim ** Original author: dejan + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Interface for expression types. ** ** Interface for expression types **/ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 821349b45..1afaf2b89 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -1,14 +1,17 @@ /********************* */ -/** node.cpp +/*! \file type_node.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index f7b1a6b9e..9b67c674c 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1,12 +1,17 @@ /********************* */ -/** type_node.h +/*! \file type_node.h + ** \verbatim ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ @@ -62,8 +67,8 @@ class TypeNode { friend class NodeManager; - template <class Builder> - friend class NodeBuilderBase; + template <unsigned nchild_thresh> + friend class NodeBuilder; /** * Assigns the expression value and does reference counting. No assumptions diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h index 298bb14fb..77cadf0ea 100644 --- a/src/include/cvc4_private.h +++ b/src/include/cvc4_private.h @@ -1,5 +1,6 @@ /********************* */ -/** cvc4_private.h +/*! \file cvc4_private.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief #inclusion of this file marks a header as private and generates a + ** warning when the file is included improperly. ** ** #inclusion of this file marks a header as private and generates a ** warning when the file is included improperly. diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 4de3faf4c..e1b515ba5 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -1,5 +1,6 @@ /********************* */ -/** cvc4_public.h +/*! \file cvc4_public.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Macros that should be defined everywhere during the building of + ** the libraries and driver binary, and also exported to the user. ** ** Macros that should be defined everywhere during the building of ** the libraries and driver binary, and also exported to the user. diff --git a/src/include/cvc4parser_private.h b/src/include/cvc4parser_private.h index 5960b5c61..cb6e486d8 100644 --- a/src/include/cvc4parser_private.h +++ b/src/include/cvc4parser_private.h @@ -1,5 +1,6 @@ /********************* */ -/** cvc4parser_private.h +/*! \file cvc4parser_private.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief #inclusion of this file marks a header as private and generates a + ** warning when the file is included improperly. ** ** #inclusion of this file marks a header as private and generates a ** warning when the file is included improperly. diff --git a/src/include/cvc4parser_public.h b/src/include/cvc4parser_public.h index ec0f3a064..a60d281bb 100644 --- a/src/include/cvc4parser_public.h +++ b/src/include/cvc4parser_public.h @@ -1,5 +1,6 @@ /********************* */ -/** cvc4parser_public.h +/*! \file cvc4parser_public.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Macros that should be defined everywhere during the building of + ** the libraries and driver binary, and also exported to the user. ** ** Macros that should be defined everywhere during the building of ** the libraries and driver binary, and also exported to the user. diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index fda0bf766..c3c57cf94 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -1,14 +1,17 @@ /********************* */ -/** getopt.cpp +/*! \file getopt.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan, barrett, cconway + ** Major contributors: cconway + ** Minor contributors (to current version): dejan, barrett ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Contains code for handling command-line options. ** ** Contains code for handling command-line options **/ diff --git a/src/main/main.cpp b/src/main/main.cpp index 5150d32f9..7fb0d92c9 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -1,14 +1,17 @@ /********************* */ -/** main.cpp +/*! \file main.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan, barrett, cconway + ** Major contributors: cconway + ** Minor contributors (to current version): barrett, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Main driver for CVC4 executable. ** ** Main driver for CVC4 executable. **/ diff --git a/src/main/main.h b/src/main/main.h index 117b52c17..d56684d7d 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -1,5 +1,6 @@ /********************* */ -/** main.h +/*! \file main.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): dejan, barrett @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Header for main CVC4 driver. ** ** Header for main CVC4 driver. **/ diff --git a/src/main/usage.h b/src/main/usage.h index 4c600759f..4da37749b 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -1,14 +1,17 @@ /********************* */ -/** usage.h +/*! \file usage.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): cconway + ** Major contributors: cconway + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The "usage" string for the CVC4 driver binary. ** ** The "usage" string for the CVC4 driver binary. **/ diff --git a/src/main/util.cpp b/src/main/util.cpp index 6a69252ce..77274d575 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -1,5 +1,6 @@ /********************* */ -/** util.cpp +/*! \file util.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Utilities for the main driver. ** ** Utilities for the main driver. **/ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 9d75dd31f..fdaa83b04 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -1,5 +1,6 @@ /********************* */ -/** input.cpp +/*! \file antlr_input.cpp + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A super-class for ANTLR-generated input language parsers. ** ** A super-class for ANTLR-generated input language parsers **/ diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 642dc9654..d2d885ce0 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -1,14 +1,17 @@ /********************* */ -/** input.h +/*! \file antlr_input.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Base for ANTLR parser classes. ** ** Base for ANTLR parser classes. **/ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index d25d7b66b..b647842fa 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file antlr_input_imports.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + /* * The functions in this file are based on implementations in libantlr3c, * with only minor CVC4-specific changes. diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 53b56dcdd..adc0505db 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -1,14 +1,17 @@ /********************* */ -/** bounded_token_buffer.h +/*! \file bounded_token_buffer.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token stream implementation. ** ** An ANTLR3 bounded token stream implementation. ** This code is largely based on the original token buffer implementation diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h index 663e5b403..9634f016b 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -1,14 +1,17 @@ /********************* */ -/** bounded_token_buffer.h +/*! \file bounded_token_buffer.h + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token stream. ** ** An ANTLR3 bounded token stream. The stream has a bounded ** lookahead/behind k. Calling LT(i) with i > k or i < -k will raise diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index c9f9b66e7..5f42f0f29 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -1,14 +1,17 @@ /********************* */ -/** bounded_token_factory.cpp +/*! \file bounded_token_factory.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token factory implementation. ** ** An ANTLR3 bounded token factory implementation. **/ diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index faf289ef4..4d510c9e3 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -1,5 +1,6 @@ /********************* */ -/** bounded_token_factory.h +/*! \file bounded_token_factory.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token factory. ** ** An ANTLR3 bounded token factory. The factory has a fixed number of ** tokens that are re-used as parsing proceeds. Only use this factory diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index a53604efa..0f44e692a 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1,14 +1,17 @@ /* ******************* */ -/* Cvc.g +/*! \file Cvc.g + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Parser for CVC-LIB input language. ** ** Parser for CVC-LIB input language. **/ diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 4a8551a7a..2b99f9a87 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** cvc_input.cpp +/*! \file cvc_input.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 82c31813b..64c6beea7 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -1,14 +1,17 @@ /********************* */ -/** cvc_input.h +/*! \file cvc_input.h + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index a900765b5..2c4671b93 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** input.cpp - ** Original author: cconway - ** Major contributors: none +/*! \file input.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A super-class for input language parsers. ** ** A super-class for input language parsers **/ diff --git a/src/parser/input.h b/src/parser/input.h index 926ebe156..ceec1c8bd 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -1,14 +1,17 @@ /********************* */ -/** input.h +/*! \file input.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Base for parser inputs. ** ** Base for parser inputs. **/ diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index a87ba9cf8..7748a1cca 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -1,14 +1,17 @@ /********************* */ -/** memory_mapped_input_buffer.cpp +/*! \file memory_mapped_input_buffer.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index c63ec5407..18618a090 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -1,5 +1,6 @@ /********************* */ -/** memory_mapped_input_buffer.h +/*! \file memory_mapped_input_buffer.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief ANTLR input buffer from a memory-mapped file. ** ** ANTLR input buffer from a memory-mapped file. **/ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 286867e84..2bad12e2c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,14 +1,17 @@ /********************* */ -/** parser.cpp - ** Original author: cconway - ** Major contributors: dejan, mdeters +/*! \file parser.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Parser state implementation. ** ** Parser state implementation. **/ diff --git a/src/parser/parser.h b/src/parser/parser.h index e6e5a2250..3e10f632f 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -1,14 +1,17 @@ /********************* */ -/** parser.h +/*! \file parser.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A collection of state for use by parser implementations. ** ** A collection of state for use by parser implementations. **/ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 4e4b0309f..3b62cbc57 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -1,5 +1,6 @@ /********************* */ -/** parser_builder.cpp +/*! \file parser_builder.cpp + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A builder for parsers. ** ** A builder for parsers. **/ diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 92b44a82d..ed1ab807b 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -1,5 +1,6 @@ /********************* */ -/** parser_builder.h +/*! \file parser_builder.h + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A builder for parsers. ** ** A builder for parsers. **/ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index dfca01ce2..2ae38622d 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -1,5 +1,6 @@ /********************* */ -/** parser_exception.h +/*! \file parser_exception.h + ** \verbatim ** Original author: mdeters ** Major contributors: cconway ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Exception class for parse errors. ** ** Exception class for parse errors. **/ diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h index 51d28e51d..85994c52c 100644 --- a/src/parser/parser_options.h +++ b/src/parser/parser_options.h @@ -1,5 +1,6 @@ /********************* */ -/** parser_options.h +/*! \file parser_options.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index c11f350a6..4247dba7a 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -1,14 +1,17 @@ /* ******************* */ -/* Smt.g +/*! \file Smt.g + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Parser for SMT-LIB input language. ** ** Parser for SMT-LIB input language. **/ @@ -60,7 +63,6 @@ namespace CVC4 { @parser::postinclude { #include "expr/expr.h" #include "expr/kind.h" -#include "expr/metakind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" @@ -171,7 +173,7 @@ annotatedFormula[CVC4::Expr& expr] /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::metakind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index 7c8bf19dd..c19eca080 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** smt_input.cpp +/*! \file smt_input.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 1d3f87668..42581ec1c 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -1,5 +1,6 @@ /********************* */ -/** smt_input.h +/*! \file smt_input.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 11ce111a6..37612901e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1,14 +1,17 @@ /* ******************* */ -/* Smt2.g +/*! \file Smt2.g + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): mdeters, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Parser for SMT-LIB v2 input language. ** ** Parser for SMT-LIB v2 input language. **/ @@ -74,7 +77,6 @@ namespace CVC4 { @parser::postinclude { #include "expr/expr.h" #include "expr/kind.h" -#include "expr/metakind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" @@ -210,7 +212,7 @@ term[CVC4::Expr& expr] /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::metakind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 5cf902260..2776bff7e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1,14 +1,17 @@ /********************* */ -/** smt2.h +/*! \file smt2.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Definitions of SMT2 constants. ** ** Definitions of SMT2 constants. **/ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 0e057db68..b54fe82e9 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -1,14 +1,17 @@ /********************* */ -/** smt2.h +/*! \file smt2.h + ** \verbatim ** Original author: cconway - ** Major contributors: + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Definitions of SMT2 constants. ** ** Definitions of SMT2 constants. **/ diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 5150ba010..829d6a5f8 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** smt2_input.cpp +/*! \file smt2_input.cpp + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 962e2a987..1fa8cff1c 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -1,14 +1,17 @@ /********************* */ -/** smt2_input.h +/*! \file smt2_input.h + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 225f95d54..45f7ab398 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -1,14 +1,18 @@ /********************* */ -/** cnf_stream.cpp +/*! \file cnf_stream.cpp + ** \verbatim ** Original author: taking ** Major contributors: dejan - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): mdeters, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A CNF converter that takes in asserts and has the side effect + ** of given an equisatisfiable stream of assertions to PropEngine. ** ** A CNF converter that takes in asserts and has the side effect ** of given an equisatisfiable stream of assertions to PropEngine. diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index ce6c7eb1e..abb69f590 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -1,14 +1,17 @@ /********************* */ -/** cnf_stream.h +/*! \file cnf_stream.h + ** \verbatim ** Original author: taking - ** Major contributors: dejan - ** Minor contributors (to current version): cconway, mdeters + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief This class transforms a sequence of formulas into clauses. ** ** This class takes a sequence of formulas. ** It outputs a stream of clauses that is propositionally diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 16881f9e4..7cccca177 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,15 +1,19 @@ /********************* */ -/** prop_engine.cpp +/*! \file prop_engine.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan + ** Major contributors: cconway, dejan ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim ** + ** \brief Implementation of the propositional engine of CVC4. + ** + ** Implementation of the propositional engine of CVC4. **/ #include "cnf_stream.h" diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 7d3656a32..4adaa1434 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,14 +1,18 @@ /********************* */ -/** prop_engine.h +/*! \file prop_engine.h + ** \verbatim ** Original author: mdeters ** Major contributors: taking, dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The PropEngine (proposiitonal engine); main interface point + ** between CVC4's SMT infrastructure and the SAT solver. ** ** The PropEngine (proposiitonal engine); main interface point ** between CVC4's SMT infrastructure and the SAT solver. diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index df6eead4c..207bda4db 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file sat.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cnf_stream.h" #include "prop_engine.h" #include "sat.h" diff --git a/src/prop/sat.h b/src/prop/sat.h index f9d27d2ac..e023410c7 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -1,14 +1,17 @@ /********************* */ -/** sat.h +/*! \file sat.h + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Major contributors: dejan, cconway + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief SAT Solver. ** ** SAT Solver. **/ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3b003846c..37f6f0657 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1,5 +1,6 @@ /********************* */ -/** smt_engine.cpp +/*! \file smt_engine.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The main entry point into the CVC4 library's SMT interface. ** ** The main entry point into the CVC4 library's SMT interface. **/ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index cca765b84..b5807852b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,5 +1,6 @@ /********************* */ -/** smt_engine.h +/*! \file smt_engine.h + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief SmtEngine: the main public entry point of libcvc4. ** ** SmtEngine: the main public entry point of libcvc4. **/ diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h index 775db3ae0..c34e86191 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_constants.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 312e1c6ea..19980cd20 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_rewriter.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 6388c7031..704b57ca6 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_rewriter.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "util/rational.h" diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 297def3c7..dcfedb7e8 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -1,10 +1,25 @@ - - +/********************* */ +/*! \file arith_utilities.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H - #include "util/rational.h" #include "expr/node.h" diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h index 0f1cb07dc..963f2b969 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/basic.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file basic.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "expr/attribute.h" diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 0c94b1d08..55e6b3dc9 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file delta_rational.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/delta_rational.h" diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 4b6e06bc5..c37c65241 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file delta_rational.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #include "util/integer.h" diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h index 0dbd7355a..12b2a5e71 100644 --- a/src/theory/arith/normal.h +++ b/src/theory/arith/normal.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file normal.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #ifndef __CVC4__THEORY__ARITH__NORMAL_H #define __CVC4__THEORY__ARITH__NORMAL_H diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 33c690276..2d65f0640 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file partial_model.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/partial_model.h" #include "util/output.h" diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 57996a510..36567e86e 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file partial_model.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "context/context.h" #include "context/cdmap.h" diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h index 37595fda5..5cf391e64 100644 --- a/src/theory/arith/slack.h +++ b/src/theory/arith/slack.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file slack.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + namespace CVC4 { namespace theory { diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 76d8aa4f3..e43b48c66 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file tableau.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "expr/attribute.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3ca3245dd..e99a3e823 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_arith.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "expr/kind.h" #include "expr/metakind.h" diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ade63b6c9..c6b555bf8 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_arith.h +/*! \file theory_arith.h + ** \verbatim ** Original author: mdeters ** Major contributors: taking ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Arithmetic theory. ** ** Arithmetic theory. **/ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index b21ed0d6f..a995f90af 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_arith_type_rules.cpp +/*! \file theory_arith_type_rules.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none ** This file is part of the CVC4 prototype. @@ -7,7 +8,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add brief comments here ]] + ** + ** [[ Add file-specific comments here ]] **/ #include "cvc4_private.h" diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 2f62aacd7..6ab0fac90 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_arrays.h +/*! \file theory_arrays.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Theory of arrays. ** ** Theory of arrays. **/ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index b39663449..83effa005 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -1,14 +1,17 @@ /********************* */ -/** theory_bool.h +/*! \file theory_bool.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The theory of booleans. ** ** The theory of booleans. **/ diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 95d0f3bf6..8843a38c1 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_bool_type_rules.cpp +/*! \file theory_bool_type_rules.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none ** This file is part of the CVC4 prototype. @@ -7,7 +8,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add brief comments here ]] + ** + ** [[ Add file-specific comments here ]] **/ #include "cvc4_private.h" diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a859291a7..dc29183ea 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_bv.h +/*! \file theory_bv.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Bitvector theory. ** ** Bitvector theory. **/ diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 9c245b67a..142c9c963 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_bv_types.h +/*! \file theory_bv_type_rules.h + ** \verbatim ** Original author: dejan ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Bitvector theory. ** ** Bitvector theory. **/ diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index 00afd3b2b..616d3da74 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -1,5 +1,6 @@ /********************* */ -/** interrupted.h +/*! \file interrupted.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The theory output channel interface. ** ** The theory output channel interface. **/ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 08a3353e6..42d68efe5 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -1,14 +1,17 @@ /********************* */ -/** output_channel.h +/*! \file output_channel.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The theory output channel interface. ** ** The theory output channel interface. **/ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index d4bd717be..e06c9594c 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -1,5 +1,6 @@ /********************* */ -/** theory.cpp +/*! \file theory.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Base for theory interface. ** ** Base for theory interface. **/ diff --git a/src/theory/theory.h b/src/theory/theory.h index 2fcac86b0..bdd695cdd 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -1,5 +1,6 @@ /********************* */ -/** theory.h +/*! \file theory.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): dejan, taking @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Base of the theory interface. ** ** Base of the theory interface. **/ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9af4fc572..9dfaed68b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1,14 +1,17 @@ /********************* */ -/** theory_engine.cpp +/*! \file theory_engine.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The theory engine. ** ** The theory engine. **/ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 63d7a299f..1912cb026 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -1,14 +1,17 @@ /********************* */ -/** theory_engine.h +/*! \file theory_engine.h + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Major contributors: taking, dejan + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The theory engine. ** ** The theory engine. **/ diff --git a/src/theory/theoryof_table_template.h b/src/theory/theoryof_table_template.h index 465c4ee6d..e0d6fc8c8 100644 --- a/src/theory/theoryof_table_template.h +++ b/src/theory/theoryof_table_template.h @@ -1,5 +1,6 @@ /********************* */ -/** theoryof_table_template.h +/*! \file theoryof_table_template.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief The template for the automatically-generated theoryOf table. ** ** The template for the automatically-generated theoryOf table. ** See the mktheoryof script. diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp index 244605476..822f3a95b 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/ecdata.cpp @@ -1,5 +1,6 @@ /********************* */ -/** ecdata.cpp +/*! \file ecdata.cpp + ** \verbatim ** Original author: taking ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of equivalence class data for UF theory. ** ** Implementation of equivalence class data for UF theory. This is a ** context-dependent object. diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index bfc7eab8e..bff0a67a2 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -1,14 +1,17 @@ /********************* */ -/** ecdata.h +/*! \file ecdata.h + ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Context dependent equivalence class datastructure for nodes. ** ** Context dependent equivalence class datastructure for nodes. ** Currently keeps a context dependent watch list. diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1f09ce81d..d13baf6a9 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -1,14 +1,17 @@ /********************* */ -/** theory_uf.cpp +/*! \file theory_uf.cpp + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): cconway, dejan + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of the theory of uninterpreted functions. ** ** Implementation of the theory of uninterpreted functions. **/ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index be08cfee7..5add2e92a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,14 +1,18 @@ /********************* */ -/** theory_uf.h +/*! \file theory_uf.h + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. ** ** This is a basic implementation of the Theory of Uninterpreted Functions ** with Equality. It is based on the Nelson-Oppen algorithm given in diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 4028c3022..33123cd8f 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_uf_type_rules.h +/*! \file theory_uf_type_rules.h + ** \verbatim ** Original author: dejan ** Major contributors: none ** This file is part of the CVC4 prototype. @@ -7,7 +8,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add brief comments here ]] + ** + ** [[ Add file-specific comments here ]] **/ #include "cvc4_private.h" diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 1611f28d3..dbf292108 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -1,5 +1,6 @@ /********************* */ -/** Assert.cpp +/*! \file Assert.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Assertion utility classes, functions, and exceptions. ** ** Assertion utility classes, functions, and exceptions. Implementation. **/ diff --git a/src/util/Assert.h b/src/util/Assert.h index 744782ba2..5333817aa 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -1,5 +1,6 @@ /********************* */ -/** Assert.h +/*! \file Assert.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Assertion utility classes, functions, exceptions, and macros. ** ** Assertion utility classes, functions, exceptions, and macros. **/ diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 125065118..f789313b8 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -1,9 +1,21 @@ -/* - * bitvector.cpp - * - * Created on: Apr 5, 2010 - * Author: dejan - */ +/********************* */ +/*! \file bitvector.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #include "bitvector.h" diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 4f6038a81..e3ba969ec 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -1,9 +1,21 @@ -/* - * bitvector.h - * - * Created on: Mar 31, 2010 - * Author: dejan - */ +/********************* */ +/*! \file bitvector.h + ** \verbatim + ** Original author: dejan + ** Major contributors: cconway + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__BITVECTOR_H_ #define __CVC4__BITVECTOR_H_ diff --git a/src/util/bool.h b/src/util/bool.h index edd45b8a0..d2a29c8d5 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -1,5 +1,6 @@ /********************* */ -/** bool.h +/*! \file bool.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multiprecision rational constant. ** ** A multiprecision rational constant. ** This stores the rational as a pair of multiprecision integers, diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 5ed13a139..2a7563f82 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -1,5 +1,6 @@ /********************* */ -/** configuration.cpp +/*! \file configuration.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of Configuration class, which provides compile-time + ** configuration information about the CVC4 library. ** ** Implementation of Configuration class, which provides compile-time ** configuration information about the CVC4 library. diff --git a/src/util/configuration.h b/src/util/configuration.h index f939d8981..00651202d 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -1,5 +1,6 @@ /********************* */ -/** configuration.h +/*! \file configuration.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Interface to a public class that provides compile-time information + ** about the CVC4 library. ** ** Interface to a public class that provides compile-time information ** about the CVC4 library. diff --git a/src/util/debug.h b/src/util/debug.h index a99652661..4fc5d5caa 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -1,5 +1,6 @@ /********************* */ -/** debug.h +/*! \file debug.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Debugging things. ** ** Debugging things. ** diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index 06ea283a8..1ef2440c9 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -1,5 +1,6 @@ /********************* */ -/** decision_engine.cpp +/*! \file decision_engine.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief . ** **/ diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 84ace55b2..e1d9e21b7 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -1,5 +1,6 @@ /********************* */ -/** decision_engine.h +/*! \file decision_engine.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A decision engine for CVC4. ** ** A decision engine for CVC4. **/ diff --git a/src/util/exception.h b/src/util/exception.h index 48dcf1244..4893bd3c2 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -1,14 +1,17 @@ /********************* */ -/** exception.h +/*! \file exception.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief CVC4's exception base class and some associated utilities. ** ** CVC4's exception base class and some associated utilities. **/ diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 1849974cd..de237b793 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -1,9 +1,21 @@ -/* - * gmp.h - * - * Created on: Apr 5, 2010 - * Author: dejan - */ +/********************* */ +/*! \file gmp_util.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__GMP_H_ #define __CVC4__GMP_H_ diff --git a/src/util/hash.h b/src/util/hash.h index c72fe47e8..708628c24 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -1,9 +1,21 @@ -/* - * hash.h - * - * Created on: May 8, 2010 - * Author: chris - */ +/********************* */ +/*! \file hash.h + ** \verbatim + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__HASH_H_ #define __CVC4__HASH_H_ diff --git a/src/util/integer.cpp b/src/util/integer.cpp index a26f2108f..85075fd39 100644 --- a/src/util/integer.cpp +++ b/src/util/integer.cpp @@ -1,14 +1,17 @@ /********************* */ -/** integer.cpp +/*! \file integer.cpp + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multiprecision rational constant. ** ** A multiprecision rational constant. ** This stores the rational as a pair of multiprecision integers, diff --git a/src/util/integer.h b/src/util/integer.h index 41582d8db..d1921f597 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -1,14 +1,17 @@ /********************* */ -/** integer.h +/*! \file integer.h + ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): dejan, cconway, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multiprecision integer constant. ** ** A multiprecision integer constant. **/ diff --git a/src/util/model.h b/src/util/model.h index f807ff963..31fed1f31 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -1,5 +1,6 @@ /********************* */ -/** model.h +/*! \file model.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A model. ** ** A model. **/ diff --git a/src/util/options.h b/src/util/options.h index c7a730b14..7fcf35f00 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,5 +1,6 @@ /********************* */ -/** options.h +/*! \file options.h + ** \verbatim ** Original author: mdeters ** Major contributors: cconway ** Minor contributors (to current version): dejan @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Global (command-line or equivalent) tuning parameters. ** ** Global (command-line or equivalent) tuning parameters. **/ diff --git a/src/util/output.cpp b/src/util/output.cpp index 5d09e1d93..501ef52fd 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -1,5 +1,6 @@ /********************* */ -/** output.cpp +/*! \file output.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Output utility classes and functions. ** ** Output utility classes and functions. **/ diff --git a/src/util/output.h b/src/util/output.h index ea96606cb..f27ec24da 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -1,14 +1,17 @@ /********************* */ -/** output.h +/*! \file output.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Output utility classes and functions. ** ** Output utility classes and functions. **/ diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 5e9141758..beaa184bb 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -1,14 +1,17 @@ /********************* */ -/** rational.cpp +/*! \file rational.cpp + ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multi-precision rational constant. ** ** A multi-precision rational constant. **/ diff --git a/src/util/rational.h b/src/util/rational.h index 8218984a7..5e187de7f 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -1,14 +1,17 @@ /********************* */ -/** rational.h +/*! \file rational.h + ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: cconway + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Multi-precision rational constants. ** ** Multi-precision rational constants. **/ diff --git a/src/util/result.h b/src/util/result.h index 679e68763..e76e5605b 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -1,5 +1,6 @@ /********************* */ -/** result.h +/*! \file result.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Encapsulation of the result of a query. ** ** Encapsulation of the result of a query. **/ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index cf9298c4e..f00343729 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -1,5 +1,6 @@ /********************* */ -/** sexpr.cpp +/*! \file sexpr.h + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Simple representation of SMT S-expressions. ** ** Simple representation of SMT S-expressions. **/ diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 54e56da96..67a6c5cff 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -1,5 +1,6 @@ /********************* */ -/** unique_id.h +/*! \file unique_id.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A mechanism for getting a compile-time unique ID. ** ** A mechanism for getting a compile-time unique ID. **/ diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index bcc95b470..299e11dee 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -1,5 +1,6 @@ /********************* */ -/** cdlist_black.h +/*! \file cdlist_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::context::CDList<>. ** ** Black box testing of CVC4::context::CDList<>. **/ diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 262c66fe5..93316da76 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -1,5 +1,6 @@ /********************* */ -/** cdmap_black.h +/*! \file cdmap_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::context::CDMap<>. ** ** Black box testing of CVC4::context::CDMap<>. **/ diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 9a920ede8..a3abd6f25 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -1,5 +1,6 @@ /********************* */ -/** cdmap_white.h +/*! \file cdmap_white.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::context::CDMap<>. ** ** White box testing of CVC4::context::CDMap<>. **/ diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index 4cdb8f343..f844c2ef5 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -1,5 +1,6 @@ /********************* */ -/** cdo_black.h +/*! \file cdo_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::context::CDO<>. ** ** Black box testing of CVC4::context::CDO<>. **/ diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 46d01946b..e5aee4baa 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -1,5 +1,6 @@ /********************* */ -/** context_black.h +/*! \file context_black.h + ** \verbatim ** Original author: dejan ** Major contributors: mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::context::Context. ** ** Black box testing of CVC4::context::Context. **/ diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index e25d1f336..126245af7 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -1,14 +1,17 @@ /********************* */ -/** context_mm_black.h +/*! \file context_mm_black.h + ** \verbatim ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::context::ContextMemoryManager. ** ** Black box testing of CVC4::context::ContextMemoryManager. **/ diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 0963e4100..38649ef5b 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -1,5 +1,6 @@ /********************* */ -/** context_white.h +/*! \file context_white.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::context::Context. ** ** White box testing of CVC4::context::Context. **/ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 7894743d6..c9fc1f50b 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -1,14 +1,17 @@ /********************* */ -/** attribute_black.h - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): none +/*! \file attribute_black.h + ** \verbatim + ** Original author: dejan + ** Major contributors: taking + ** Minor contributors (to current version): cconway, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Attribute. ** ** Black box testing of CVC4::Attribute. **/ diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 509f0b02d..8afc012ff 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -1,14 +1,17 @@ /********************* */ -/** attribute_white.h +/*! \file attribute_white.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of Node attributes. ** ** White box testing of Node attributes. **/ diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h index 67e6d3e98..923df2afb 100644 --- a/test/unit/expr/declaration_scope_black.h +++ b/test/unit/expr/declaration_scope_black.h @@ -1,12 +1,17 @@ /********************* */ -/** declaration_scope_black.h +/*! \file declaration_scope_black.h + ** \verbatim ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::DeclarationScope. ** ** Black box testing of CVC4::DeclarationScope. **/ diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index ecb71081d..4d3958278 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -1,5 +1,6 @@ /********************* */ -/** expr_manager_public.h +/*! \file expr_manager_public.h + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,9 +9,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim ** - ** Public black-box testing of CVC4::Expr. + ** \brief Public black-box testing of CVC4::ExprManager. + ** + ** Public black-box testing of CVC4::ExprManager. **/ #include <cxxtest/TestSuite.h> diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 00f20dbe6..7900057e1 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -1,14 +1,17 @@ /********************* */ -/** expr_public.h +/*! \file expr_public.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public black-box testing of CVC4::Expr. ** ** Public black-box testing of CVC4::Expr. **/ diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index 8f25a9fc1..314108a5b 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -1,5 +1,6 @@ /********************* */ -/** kind_black.h +/*! \file kind_black.h + ** \verbatim ** Original author: taking ** Major contributors: none ** Minor contributors (to current version): mdeters @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Kind. ** ** Black box testing of CVC4::Kind. **/ diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 52a324d53..c79832583 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -1,14 +1,17 @@ /********************* */ -/** node_black.h +/*! \file node_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: taking - ** Minor contributors (to current version): dejan, cconway + ** Minor contributors (to current version): cconway, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Node. ** ** Black box testing of CVC4::Node. **/ diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 8bde4b047..7f315f092 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -1,14 +1,17 @@ /********************* */ -/** node_builder_black.h +/*! \file node_builder_black.h + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::NodeBuilder. ** ** Black box testing of CVC4::NodeBuilder. **/ @@ -20,6 +23,7 @@ #include <sstream> #include "expr/node_builder.h" +#include "expr/convenience_node_builders.h" #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" @@ -673,25 +677,4 @@ public: TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b)); TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b)); } - - /** - * This tests the "stack builder" - */ - void testStackBuilder() { - try { - for(unsigned i = 0; i < 100; ++i) { - size_t n = 1 + (rand() % 50); - - // make a builder "b" with a backing store for n children - makeStackNodeBuilder(b, n); - - // build one-past-the-end - for(size_t j = 0; j <= n; ++j) { - b << d_nm->mkConst(true); - } - } - } catch(Exception e) { - std::cout << e; - } - } }; diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 78c38d782..af79f5ff2 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -1,14 +1,17 @@ /********************* */ -/** node_manager_black.h - ** Original author: - ** Major contributors: none - ** Minor contributors (to current version): none +/*! \file node_manager_black.h + ** \verbatim + ** Original author: cconway + ** Major contributors: dejan + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::NodeManager. ** ** White box testing of CVC4::NodeManager. **/ @@ -341,7 +344,6 @@ public: /* This test is only valid if assertions are enabled. */ void testMkNodeTooFew() { #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_nodeManager->mkNode(AND), AssertionException ); Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() ); TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException ); #endif diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 7f0115922..62fdeb45b 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -1,14 +1,17 @@ /********************* */ -/** node_manager_white.h +/*! \file node_manager_white.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::NodeManager. ** ** White box testing of CVC4::NodeManager. **/ diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index d851c191f..9ffd2d094 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -1,14 +1,17 @@ /********************* */ -/** node_white.h +/*! \file node_white.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::Node. ** ** White box testing of CVC4::Node. **/ diff --git a/test/unit/memory.h b/test/unit/memory.h index 38ac63e65..64b1da51b 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -1,5 +1,6 @@ /********************* */ -/** memory.h +/*! \file memory.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Utility class to help testing out-of-memory conditions. ** ** Utility class to help testing out-of-memory conditions. ** diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index f6d822265..1f986732c 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -1,14 +1,18 @@ /********************* */ -/** parser_black.h +/*! \file parser_black.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::parser::Parser, including CVC, SMT and + ** SMT v2 inputs. ** ** Black box testing of CVC4::parser::Parser, including CVC, SMT and ** SMT v2 inputs. diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index f254580af..e839360d7 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -1,14 +1,17 @@ /********************* */ -/** parser_builder_black.h +/*! \file parser_builder_black.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::parser::ParserBuilder. ** ** Black box testing of CVC4::parser::ParserBuilder. **/ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index bbae46df7..def0a12ed 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -1,14 +1,17 @@ /********************* */ -/** cnf_stream_black.h +/*! \file cnf_stream_black.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::prop::CnfStream. ** ** White box testing of CVC4::prop::CnfStream. **/ diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 0443b7b8e..9c056d368 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -1,14 +1,17 @@ /********************* */ -/** theory_black.h +/*! \file theory_black.h + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::theory::Theory. ** ** Black box testing of CVC4::theory::Theory. **/ diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 8be56bc79..50c201606 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -1,14 +1,17 @@ /********************* */ -/** theory_uf_white.h +/*! \file theory_uf_white.h + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::theory::uf::TheoryUF. ** ** White box testing of CVC4::theory::uf::TheoryUF. **/ diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index d001c5a84..389f2aa1b 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -1,5 +1,6 @@ /********************* */ -/** assert_white.h +/*! \file assert_white.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::Configuration. ** ** White box testing of CVC4::Configuration. **/ diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index b866aa877..c4e77852b 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -1,14 +1,17 @@ /********************* */ -/** bitvector_black.h - ** Original author: taking +/*! \file bitvector_black.h + ** \verbatim + ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::BitVector. ** ** Black box testing of CVC4::BitVector. **/ diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h index 5ee4cf095..e06fe9636 100644 --- a/test/unit/util/configuration_black.h +++ b/test/unit/util/configuration_black.h @@ -1,5 +1,6 @@ /********************* */ -/** configuration_black.h +/*! \file configuration_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Configuration. ** ** Black box testing of CVC4::Configuration. **/ diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h index 758a12645..2bbd727fb 100644 --- a/test/unit/util/exception_black.h +++ b/test/unit/util/exception_black.h @@ -1,5 +1,6 @@ /********************* */ -/** exception_black.h +/*! \file exception_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Exception. ** ** Black box testing of CVC4::Exception. **/ diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index 627167ad3..57ae247ac 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -1,14 +1,17 @@ /********************* */ -/** integer_black.h +/*! \file integer_black.h + ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Integer. ** ** Black box testing of CVC4::Integer. **/ diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h index 3a86289a3..cd9244996 100644 --- a/test/unit/util/integer_white.h +++ b/test/unit/util/integer_white.h @@ -1,14 +1,17 @@ /********************* */ -/** integer_white.h +/*! \file integer_white.h + ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::Integer. ** ** White box testing of CVC4::Integer. **/ diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index 6e613e9f4..e6a040f7b 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -1,5 +1,6 @@ /********************* */ -/** output_black.h +/*! \file output_black.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4 output classes. ** ** Black box testing of CVC4 output classes. **/ diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h index 35d22b150..17bd7b245 100644 --- a/test/unit/util/rational_black.h +++ b/test/unit/util/rational_black.h @@ -1,5 +1,6 @@ /********************* */ -/** rational_black.h +/*! \file rational_black.h + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Rational. ** ** Black box testing of CVC4::Rational. **/ diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h index 45f1301f3..4a76e7a5d 100644 --- a/test/unit/util/rational_white.h +++ b/test/unit/util/rational_white.h @@ -1,14 +1,17 @@ /********************* */ -/** rational_white.h +/*! \file rational_white.h + ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::Rational. ** ** White box testing of CVC4::Rational. **/ |