diff options
Diffstat (limited to 'test/unit/expr/node_manager_white.h')
-rw-r--r-- | test/unit/expr/node_manager_white.h | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 99ee171b7..0e5d550a9 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -70,4 +70,24 @@ class NodeManagerWhite : public CxxTest::TestSuite { TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&); #endif /* CVC4_ASSERTIONS */ } + + void testTopologicalSort() + { + TypeNode boolType = d_nm->booleanType(); + Node i = d_nm->mkSkolem("i", boolType); + Node j = d_nm->mkSkolem("j", boolType); + Node n1 = d_nm->mkNode(kind::AND, j, j); + Node n2 = d_nm->mkNode(kind::AND, i, n1); + + { + std::vector<NodeValue*> roots = {n1.d_nv}; + TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), roots); + } + + { + std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv}; + std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv}; + TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), result); + } + } }; |