# 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.
** 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;
** 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 ##
} 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 "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)$/) {
/********************* */
-/** cdlist.h
+/*! \file cdlist.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): barrett, taking
** 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.
**/
/********************* */
-/** 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
/********************* */
-/** cdo.h
+/*! \file cdo.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): barrett
** 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.
**/
/********************* */
-/** cdset.h
+/*! \file cdset.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** context.h
+/*! \file context.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: barrett
** Minor contributors (to current version): taking, dejan
** 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.
**/
/********************* */
-/** context_mm.cpp
+/*! \file context_mm.cpp
+ ** \verbatim
** Original author: barrett
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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
**/
/********************* */
-/** context_mm.h
+/*! \file context_mm.h
+ ** \verbatim
** Original author: barrett
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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.
type_node.cpp \
builtin_type_rules.h \
node_builder.h \
+ convenience_node_builders.h \
@srcdir@/expr.h \
type.h \
type.cpp \
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** builtin_type_rules.cpp
+/*! \file builtin_type_rules.cpp
+ ** \verbatim
** Original author: dejan
** Major contributors: none
** This file is part of the CVC4 prototype.
** 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"
/********************* */
-/** command.cpp
+/*! \file command.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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
--- /dev/null
+/********************* */
+/*! \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 */
/********************* */
-/** 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)
**/
/********************* */
-/** 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.
**/
-/*
- * 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
/********************* */
-/** expr_manager_template.cpp
+/*! \file expr_manager_template.cpp
+ ** \verbatim
** Original author: dejan
** Major contributors: cconway, mdeters
** Minor contributors (to current version): none
** 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.
**/
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,
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());
/********************* */
-/** 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.
**/
/** The the type for bit-vectors */
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
/********************* */
-/** 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.
**/
/********************* */
-/** expr_template.h
+/*! \file expr_template.h
+ ** \verbatim
** Original author: dejan
** Major contributors: mdeters
** Minor contributors (to current version): cconway, taking
** 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.
**/
/********************* */
-/** kind_template.h
+/*! \file kind_template.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
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;
/********************* */
-/** 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.
**/
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 */
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
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;
/********************* */
-/** 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.
**
** 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:
**
** 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;
** 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"
namespace CVC4 {
static const unsigned default_nchild_thresh = 10;
- template <class Builder>
- class NodeBuilderBase;
+ template <unsigned nchild_thresh>
+ class NodeBuilder;
class NodeManager;
}/* CVC4 namespace */
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
/** The NodeManager at play */
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().
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;
}
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;
}
}
}
- Builder& collapseTo(Kind k) {
+ NodeBuilder<nchild_thresh>& collapseTo(Kind k) {
AssertArgument(k != kind::UNDEFINED_KIND &&
k != kind::NULL_EXPR &&
k < kind::LAST_KIND,
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;
* 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);
// "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,
k < kind::LAST_KIND,
k, "illegal node-building kind");
d_nv->d_kind = expr::NodeValue::kindToDKind(k);
- return static_cast<Builder&>(*this);
+ return *this;
}
/**
* 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..
}
/** 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");
/** 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");
/** 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");
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");
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:
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() )) {
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!" );
}
}
-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" );
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" );
}
-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,
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);
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;
}
// 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,
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);
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;
}
/********************* */
-/** 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.
**
/********************* */
-/** 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.
**
}/* 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;
// 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);
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;
}
/********************* */
-/** node_value.cpp
+/*! \file node_value.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): cconway
** 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.
**
/********************* */
-/** node_value.h
+/*! \file node_value.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): cconway, taking
** 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.
**
template <bool ref_count> class NodeTemplate;
class TypeNode;
-template <class Builder> class NodeBuilderBase;
template <unsigned N> class NodeBuilder;
class AndNodeBuilder;
class OrNodeBuilder;
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;
/********************* */
-/** 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
**/
/********************* */
-/** 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
**/
/********************* */
-/** 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
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
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
/********************* */
-/** cvc4_private.h
+/*! \file cvc4_private.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** cvc4_public.h
+/*! \file cvc4_public.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** cvc4parser_private.h
+/*! \file cvc4parser_private.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** cvc4parser_public.h
+/*! \file cvc4parser_public.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** 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
**/
/********************* */
-/** 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.
**/
/********************* */
-/** main.h
+/*! \file main.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): dejan, barrett
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** util.cpp
+/*! \file util.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** input.cpp
+/*! \file antlr_input.cpp
+ ** \verbatim
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): none
** 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
**/
/********************* */
-/** 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.
**/
+/********************* */
+/*! \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
+ **
+ ** \brief [[ 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.
/********************* */
-/** 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
/********************* */
-/** 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
/********************* */
-/** 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.
**/
/********************* */
-/** bounded_token_factory.h
+/*! \file bounded_token_factory.h
+ ** \verbatim
** Original author: cconway
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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
/* ******************* */
-/* 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.
**/
/********************* */
-/** 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 ]]
**/
/********************* */
-/** 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 ]]
**/
/********************* */
-/** 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
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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 ]]
**/
/********************* */
-/** memory_mapped_input_buffer.h
+/*! \file memory_mapped_input_buffer.h
+ ** \verbatim
** Original author: cconway
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** parser_builder.cpp
+/*! \file parser_builder.cpp
+ ** \verbatim
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** parser_builder.h
+/*! \file parser_builder.h
+ ** \verbatim
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** parser_exception.h
+/*! \file parser_exception.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: cconway
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** parser_options.h
+/*! \file parser_options.h
+ ** \verbatim
** Original author: cconway
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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 ]]
**/
/* ******************* */
-/* 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.
**/
@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"
/* 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);
/********************* */
-/** 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 ]]
**/
/********************* */
-/** smt_input.h
+/*! \file smt_input.h
+ ** \verbatim
** Original author: cconway
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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 ]]
**/
/* ******************* */
-/* 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.
**/
@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"
/* 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);
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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 ]]
**/
/********************* */
-/** 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 ]]
**/
/********************* */
-/** 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.
/********************* */
-/** 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
/********************* */
-/** 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"
/********************* */
-/** 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.
+/********************* */
+/*! \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"
/********************* */
-/** 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.
**/
/********************* */
-/** smt_engine.cpp
+/*! \file smt_engine.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** smt_engine.h
+/*! \file smt_engine.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): none
** 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.
**/
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
-
-
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
+/********************* */
+/*! \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
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
+/********************* */
+/*! \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 {
+/********************* */
+/*! \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"
+/********************* */
+/*! \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"
/********************* */
-/** theory_arith.h
+/*! \file theory_arith.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: taking
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
** 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"
/********************* */
-/** theory_arrays.h
+/*! \file theory_arrays.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
** 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"
/********************* */
-/** theory_bv.h
+/*! \file theory_bv.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** theory_bv_types.h
+/*! \file theory_bv_type_rules.h
+ ** \verbatim
** Original author: dejan
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** interrupted.h
+/*! \file interrupted.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** theory.cpp
+/*! \file theory.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** theory.h
+/*! \file theory.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): dejan, taking
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** theoryof_table_template.h
+/*! \file theoryof_table_template.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** ecdata.cpp
+/*! \file ecdata.cpp
+ ** \verbatim
** Original author: taking
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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.
/********************* */
-/** 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.
/********************* */
-/** 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.
**/
/********************* */
-/** 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
/********************* */
-/** 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.
** 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"
/********************* */
-/** Assert.cpp
+/*! \file Assert.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** Assert.h
+/*! \file Assert.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
-/*
- * 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"
-/*
- * 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_
/********************* */
-/** bool.h
+/*! \file bool.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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,
/********************* */
-/** configuration.cpp
+/*! \file configuration.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** configuration.h
+/*! \file configuration.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
/********************* */
-/** debug.h
+/*! \file debug.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**
/********************* */
-/** decision_engine.cpp
+/*! \file decision_engine.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief .
**
**/
/********************* */
-/** decision_engine.h
+/*! \file decision_engine.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
-/*
- * 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_
-/*
- * 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_
/********************* */
-/** 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,
/********************* */
-/** 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.
**/
/********************* */
-/** model.h
+/*! \file model.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** options.h
+/*! \file options.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: cconway
** Minor contributors (to current version): dejan
** 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.
**/
/********************* */
-/** output.cpp
+/*! \file output.cpp
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** result.h
+/*! \file result.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** sexpr.cpp
+/*! \file sexpr.h
+ ** \verbatim
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** unique_id.h
+/*! \file unique_id.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** cdlist_black.h
+/*! \file cdlist_black.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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<>.
**/
/********************* */
-/** cdmap_black.h
+/*! \file cdmap_black.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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<>.
**/
/********************* */
-/** cdmap_white.h
+/*! \file cdmap_white.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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<>.
**/
/********************* */
-/** cdo_black.h
+/*! \file cdo_black.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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<>.
**/
/********************* */
-/** context_black.h
+/*! \file context_black.h
+ ** \verbatim
** Original author: dejan
** Major contributors: mdeters
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** context_white.h
+/*! \file context_white.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** expr_manager_public.h
+/*! \file expr_manager_public.h
+ ** \verbatim
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): none
** 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>
/********************* */
-/** 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.
**/
/********************* */
-/** kind_black.h
+/*! \file kind_black.h
+ ** \verbatim
** Original author: taking
** Major contributors: none
** Minor contributors (to current version): mdeters
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
#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"
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;
- }
- }
};
/********************* */
-/** 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.
**/
/* 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
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** memory.h
+/*! \file memory.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**
/********************* */
-/** 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.
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** assert_white.h
+/*! \file assert_white.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** configuration_black.h
+/*! \file configuration_black.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** exception_black.h
+/*! \file exception_black.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** 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.
**/
/********************* */
-/** output_black.h
+/*! \file output_black.h
+ ** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** rational_black.h
+/*! \file rational_black.h
+ ** \verbatim
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): none
** 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.
**/
/********************* */
-/** 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.
**/
projects / cvc5.git / commitdiff