diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-01-26 15:06:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-01-26 15:06:24 +0000 |
commit | b3d0ea6ed6d92943d9a52abbe30e944e9887516d (patch) | |
tree | 0330893fa4e129bab8341765e66b279382fddbbf /src/expr | |
parent | 21e01d42ed4c0b6d9fa5855c2e0cfc1a3765d14f (diff) |
cnf conversion
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_builder.h | 2 | ||||
-rw-r--r-- | src/expr/node_value.h | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 747854d23..13aa0b0ff 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -390,7 +390,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& d_childrenStorage() { if(evIsAllocated(nb)) { - realloc(nb->d_size, false); + realloc(nb.d_size, false); std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin()); } else { std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin()); diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 985ad15a7..84df5957a 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -29,6 +29,7 @@ #include "kind.h" #include <string> +#include <iterator> namespace CVC4 { @@ -142,6 +143,12 @@ class NodeValue { node_iterator operator++(int) { return node_iterator(d_i++); } + + typedef std::input_iterator_tag iterator_category; + typedef Node value_type; + typedef ptrdiff_t difference_type; + typedef Node* pointer; + typedef Node& reference; }; typedef node_iterator const_node_iterator; |