summaryrefslogtreecommitdiff
path: root/src/expr/convenience_node_builders.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/convenience_node_builders.h')
-rw-r--r--src/expr/convenience_node_builders.h401
1 files changed, 401 insertions, 0 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback