diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-02 10:17:09 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-02 10:17:09 -0600 |
| commit | 57b54a2eba7904652dfaf7e32b4eac8abd22c79b (patch) | |
| tree | 79e8ef9e722f62b48ee948a0cce9078afff7f2f0 /test/unit/expr/node_black.h | |
| parent | 5151238c98492fe332a2603c05752f3319ae8035 (diff) | |
Use new let binding for cvc printer (#5561)
Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used.
Diffstat (limited to 'test/unit/expr/node_black.h')
| -rw-r--r-- | test/unit/expr/node_black.h | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 5b82e0a58..4e4a39654 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -631,31 +631,6 @@ class NodeBlack : public CxxTest::TestSuite { TS_ASSERT(sstr.str() == "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = " "y) OR (f(g(x)) = g(y))"); - - sstr.str(string()); - sstr << Node::dag(true) << n; // always dagify - TS_ASSERT(sstr.str() == - "LET _let_0 = f(x), _let_1 = g(x), _let_2 = f(f(_let_0)) IN " - "(_let_2 = x) OR (_let_2 = y) OR (_let_0 = _let_1) OR (x = y) OR " - "(f(_let_1) = g(y))"); - - sstr.str(string()); - sstr << Node::dag(2) << n; // dagify subexprs occurring > 2 times - TS_ASSERT(sstr.str() == - "LET _let_0 = f(x) IN (f(f(_let_0)) = x) OR (f(f(_let_0)) = y) " - "OR (_let_0 = g(x)) OR (x = y) OR (f(g(x)) = g(y))"); - - Warning() << Node::setdepth(-1) - << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) - << n << std::endl; - sstr.str(string()); - sstr << Node::dag(3) << n; // dagify subexprs occurring > 3 times - TS_ASSERT(sstr.str() == - "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = " - "y) OR (f(g(x)) = g(y))"); - Warning() << Node::setdepth(-1) - << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) - << n << std::endl; } void testForEachOverNodeAsNodes() { |