diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/expr/node.h | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index c9bfb75a4..6dbb5aa2b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -893,8 +893,6 @@ public: NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart, const NodeTemplate<ref_count3>& elsepart) const; template <bool ref_count2> - NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const; - template <bool ref_count2> NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const; template <bool ref_count2> NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const; @@ -1203,14 +1201,6 @@ NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart, template <bool ref_count> template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const { - assertTNodeNotExpired(); - return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); -} - -template <bool ref_count> -template <bool ref_count2> -NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); |