diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
commit | 826f583ee14b922f39666dc827a5624fff753724 (patch) | |
tree | 03e7f1ad98b003dae5f6406bb990a715041d239c /src/expr/node_builder.h | |
parent | f716b67e7bedd90c4dd43617158c0f55c1811334 (diff) |
* src/expr/node.h: add a copy constructor. Apparently GCC doesn't
recognize an instantiation of the join conversion/copy ctor with
ref_count = ref_count_1 as a copy constructor. Problems with
reference counts ensue.
* src/theory/theory.h, src/theory/theory.cpp: Theory base
implementation work. Changed from continuation-style theory calls
to having an data member for the output channel. registerTerm() and
preRegisterTerm() work.
* src/theory/output_channel.h, src/theory/theory.h,
src/theory/theory.cpp, src/theory/uf/theory_uf.h,
src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
OutputChannel.
* test/unit/expr/node_black.h: remove testPlusNode(),
testUMinusNode(), testMultNode().
* src/expr/attribute.h: new facilities ManagedAttribute<> and
CDAttribute<>, and add new template parameters to Attribute<>. Make
CDAttribute<>s work with context manager.
* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
TypeAttr are now "owned" (defined) by the NodeManager. The
AttributeManager knows nothing of specific attributes, it just as
all the code for dealing generically with attributes.
* test/unit/expr/node_white.h: test new attribute facilities.
* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
away.
* src/theory/Makefile.am: fixed improper linking of theories
* src/theory/theory_engine.h: some implementation work (mainly stubs
for now, just to make sure TheoryUF can be instantiated properly,
etc.)
* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
function implementations to the header and make them inline
* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
function implementations to the header and make them inline
* src/theory/theoryof_table_prologue.h,
src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
src/theory/Makefile.am: make the theoryOf() table from kinds and
implement TheoryEngine::theoryOf().
* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
stub Makefiles (with contrib/addsourcedir) as per policy
* src/theory/arith, src/theory/bool [directory properties]: add .deps
to svn:ignore.
* contrib/configure-in-place: permit configuring "in-place" in the
source directory.
* contrib/get-authors, contrib/dimacs_to_smt.pl,
contrib/update-copyright.pl, contrib/get-authors,
contrib/addsourcedir, src/expr/mkkind: copyright notice
* src/expr/node_manager.h, src/expr/node_builder.h,
src/prop/prop_engine.h, src/prop/prop_engine.cpp,
src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
src/theory/output_channel.h: turn "const Node&"-typed formal
parameters into "TNode"
* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
to avoid keyword clash on containing namespace
* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
src/theory/arith/theory_def.h: "define" a theory simply (for automatic
theoryOf() generator).
* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
src/theory/theoryof_table.h header gets generated before it's needed
* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
separate CVC4::kind namespace to avoid its contents from cluttering
the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace
but not the enum values.
* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
test/unit/expr/node_white.h, test/unit/expr/node_black.h,
test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
update for having moved Kind into CVC4::kind.
* src/parser/parser.cpp: added file-does-not-exist check (was failing
silently).
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 41 |
1 files changed, 22 insertions, 19 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index cd34c415b..0b89fcb5e 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -13,6 +13,9 @@ ** A builder interface for nodes. **/ +/* strong dependency; make sure node is included first */ +#include "node.h" + #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H @@ -145,42 +148,42 @@ public: return Node(d_nv->d_children[i]); } - void clear(Kind k = UNDEFINED_KIND); + void clear(Kind k = kind::UNDEFINED_KIND); // Compound expression constructors /* - NodeBuilder& eqExpr(const Node& right); + NodeBuilder& eqExpr(TNode right); NodeBuilder& notExpr(); - NodeBuilder& andExpr(const Node& right); - NodeBuilder& orExpr(const Node& right); - NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart); - NodeBuilder& iffExpr(const Node& right); - NodeBuilder& impExpr(const Node& right); - NodeBuilder& xorExpr(const Node& right); + NodeBuilder& andExpr(TNode right); + NodeBuilder& orExpr(TNode right); + NodeBuilder& iteExpr(TNode thenpart, TNode elsepart); + NodeBuilder& iffExpr(TNode right); + NodeBuilder& impExpr(TNode right); + NodeBuilder& xorExpr(TNode right); */ /* TODO design: these modify NodeBuilder ?? */ /* NodeBuilder& operator!() { return notExpr(); } - NodeBuilder& operator&&(const Node& right) { return andExpr(right); } - NodeBuilder& operator||(const Node& right) { return orExpr(right); } + NodeBuilder& operator&&(TNode right) { return andExpr(right); } + NodeBuilder& operator||(TNode right) { return orExpr(right); } */ /* - NodeBuilder& operator&&=(const Node& right) { return andExpr(right); } - NodeBuilder& operator||=(const Node& right) { return orExpr(right); } + NodeBuilder& operator&&=(TNode right) { return andExpr(right); } + NodeBuilder& operator||=(TNode right) { return orExpr(right); } */ // "Stream" expression constructor syntax NodeBuilder& operator<<(const Kind& k) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_nv->getKind() == UNDEFINED_KIND); + Assert(d_nv->getKind() == kind::UNDEFINED_KIND); d_nv->d_kind = k; return *this; } - NodeBuilder& operator<<(const Node& n) { + NodeBuilder& operator<<(TNode n) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); return append(n); } @@ -191,7 +194,7 @@ public: return append(children.begin(), children.end()); } - NodeBuilder& append(const Node& n) { + NodeBuilder& append(TNode n) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl; allocateEvIfNecessaryForAppend(); @@ -466,7 +469,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) : d_nv(&d_inlineNv), d_inlineNv(0), d_childrenStorage() { - d_inlineNv.d_kind = UNDEFINED_KIND; + d_inlineNv.d_kind = NodeValue::kindToDKind(kind::UNDEFINED_KIND); } template <unsigned nchild_thresh> @@ -573,16 +576,16 @@ inline void NodeBuilder<nchild_thresh>::dealloc() { template <unsigned nchild_thresh> NodeBuilder<nchild_thresh>::operator Node() {// not const Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_nv->getKind() != UNDEFINED_KIND, + Assert(d_nv->getKind() != kind::UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); - if(d_nv->d_kind == VARIABLE) { + if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); NodeValue *nv = (NodeValue*) std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * d_inlineNv.d_nchildren )); nv->d_nchildren = 0; - nv->d_kind = VARIABLE; + nv->d_kind = kind::VARIABLE; nv->d_id = NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; d_used = true; |