diff options
Diffstat (limited to 'src/expr')
29 files changed, 782 insertions, 831 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index c3c3fccf6..cacae45ce 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -12,6 +12,7 @@ libexpr_la_SOURCES = \ type_node.cpp \ builtin_type_rules.h \ node_builder.h \ + convenience_node_builders.h \ @srcdir@/expr.h \ type.h \ type.cpp \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index bc724cdd1..5aaa7393a 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -1,14 +1,17 @@ /********************* */ -/** attribute.cpp +/*! \file attribute.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief AttributeManager implementation. ** ** AttributeManager implementation. **/ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 619f60a6c..2ef34a771 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -1,14 +1,17 @@ /********************* */ -/** attribute.h +/*! \file attribute.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): cconway, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Node attributes. ** ** Node attributes. **/ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 4ac89afec..b5ccb6f79 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -1,14 +1,17 @@ /********************* */ -/** attribute_internals.h +/*! \file attribute_internals.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan, taking, cconway + ** Minor contributors (to current version): taking, dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Node attributes' internals. ** ** Node attributes' internals. **/ diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h index e0ad0b038..afd206260 100644 --- a/src/expr/builtin_type_rules.h +++ b/src/expr/builtin_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** builtin_type_rules.cpp +/*! \file builtin_type_rules.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none ** This file is part of the CVC4 prototype. @@ -7,7 +8,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add brief comments here ]] + ** + ** [[ Add file-specific comments here ]] **/ #include "cvc4_private.h" diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 5fc9dee20..6c466a74c 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1,5 +1,6 @@ /********************* */ -/** command.cpp +/*! \file command.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of command objects. ** ** Implementation of command objects. **/ diff --git a/src/expr/command.h b/src/expr/command.h index 5061722f6..388ad62e6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -1,14 +1,17 @@ /********************* */ -/** command.h +/*! \file command.h + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of the command pattern on SmtEngines. ** ** Implementation of the command pattern on SmtEngines. Command ** objects are generated by the parser (typically) to implement the diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h new file mode 100644 index 000000000..655accde3 --- /dev/null +++ b/src/expr/convenience_node_builders.h @@ -0,0 +1,401 @@ +/********************* */ +/*! \file convenience_node_builders.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Convenience node builders. + ** + ** These are convenience node builders for building AND, OR, PLUS, + ** and MULT expressions. + ** + ** \todo These should be moved into theory code (say, + ** src/theory/booleans/node_builders.h and + ** src/theory/arith/node_builders.h), but for now they're here + ** because their design requires CVC4::NodeBuilder to friend them. + **/ + +// TODO: add templatized NodeTemplate<ref_count> to all these inlines +// for 'const [T]Node&' arguments? Technically a lot of time is spent +// in the TNode conversion and copy constructor, but this should be +// optimized into a simple pointer copy (?) +// TODO: double-check this. + +#include "cvc4_private.h" + +#ifndef __CVC4__CONVENIENCE_NODE_BUILDERS_H +#define __CVC4__CONVENIENCE_NODE_BUILDERS_H + +#include "expr/node_builder.h" + +namespace CVC4 { + +class AndNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::AND); + } + + inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) { + d_eb << a << b; + } + + template <bool rc> + inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&); + + template <bool rc> + inline OrNodeBuilder operator||(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class AndNodeBuilder */ + +class OrNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::OR); + } + + inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) { + d_eb << a << b; + } + + template <bool rc> + inline AndNodeBuilder operator&&(const NodeTemplate<rc>&); + + template <bool rc> + inline OrNodeBuilder& operator||(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class OrNodeBuilder */ + +class PlusNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::PLUS); + } + + inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) { + d_eb << a << b; + } + + template <bool rc> + inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&); + + template <bool rc> + inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&); + + template <bool rc> + inline MultNodeBuilder operator*(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class PlusNodeBuilder */ + +class MultNodeBuilder { +public: + NodeBuilder<> d_eb; + + inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(kind::MULT); + } + + inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) { + d_eb << a << b; + } + + template <bool rc> + inline PlusNodeBuilder operator+(const NodeTemplate<rc>&); + + template <bool rc> + inline PlusNodeBuilder operator-(const NodeTemplate<rc>&); + + template <bool rc> + inline MultNodeBuilder& operator*(const NodeTemplate<rc>&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } + +};/* class MultNodeBuilder */ + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) { + return collapseTo(kind::AND).append(e); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) { + return collapseTo(kind::OR).append(e); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) { + return collapseTo(kind::PLUS).append(e); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) { + return collapseTo(kind::PLUS). + append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) { + return collapseTo(kind::MULT).append(e); +} + +template <bool rc> +inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +template <bool rc> +inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) { + return OrNodeBuilder(Node(d_eb), n); +} + +inline AndNodeBuilder& operator&&(AndNodeBuilder& a, + const AndNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline AndNodeBuilder& operator&&(AndNodeBuilder& a, + const OrNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder operator||(AndNodeBuilder& a, + const AndNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder operator||(AndNodeBuilder& a, + const OrNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) { + return AndNodeBuilder(Node(d_eb), n); +} + +template <bool rc> +inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +inline AndNodeBuilder operator&&(OrNodeBuilder& a, + const AndNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline AndNodeBuilder operator&&(OrNodeBuilder& a, + const OrNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder& operator||(OrNodeBuilder& a, + const AndNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline OrNodeBuilder& operator||(OrNodeBuilder& a, + const OrNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +template <bool rc> +inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) { + d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n)); + return *this; +} + +template <bool rc> +inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) { + return MultNodeBuilder(Node(d_eb), n); +} + +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, + const PlusNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, + const MultNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, + const PlusNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, + const MultNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, + const PlusNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, + const MultNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { + return PlusNodeBuilder(Node(d_eb), n); +} + +template <bool rc> +inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) { + return PlusNodeBuilder(Node(d_eb), + NodeManager::currentNM()->mkNode(kind::UMINUS, n)); +} + +template <bool rc> +inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) { + d_eb.append(n); + return *this; +} + +inline PlusNodeBuilder operator+(MultNodeBuilder& a, + const PlusNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder operator+(MultNodeBuilder& a, + const MultNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, + const PlusNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, + const MultNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, + const PlusNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, + const MultNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc1, bool rc2> +inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return AndNodeBuilder(a, b); +} + +template <bool rc1, bool rc2> +inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return OrNodeBuilder(a, b); +} + +template <bool rc1, bool rc2> +inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return PlusNodeBuilder(a, b); +} + +template <bool rc1, bool rc2> +inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b)); +} + +template <bool rc1, bool rc2> +inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, + const NodeTemplate<rc2>& b) { + return MultNodeBuilder(a, b); +} + +template <bool rc> +inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, + const AndNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, + const OrNodeBuilder& b) { + return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, + const AndNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, + const OrNodeBuilder& b) { + return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, + const PlusNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, + const MultNodeBuilder& b) { + return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, + const PlusNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, + const MultNodeBuilder& b) { + return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, + const PlusNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, + const MultNodeBuilder& b) { + return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); +} + +template <bool rc> +inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { + return NodeManager::currentNM()->mkNode(kind::UMINUS, a); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__CONVENIENCE_NODE_BUILDERS_H */ diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 6dc9453d2..761dd6d24 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -1,12 +1,17 @@ /********************* */ -/** declaration_scope.cpp +/*! \file declaration_scope.cpp + ** \verbatim ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Convenience class for scoping variable and type declarations (implementation). ** ** Convenience class for scoping variable and type declarations (implementation) **/ diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index e33aa25fa..a6947c536 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -1,12 +1,17 @@ /********************* */ -/** context.h +/*! \file declaration_scope.h + ** \verbatim ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Convenience class for scoping variable and type declarations. ** ** Convenience class for scoping variable and type declarations. **/ diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index 38f8fc787..cb983b006 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -1,9 +1,21 @@ -/* - * expr_manager_scope.h - * - * Created on: Apr 7, 2010 - * Author: dejan - */ +/********************* */ +/*! \file expr_manager_scope.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__EXPR_MANAGER_SCOPE_H #define __CVC4__EXPR_MANAGER_SCOPE_H diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index bf0e2f96e..3eb2a8109 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1,5 +1,6 @@ /********************* */ -/** expr_manager_template.cpp +/*! \file expr_manager_template.cpp + ** \verbatim ** Original author: dejan ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression manager interface, implementation. ** ** Public-facing expression manager interface, implementation. **/ @@ -71,17 +74,6 @@ BitVectorType ExprManager::bitVectorType(unsigned size) const { return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size))); } -Expr ExprManager::mkExpr(Kind kind) { - const unsigned n = 0; - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkNodePtr(kind)); -} - Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { const unsigned n = 1; CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, @@ -252,7 +244,7 @@ Expr ExprManager::mkVar(const Type& type) { Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { - CheckArgument( metakind::isAssociative(kind), kind, + CheckArgument( kind::isAssociative(kind), kind, "Illegal kind in mkAssociative: %s", kind::kindToString(kind).c_str()); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 4cde091ac..707d9a26e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -1,14 +1,17 @@ /********************* */ -/** expr_manager_template.h +/*! \file expr_manager_template.h + ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking, cconway + ** Major contributors: cconway, mdeters + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression manager interface. ** ** Public-facing expression manager interface. **/ @@ -101,13 +104,6 @@ public: BitVectorType bitVectorType(unsigned size) const; /** - * Make a unary expression of a given kind (TRUE, FALSE,...). - * @param kind the kind of expression - * @return the expression - */ - Expr mkExpr(Kind kind); - - /** * Make a unary expression of a given kind (NOT, BVNOT, ...). * @param child1 kind the kind of expression * @return the expression diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index edd49f032..b4359cf2a 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -1,14 +1,17 @@ /********************* */ -/** expr_template.cpp +/*! \file expr_template.cpp + ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): cconway, taking + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression interface, implementation. ** ** Public-facing expression interface, implementation. **/ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 6597d5f14..73aa666e6 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -1,5 +1,6 @@ /********************* */ -/** expr_template.h +/*! \file expr_template.h + ** \verbatim ** Original author: dejan ** Major contributors: mdeters ** Minor contributors (to current version): cconway, taking @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Public-facing expression interface. ** ** Public-facing expression interface. **/ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 96c34a02a..718fd58f4 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -1,5 +1,6 @@ /********************* */ -/** kind_template.h +/*! \file kind_template.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Template for the Node kind header. ** ** Template for the Node kind header. **/ @@ -57,6 +60,23 @@ ${kind_printers} return out; } +/** Returns true if the given kind is associative. This is used by ExprManager to + * decide whether it's safe to modify big expressions by changing the grouping of + * the arguments. */ +/* TODO: This could be generated. */ +inline bool isAssociative(::CVC4::Kind k) { + switch(k) { + case kind::AND: + case kind::OR: + case kind::MULT: + case kind::PLUS: + return true; + + default: + return false; + } +} + inline std::string kindToString(::CVC4::Kind k) { std::stringstream ss; ss << k; diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index fc0910893..079199359 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -1,14 +1,17 @@ /********************* */ -/** metakind_template.h +/*! \file metakind_template.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Template for the metakind header. ** ** Template for the metakind header. **/ @@ -294,23 +297,6 @@ ${metakind_ubchildren} return ubs[k]; } -/** Returns true if the given kind is associative. This is used by ExprManager to - * decide whether it's safe to modify big expressions by changing the grouping of - * the arguments. */ -/* TODO: This could be generated. */ -inline bool isAssociative(::CVC4::Kind k) { - switch(k) { - case kind::AND: - case kind::OR: - case kind::MULT: - case kind::PLUS: - return true; - - default: - return false; - } -} - }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ }/* CVC4 namespace */ diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 7ebea8a70..2b6417e8a 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,14 +1,17 @@ /********************* */ -/** node.cpp +/*! \file node.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ diff --git a/src/expr/node.h b/src/expr/node.h index 0daa3f58c..cfaab142d 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1,14 +1,17 @@ /********************* */ -/** node.h +/*! \file node.h + ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway, taking + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ @@ -138,8 +141,8 @@ class NodeTemplate { friend class NodeTemplate<false>; friend class NodeManager; - template <class Builder> - friend class NodeBuilderBase; + template <unsigned nchild_thresh> + friend class NodeBuilder; friend class ::CVC4::expr::attr::AttributeManager; diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 877c50d82..d81190d7a 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,14 +1,17 @@ /********************* */ -/** node_builder.h +/*! \file node_builder.h + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): taking, dejan + ** Major contributors: dejan + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A builder interface for Nodes. ** ** A builder interface for Nodes. ** @@ -101,12 +104,12 @@ ** returned in a Node wrapper. ** ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper - ** temporary for the NodeValue in the NodeBuilderBase<>::operator - ** Node() member function. If we create a temporary (for example by - ** writing Debug("builder") << Node(nv) << endl), the NodeValue will - ** have its reference count incremented from zero to one, then - ** decremented, which makes it eligible for collection before the - ** builder has even returned it! So this is a no-no. + ** temporary for the NodeValue in the NodeBuilder<>::operator Node() + ** member function. If we create a temporary (for example by writing + ** Debug("builder") << Node(nv) << endl), the NodeValue will have its + ** reference count incremented from zero to one, then decremented, + ** which makes it eligible for collection before the builder has even + ** returned it! So this is a no-no. ** ** There are also two cases when the NodeBuilder is clear()'ed: ** @@ -131,32 +134,10 @@ ** d_nv is deallocated. ** ** Regarding the backing store (typically on the stack): the file - ** below provides three classes (two of them are templates): - ** - ** template <class Builder> class NodeBuilderBase; - ** - ** This is the base class for node builders. It can not be used - ** directly. It contains a shared implementation but is intended - ** to be subclassed. Derived classes supply its "in-line" buffer. - ** - ** class BackedNodeBuilder; - ** - ** This is the usable form for a user-supplied-backing-store node - ** builder. A user can allocate a buffer large enough for a - ** NodeValue with N children (say, on the stack), then pass a - ** pointer to this buffer, and the parameter N, to a - ** BackedNodeBuilder. It will use this buffer to build its - ** NodeValue until the number of children exceeds N; then it will - ** allocate d_nv on the heap. - ** - ** To ensure that the buffer is properly-sized, it is recommended - ** to use the makeStackNodeBuilder(b, N) macro to make a - ** BackedNodeBuilder "b" with a stack-allocated buffer large - ** enough to hold N children. + ** below provides the template: ** ** template <unsigned nchild_thresh> class NodeBuilder; ** - ** This is the conceptually easiest form of NodeBuilder to use. ** The default: ** ** NodeBuilder<> b; @@ -164,9 +145,7 @@ ** gives you a backing buffer with capacity for 10 children in ** the same place as the NodeBuilder<> itself is allocated. You ** can specify another size as a template parameter, but it must - ** be a compile-time constant (which is why the BackedNodeBuilder - ** creator-macro "makeStackNodeBuilder(b, N)" is sometimes - ** preferred). + ** be a compile-time constant. **/ #include "cvc4_private.h" @@ -185,8 +164,8 @@ namespace CVC4 { static const unsigned default_nchild_thresh = 10; - template <class Builder> - class NodeBuilderBase; + template <unsigned nchild_thresh> + class NodeBuilder; class NodeManager; }/* CVC4 namespace */ @@ -199,38 +178,31 @@ namespace CVC4 { namespace CVC4 { -template <class Builder> -inline std::ostream& operator<<(std::ostream&, const NodeBuilderBase<Builder>&); +template <unsigned nchild_thresh> +inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&); +/* see expr/convenience_node_builders.h */ class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; class MultNodeBuilder; /** - * A base class for NodeBuilders. When extending this class, use: - * - * class MyExtendedNodeBuilder : - * public NodeBuilderBase<MyExtendedNodeBuilder> { ... }; - * - * This ensures that certain member functions return the right - * (derived) class type. - * - * There are no virtual functions here, and that should remain the - * case! This class is just used for sharing of implementation. Two - * types derive from it: BackedNodeBuilder (which allows for an - * external buffer), and the NodeBuilder<> template, which requires - * that you give it a compile-time constant backing-store size. + * The main template NodeBuilder. */ -template <class Builder> -class NodeBuilderBase { -protected: - +template <unsigned nchild_thresh = default_nchild_thresh> +class NodeBuilder { /** - * A reference to an "in-line" stack-allocated buffer for use by the + * An "in-line" stack-allocated buffer for use by the * NodeBuilder. */ - expr::NodeValue& d_inlineNv; + expr::NodeValue d_inlineNv; + /** + * Space for the children of the node being constructed. This is + * never accessed directly, but rather through + * d_inlineNv.d_children[i]. + */ + expr::NodeValue* d_inlineNvChildSpace[nchild_thresh]; /** * A pointer to the "current" NodeValue buffer; either &d_inlineNv @@ -242,16 +214,13 @@ protected: NodeManager* d_nm; /** - * The maximum number of children that can be held in this "in-line" - * buffer. - */ - const uint16_t d_inlineNvMaxChildren; - - /** * The number of children allocated in d_nv. */ uint16_t d_nvMaxChildren; + template <unsigned N> + void internalCopy(const NodeBuilder<N>& nb); + /** * Returns whether or not this NodeBuilder has been "used"---i.e., * whether a Node has been extracted with operator Node(). @@ -267,7 +236,7 @@ protected: inline void setUsed() { Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!"); Assert(d_inlineNv.d_nchildren == 0 && - d_nvMaxChildren == d_inlineNvMaxChildren, + d_nvMaxChildren == nchild_thresh, "Internal error: bad `inline' state in NodeBuilder!"); d_nv = NULL; } @@ -279,7 +248,7 @@ protected: inline void setUnused() { Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!"); Assert(d_inlineNv.d_nchildren == 0 && - d_nvMaxChildren == d_inlineNvMaxChildren, + d_nvMaxChildren == nchild_thresh, "Internal error: bad `inline' state in NodeBuilder!"); d_nv = &d_inlineNv; } @@ -377,7 +346,7 @@ protected: } } - Builder& collapseTo(Kind k) { + NodeBuilder<nchild_thresh>& collapseTo(Kind k) { AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, @@ -389,27 +358,98 @@ protected: d_nv->d_kind = expr::NodeValue::kindToDKind(k); return append(n); } - return static_cast<Builder&>(*this); + return *this; + } + +public: + + inline NodeBuilder() : + d_nv(&d_inlineNv), + d_nm(NodeManager::currentNM()), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_nchildren = 0; } -protected: + inline NodeBuilder(Kind k) : + d_nv(&d_inlineNv), + d_nm(NodeManager::currentNM()), + d_nvMaxChildren(nchild_thresh) { - inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, - Kind k = kind::UNDEFINED_KIND); - inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, - NodeManager* nm, Kind k = kind::UNDEFINED_KIND); + Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); -private: - // disallow copy or assignment of these base classes directly (there - // would be no backing store!) - NodeBuilderBase(const NodeBuilderBase& nb); - NodeBuilderBase& operator=(const NodeBuilderBase& nb); + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; + } -public: + inline NodeBuilder(NodeManager* nm) : + d_nv(&d_inlineNv), + d_nm(nm), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_nchildren = 0; + } + + inline NodeBuilder(NodeManager* nm, Kind k) : + d_nv(&d_inlineNv), + d_nm(nm), + d_nvMaxChildren(nchild_thresh) { + + Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); - // Intentionally not virtual; we don't want a vtable. Don't - // override this in a derived class. - inline ~NodeBuilderBase(); + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; + } + + inline ~NodeBuilder() { + if(EXPECT_FALSE( nvIsAllocated() )) { + dealloc(); + } else if(EXPECT_FALSE( !isUsed() )) { + decrRefCounts(); + } + } + + // These implementations are identical, but we need to have both of + // these because the templatized version isn't recognized as a + // generalization of a copy constructor (and a default copy + // constructor will be generated [?]) + inline NodeBuilder(const NodeBuilder& nb) : + d_nv(&d_inlineNv), + d_nm(nb.d_nm), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = nb.d_nv->d_kind; + d_inlineNv.d_nchildren = 0; + + internalCopy(nb); + } + + // technically this is a conversion, not a copy + template <unsigned N> + inline NodeBuilder(const NodeBuilder<N>& nb) : + d_nv(&d_inlineNv), + d_nm(nb.d_nm), + d_nvMaxChildren(nchild_thresh) { + + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = nb.d_nv->d_kind; + d_inlineNv.d_nchildren = 0; + + internalCopy(nb); + } typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator; typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator; @@ -485,9 +525,9 @@ public: * allocated, and decrements the reference counts of any currently * children in the NodeBuilder. * - * This should leave the BackedNodeBuilder in the state it was after + * This should leave the NodeBuilder in the state it was after * initial construction, except for Kind, which is set to the - * argument (if provided), or UNDEFINED_KIND. In particular, the + * argument, if provided, or UNDEFINED_KIND. In particular, the * associated NodeManager is not affected by clear(). */ void clear(Kind k = kind::UNDEFINED_KIND); @@ -495,7 +535,7 @@ public: // "Stream" expression constructor syntax /** Set the Kind of this Node-under-construction. */ - inline Builder& operator<<(const Kind& k) { + inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() == kind::UNDEFINED_KIND, @@ -505,7 +545,7 @@ public: k < kind::LAST_KIND, k, "illegal node-building kind"); d_nv->d_kind = expr::NodeValue::kindToDKind(k); - return static_cast<Builder&>(*this); + return *this; } /** @@ -514,7 +554,7 @@ public: * FIXME: do we really want that collapse behavior? We had agreed * on it but then never wrote code like that. */ - Builder& operator<<(TNode n) { + NodeBuilder<nchild_thresh>& operator<<(TNode n) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); /* FIXME: disable this "collapsing" for now.. @@ -527,7 +567,7 @@ public: } /** Append a sequence of children to this TypeNode-under-construction. */ - inline Builder& + inline NodeBuilder<nchild_thresh>& append(const std::vector<TypeNode>& children) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); @@ -536,7 +576,7 @@ public: /** Append a sequence of children to this Node-under-construction. */ template <bool ref_count> - inline Builder& + inline NodeBuilder<nchild_thresh>& append(const std::vector<NodeTemplate<ref_count> >& children) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); @@ -545,17 +585,17 @@ public: /** Append a sequence of children to this Node-under-construction. */ template <class Iterator> - Builder& append(const Iterator& begin, const Iterator& end) { + NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); for(Iterator i = begin; i != end; ++i) { append(*i); } - return static_cast<Builder&>(*this); + return *this; } /** Append a child to this Node-under-construction. */ - Builder& append(TNode n) { + NodeBuilder<nchild_thresh>& append(TNode n) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node"); @@ -563,11 +603,11 @@ public: expr::NodeValue* nv = n.d_nv; nv->inc(); d_nv->d_children[d_nv->d_nchildren++] = nv; - return static_cast<Builder&>(*this); + return *this; } /** Append a child to this Node-under-construction. */ - Builder& append(const TypeNode& typeNode) { + NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node"); @@ -575,7 +615,7 @@ public: expr::NodeValue* nv = typeNode.d_nv; nv->inc(); d_nv->d_children[d_nv->d_nchildren++] = nv; - return static_cast<Builder&>(*this); + return *this; } private: @@ -609,592 +649,38 @@ public: d_nv->toStream(out, depth); } - Builder& operator&=(TNode); - Builder& operator|=(TNode); - Builder& operator+=(TNode); - Builder& operator-=(TNode); - Builder& operator*=(TNode); + NodeBuilder<nchild_thresh>& operator&=(TNode); + NodeBuilder<nchild_thresh>& operator|=(TNode); + NodeBuilder<nchild_thresh>& operator+=(TNode); + NodeBuilder<nchild_thresh>& operator-=(TNode); + NodeBuilder<nchild_thresh>& operator*=(TNode); friend class AndNodeBuilder; friend class OrNodeBuilder; friend class PlusNodeBuilder; friend class MultNodeBuilder; -};/* class NodeBuilderBase */ - -/** - * Backing-store interface version for NodeBuilders. To construct one - * of these, you need to create a backing store (preferably on the - * stack) for it to hold its "inline" NodeValue. There's a - * convenience macro defined below, makeStackNodeBuilder(b, N), - * defined below to define a stack-allocated BackedNodeBuilder "b" - * with room for N children on the stack. - */ -class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> { -public: - inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, Kind k) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - inline BackedNodeBuilder(expr::NodeValue* buf, - unsigned maxChildren, - NodeManager* nm) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - inline BackedNodeBuilder(expr::NodeValue* buf, - unsigned maxChildren, - NodeManager* nm, - Kind k) : - NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) { - } - - // we don't want a vtable, so do not declare a dtor! - //inline ~BackedNodeBuilder(); - -private: - // disallow copy or assignment (there would be no backing store!) - BackedNodeBuilder(const BackedNodeBuilder& nb); - BackedNodeBuilder& operator=(const BackedNodeBuilder& nb); - -};/* class BackedNodeBuilder */ - -/** - * Stack-allocate a BackedNodeBuilder with a stack-allocated backing - * store of size __n. The BackedNodeBuilder will be named __v. - * - * __v must be a simple name. __n must be convertible to size_t, and - * will be evaluated only once. This macro may only be used where - * declarations are permitted. - */ -#define makeStackNodeBuilder(__v, __n) \ - const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \ - ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v \ - [1 + ( ( ( sizeof(::CVC4::expr::NodeValue) + \ - sizeof(::CVC4::expr::NodeValue*) + 1 ) / \ - sizeof(::CVC4::expr::NodeValue*) ) * \ - __cvc4_backednodebuilder_nchildren__ ## __v)]; \ - ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \ - __cvc4_backednodebuilder_nchildren__ ## __v) -// IF THE ABOVE ASSERTION FAILS, write another compiler-specific -// version of makeStackNodeBuilder() that works for your compiler -// (even if it's suboptimal, ignoring its __n argument, and just -// creates a NodeBuilder<10>). - - -/** - * Simple NodeBuilder interface. This is a template that requires - * that the number of children of the "inline"-allocated NodeValue be - * specified as a template parameter (which means it must be a - * compile-time constant). - */ -template <unsigned nchild_thresh = default_nchild_thresh> -class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > { - // This is messy: - // 1. This (anonymous) struct here must be a POD to avoid the - // compiler laying out things in a different way. - // 2. The layout is engineered carefully. We can't just - // stack-allocate enough bytes as a char[] because we break - // strict-aliasing rules. The first thing in the struct is a - // "NodeValue" so a pointer to this struct should be safely - // castable to a pointer to a NodeValue (same alignment). - struct BackingStore { - expr::NodeValue n; - expr::NodeValue* c[nchild_thresh]; - } d_backingStore; - - typedef NodeBuilderBase<NodeBuilder<nchild_thresh> > super; - - template <unsigned N> - void internalCopy(const NodeBuilder<N>& nb); - -public: - inline NodeBuilder() : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh) { - } - - inline NodeBuilder(Kind k) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - k) { - } - - inline NodeBuilder(NodeManager* nm) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nm) { - } - - inline NodeBuilder(NodeManager* nm, Kind k) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nm, - k) { - } - - // These implementations are identical, but we need to have both of - // these because the templatized version isn't recognized as a - // generalization of a copy constructor (and a default copy - // constructor will be generated [?]) - inline NodeBuilder(const NodeBuilder& nb) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nb.d_nm, - nb.getKind()) { - internalCopy(nb); - } - - // technically this is a conversion, not a copy - template <unsigned N> - inline NodeBuilder(const NodeBuilder<N>& nb) : - NodeBuilderBase<NodeBuilder<nchild_thresh> > - (reinterpret_cast<expr::NodeValue*>(&d_backingStore), - nchild_thresh, - nb.d_nm, - nb.getKind()) { - internalCopy(nb); - } - - // we don't want a vtable, so do not declare a dtor! - //inline ~NodeBuilder(); - // This is needed for copy constructors of different sizes to access // private fields template <unsigned N> friend class NodeBuilder; - };/* class NodeBuilder<> */ +}/* CVC4 namespace */ + // TODO: add templatized NodeTemplate<ref_count> to all above and // below inlines for 'const [T]Node&' arguments? Technically a lot of // time is spent in the TNode conversion and copy constructor, but // this should be optimized into a simple pointer copy (?) // TODO: double-check this. -class AndNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::AND); - } - - inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) { - d_eb << a << b; - } - - template <bool rc> - inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&); - - template <bool rc> - inline OrNodeBuilder operator||(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class AndNodeBuilder */ - -class OrNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::OR); - } - - inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) { - d_eb << a << b; - } - - template <bool rc> - inline AndNodeBuilder operator&&(const NodeTemplate<rc>&); - - template <bool rc> - inline OrNodeBuilder& operator||(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class OrNodeBuilder */ - -class PlusNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::PLUS); - } - - inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) { - d_eb << a << b; - } - - template <bool rc> - inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&); - - template <bool rc> - inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&); - - template <bool rc> - inline MultNodeBuilder operator*(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class PlusNodeBuilder */ - -class MultNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::MULT); - } - - inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) { - d_eb << a << b; - } - - template <bool rc> - inline PlusNodeBuilder operator+(const NodeTemplate<rc>&); - - template <bool rc> - inline PlusNodeBuilder operator-(const NodeTemplate<rc>&); - - template <bool rc> - inline MultNodeBuilder& operator*(const NodeTemplate<rc>&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class MultNodeBuilder */ - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator&=(TNode e) { - return collapseTo(kind::AND).append(e); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator|=(TNode e) { - return collapseTo(kind::OR).append(e); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) { - return collapseTo(kind::PLUS).append(e); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) { - return collapseTo(kind::PLUS). - append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); -} - -template <class Builder> -inline Builder& NodeBuilderBase<Builder>::operator*=(TNode e) { - return collapseTo(kind::MULT).append(e); -} - -template <bool rc> -inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -template <bool rc> -inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) { - return OrNodeBuilder(Node(d_eb), n); -} - -inline AndNodeBuilder& operator&&(AndNodeBuilder& a, - const AndNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline AndNodeBuilder& operator&&(AndNodeBuilder& a, - const OrNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder operator||(AndNodeBuilder& a, - const AndNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder operator||(AndNodeBuilder& a, - const OrNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) { - return AndNodeBuilder(Node(d_eb), n); -} - -template <bool rc> -inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -inline AndNodeBuilder operator&&(OrNodeBuilder& a, - const AndNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline AndNodeBuilder operator&&(OrNodeBuilder& a, - const OrNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder& operator||(OrNodeBuilder& a, - const AndNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline OrNodeBuilder& operator||(OrNodeBuilder& a, - const OrNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -template <bool rc> -inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) { - d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n)); - return *this; -} - -template <bool rc> -inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) { - return MultNodeBuilder(Node(d_eb), n); -} - -inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, - const PlusNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder operator*(PlusNodeBuilder& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder operator*(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { - return PlusNodeBuilder(Node(d_eb), n); -} - -template <bool rc> -inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) { - return PlusNodeBuilder(Node(d_eb), - NodeManager::currentNM()->mkNode(kind::UMINUS, n)); -} - -template <bool rc> -inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) { - d_eb.append(n); - return *this; -} - -inline PlusNodeBuilder operator+(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder operator+(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder operator-(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline PlusNodeBuilder operator-(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder& operator*(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} -inline MultNodeBuilder& operator*(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc1, bool rc2> -inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return AndNodeBuilder(a, b); -} - -template <bool rc1, bool rc2> -inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return OrNodeBuilder(a, b); -} - -template <bool rc1, bool rc2> -inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return PlusNodeBuilder(a, b); -} - -template <bool rc1, bool rc2> -inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b)); -} - -template <bool rc1, bool rc2> -inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, - const NodeTemplate<rc2>& b) { - return MultNodeBuilder(a, b); -} - -template <bool rc> -inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, - const AndNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, - const OrNodeBuilder& b) { - return a && Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, - const AndNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, - const OrNodeBuilder& b) { - return a || Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, - const MultNodeBuilder& b) { - return a + Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, - const PlusNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, - const MultNodeBuilder& b) { - return a - Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, - const MultNodeBuilder& b) { - return a * Node(const_cast<NodeBuilder<>&>(b.d_eb)); -} - -template <bool rc> -inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { - return NodeManager::currentNM()->mkNode(kind::UMINUS, a); -} - -}/* CVC4 namespace */ - #include "expr/node.h" #include "expr/node_manager.h" namespace CVC4 { -template <class Builder> -inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, - unsigned maxChildren, - Kind k) : - d_inlineNv(*buf), - d_nv(&d_inlineNv), - d_nm(NodeManager::currentNM()), - d_inlineNvMaxChildren(maxChildren), - d_nvMaxChildren(maxChildren) { - - Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); - - d_inlineNv.d_id = 0; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - d_inlineNv.d_nchildren = 0; -} - -template <class Builder> -inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, - unsigned maxChildren, - NodeManager* nm, - Kind k) : - d_inlineNv(*buf), - d_nv(&d_inlineNv), - d_nm(nm), - d_inlineNvMaxChildren(maxChildren), - d_nvMaxChildren(maxChildren) { - - Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); - - d_inlineNv.d_id = 0; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - d_inlineNv.d_nchildren = 0; -} - -template <class Builder> -inline NodeBuilderBase<Builder>::~NodeBuilderBase() { - if(EXPECT_FALSE( nvIsAllocated() )) { - dealloc(); - } else if(EXPECT_FALSE( !isUsed() )) { - decrRefCounts(); - } -} - -template <class Builder> -void NodeBuilderBase<Builder>::clear(Kind k) { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::clear(Kind k) { Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind"); if(EXPECT_FALSE( nvIsAllocated() )) { @@ -1214,8 +700,8 @@ void NodeBuilderBase<Builder>::clear(Kind k) { d_inlineNv.d_nchildren = 0; } -template <class Builder> -void NodeBuilderBase<Builder>::realloc(size_t toSize) { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { Assert( toSize > d_nvMaxChildren, "attempt to realloc() a NodeBuilder to a smaller/equal size!" ); @@ -1258,8 +744,8 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) { } } -template <class Builder> -void NodeBuilderBase<Builder>::dealloc() { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::dealloc() { Assert( nvIsAllocated(), "Internal error: NodeBuilder: dealloc() called without a " "private NodeBuilder-allocated buffer" ); @@ -1272,11 +758,11 @@ void NodeBuilderBase<Builder>::dealloc() { free(d_nv); d_nv = &d_inlineNv; - d_nvMaxChildren = d_inlineNvMaxChildren; + d_nvMaxChildren = nchild_thresh; } -template <class Builder> -void NodeBuilderBase<Builder>::decrRefCounts() { +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::decrRefCounts() { Assert( !nvIsAllocated(), "Internal error: NodeBuilder: decrRefCounts() called with a " "private NodeBuilder-allocated buffer" ); @@ -1291,48 +777,48 @@ void NodeBuilderBase<Builder>::decrRefCounts() { } -template <class Builder> -TypeNode NodeBuilderBase<Builder>::constructTypeNode() { +template <unsigned nchild_thresh> +TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() { return TypeNode(constructNV()); } -template <class Builder> -TypeNode NodeBuilderBase<Builder>::constructTypeNode() const { +template <unsigned nchild_thresh> +TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const { return TypeNode(constructNV()); } -template <class Builder> -Node NodeBuilderBase<Builder>::constructNode() { +template <unsigned nchild_thresh> +Node NodeBuilder<nchild_thresh>::constructNode() { return Node(constructNV()); } -template <class Builder> -Node NodeBuilderBase<Builder>::constructNode() const { +template <unsigned nchild_thresh> +Node NodeBuilder<nchild_thresh>::constructNode() const { return Node(constructNV()); } -template <class Builder> -Node* NodeBuilderBase<Builder>::constructNodePtr() { +template <unsigned nchild_thresh> +Node* NodeBuilder<nchild_thresh>::constructNodePtr() { return new Node(constructNV()); } -template <class Builder> -Node* NodeBuilderBase<Builder>::constructNodePtr() const { +template <unsigned nchild_thresh> +Node* NodeBuilder<nchild_thresh>::constructNodePtr() const { return new Node(constructNV()); } -template <class Builder> -NodeBuilderBase<Builder>::operator Node() { +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator Node() { return constructNode(); } -template <class Builder> -NodeBuilderBase<Builder>::operator Node() const { +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator Node() const { return constructNode(); } -template <class Builder> -expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { +template <unsigned nchild_thresh> +expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() != kind::UNDEFINED_KIND, @@ -1396,7 +882,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { if(EXPECT_TRUE( ! nvIsAllocated() )) { /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** supplied by the user (or derived class) **/ + ** allocated "inline" in this NodeBuilder. **/ // Lookup the expression value in the pool we already have expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); @@ -1490,7 +976,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { expr::NodeValue* nv = d_nv; nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading d_nv = &d_inlineNv; - d_nvMaxChildren = d_inlineNvMaxChildren; + d_nvMaxChildren = nchild_thresh; setUsed(); //poolNv = nv; @@ -1503,8 +989,8 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { } // CONST VERSION OF NODE EXTRACTOR -template <class Builder> -expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const { +template <unsigned nchild_thresh> +expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() != kind::UNDEFINED_KIND, @@ -1567,7 +1053,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const { if(EXPECT_TRUE( ! nvIsAllocated() )) { /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** supplied by the user (or derived class) **/ + ** allocated "inline" in this NodeBuilder. **/ // Lookup the expression value in the pool we already have expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); @@ -1683,30 +1169,30 @@ template <unsigned nchild_thresh> template <unsigned N> void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { if(nb.isUsed()) { - super::setUsed(); + setUsed(); return; } - if(nb.d_nvMaxChildren > super::d_nvMaxChildren) { - super::realloc(nb.d_nvMaxChildren); + if(nb.d_nvMaxChildren > d_nvMaxChildren) { + realloc(nb.d_nvMaxChildren); } std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), - super::d_nv->nv_begin()); + d_nv->nv_begin()); - super::d_nv->d_nchildren = nb.d_nv->d_nchildren; + d_nv->d_nchildren = nb.d_nv->d_nchildren; - for(expr::NodeValue::nv_iterator i = super::d_nv->nv_begin(); - i != super::d_nv->nv_end(); + for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); + i != d_nv->nv_end(); ++i) { (*i)->inc(); } } -template <class Builder> +template <unsigned nchild_thresh> inline std::ostream& operator<<(std::ostream& out, - const NodeBuilderBase<Builder>& b) { + const NodeBuilder<nchild_thresh>& b) { b.toStream(out, Node::setdepth::getDepth(out)); return out; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a1b5b771f..247348497 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,14 +1,17 @@ /********************* */ -/** node_manager.cpp +/*! \file node_manager.cpp + ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan, taking + ** Major contributors: dejan + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Expression manager implementation. ** ** Expression manager implementation. ** diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5642a8372..2d96ac57a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,14 +1,17 @@ /********************* */ -/** node_manager.h +/*! \file node_manager.h + ** \verbatim ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): taking, dejan + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A manager for Nodes. ** ** A manager for Nodes. ** @@ -50,7 +53,7 @@ typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; }/* CVC4::expr namespace */ class NodeManager { - template <class Builder> friend class CVC4::NodeBuilderBase; + template <unsigned nchild_thresh> friend class CVC4::NodeBuilder; friend class NodeManagerScope; friend class expr::NodeValue; @@ -262,10 +265,6 @@ public: // general expression-builders - /** Create a node with no children. */ - Node mkNode(Kind kind); - Node* mkNodePtr(Kind kind); - /** Create a node with one child. */ Node mkNode(Kind kind, TNode child1); Node* mkNodePtr(Kind kind, TNode child1); @@ -740,15 +739,6 @@ inline TypeNode NodeManager::mkSort(const std::string& name) { return type; } -inline Node NodeManager::mkNode(Kind kind) { - return NodeBuilder<0>(this, kind); -} - -inline Node* NodeManager::mkNodePtr(Kind kind) { - NodeBuilder<0> nb(this, kind); - return nb.constructNodePtr(); -} - inline Node NodeManager::mkNode(Kind kind, TNode child1) { return NodeBuilder<1>(this, kind) << child1; } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 101be5187..c64a608fb 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -1,5 +1,6 @@ /********************* */ -/** node_value.cpp +/*! \file node_value.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): cconway @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An expression node. ** ** An expression node. ** diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 260a9daae..8b2056560 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,6 @@ /********************* */ -/** node_value.h +/*! \file node_value.h + ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): cconway, taking @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief An expression node. ** ** An expression node. ** @@ -35,7 +38,6 @@ namespace CVC4 { template <bool ref_count> class NodeTemplate; class TypeNode; -template <class Builder> class NodeBuilderBase; template <unsigned N> class NodeBuilder; class AndNodeBuilder; class OrNodeBuilder; @@ -103,7 +105,6 @@ class NodeValue { template <bool> friend class ::CVC4::NodeTemplate; friend class ::CVC4::TypeNode; - template <class Builder> friend class ::CVC4::NodeBuilderBase; template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder; friend class ::CVC4::NodeManager; diff --git a/src/expr/type.cpp b/src/expr/type.cpp index af333f9d3..3bacb4792 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -1,14 +1,17 @@ /********************* */ -/** type.cpp +/*! \file type.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of expression types . ** ** Implementation of expression types **/ diff --git a/src/expr/type.h b/src/expr/type.h index 137dbfff3..2d18c2fc8 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -1,14 +1,17 @@ /********************* */ -/** type.h +/*! \file type.h + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Interface for expression types. ** ** Interface for expression types **/ diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h index a847bc827..0f5b522b6 100644 --- a/src/expr/type_constant.h +++ b/src/expr/type_constant.h @@ -1,13 +1,17 @@ /********************* */ -/** type_constant.h +/*! \file type_constant.h + ** \verbatim ** Original author: dejan + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Interface for expression types. ** ** Interface for expression types **/ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 821349b45..1afaf2b89 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -1,14 +1,17 @@ /********************* */ -/** node.cpp +/*! \file type_node.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index f7b1a6b9e..9b67c674c 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1,12 +1,17 @@ /********************* */ -/** type_node.h +/*! \file type_node.h + ** \verbatim ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Reference-counted encapsulation of a pointer to node information. ** ** Reference-counted encapsulation of a pointer to node information. **/ @@ -62,8 +67,8 @@ class TypeNode { friend class NodeManager; - template <class Builder> - friend class NodeBuilderBase; + template <unsigned nchild_thresh> + friend class NodeBuilder; /** * Assigns the expression value and does reference counting. No assumptions |