diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-11 14:00:27 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-11 14:00:27 +0000 |
| commit | 57790a14676596e8c6ed42ff7ecd8038ddbaf09b (patch) | |
| tree | 7e4d5c81f197beab924092fb72cc945d48a47e69 /src/expr/node.h | |
| parent | 5181426cd8def23d67b69227fff033ef12850e68 (diff) | |
Added some ITE rewrites,
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 37499c3bf..4d39ec60f 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -848,6 +848,7 @@ public: NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const; NodeTemplate<true> notNode() const; + NodeTemplate<true> negate() const; template <bool ref_count2> NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const; template <bool ref_count2> @@ -1118,6 +1119,12 @@ NodeTemplate<true> NodeTemplate<ref_count>::notNode() const { } template <bool ref_count> +NodeTemplate<true> NodeTemplate<ref_count>::negate() const { + assertTNodeNotExpired(); + return (getKind() == kind::NOT) ? NodeTemplate<true>(d_nv->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT, *this); +} + +template <bool ref_count> template <bool ref_count2> NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const { @@ -1235,6 +1242,9 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const template <bool ref_count> inline Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { + if (node == *this) { + return replacement; + } std::hash_map<TNode, TNode, TNodeHashFunction> cache; return substitute(node, replacement, cache); } @@ -1243,6 +1253,12 @@ template <bool ref_count> Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + Assert(node != *this); + + if (getNumChildren() == 0) { + return *this; + } + // in cache? typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { @@ -1268,6 +1284,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, // put in cache Node n = nb; + Assert(node != n); cache[*this] = n; return n; } |