diff options
Diffstat (limited to 'test/unit/expr')
-rw-r--r-- | test/unit/expr/attribute_black.h | 32 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 2 | ||||
-rw-r--r-- | test/unit/expr/expr_manager_public.h | 88 | ||||
-rw-r--r-- | test/unit/expr/expr_public.h | 52 | ||||
-rw-r--r-- | test/unit/expr/kind_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/kind_map_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_algorithm_black.h | 115 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 4 | ||||
-rw-r--r-- | test/unit/expr/node_manager_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_manager_white.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_self_iterator_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_traversal_black.h | 50 | ||||
-rw-r--r-- | test/unit/expr/node_white.h | 2 | ||||
-rw-r--r-- | test/unit/expr/symbol_table_black.h | 16 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 20 | ||||
-rw-r--r-- | test/unit/expr/type_node_white.h | 2 |
17 files changed, 260 insertions, 135 deletions
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index c8b0df1bc..f671fc869 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,15 +17,16 @@ #include <cxxtest/TestSuite.h> //Used in some of the tests -#include <vector> #include <sstream> +#include <vector> +#include "api/cvc4cpp.h" +#include "expr/attribute.h" #include "expr/expr_manager.h" -#include "expr/node_value.h" +#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" -#include "expr/attribute.h" +#include "expr/node_value.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -35,27 +36,20 @@ using namespace CVC4::smt; using namespace std; class AttributeBlack : public CxxTest::TestSuite { -private: - - ExprManager* d_exprManager; - NodeManager* d_nodeManager; - SmtEngine* d_smtEngine; - SmtScope* d_scope; - public: void setUp() override { - d_exprManager = new ExprManager(); + d_slv = new api::Solver(); + d_exprManager = d_slv->getExprManager(); d_nodeManager = NodeManager::fromExprManager(d_exprManager); - d_smtEngine = new SmtEngine(d_exprManager); + d_smtEngine = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smtEngine); } void tearDown() override { delete d_scope; - delete d_smtEngine; - delete d_exprManager; + delete d_slv; } struct PrimitiveIntAttributeId {}; @@ -135,4 +129,10 @@ private: delete node; } + private: + api::Solver* d_slv; + ExprManager* d_exprManager; + NodeManager* d_nodeManager; + SmtEngine* d_smtEngine; + SmtScope* d_scope; }; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 745264b83..89326ab98 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index 8c297232c..c632b913e 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,56 +19,28 @@ #include <sstream> #include <string> -#include "expr/expr_manager.h" -#include "expr/expr.h" +#include "api/cvc4cpp.h" #include "base/exception.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" using namespace CVC4; using namespace CVC4::kind; using namespace std; class ExprManagerPublic : public CxxTest::TestSuite { -private: - - ExprManager* d_exprManager; - - void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) { - std::vector<Expr> worklist; - worklist.push_back(expr); - - unsigned int childrenFound = 0; - - while( !worklist.empty() ) { - Expr current = worklist.back(); - worklist.pop_back(); - if( current.getKind() == kind ) { - for( unsigned int i = 0; i < current.getNumChildren(); ++i ) { - worklist.push_back( current[i] ); - } - } else { - childrenFound++; - } - } - - TS_ASSERT_EQUALS( childrenFound, numChildren ); - } - - std::vector<Expr> mkVars(Type type, unsigned int n) { - std::vector<Expr> vars; - for( unsigned int i = 0; i < n; ++i ) { - vars.push_back( d_exprManager->mkVar(type) ); - } - return vars; - } - public: - void setUp() override { d_exprManager = new ExprManager; } + void setUp() override + { + d_slv = new api::Solver(); + d_exprManager = d_slv->getExprManager(); + } void tearDown() override { try { - delete d_exprManager; + delete d_slv; } catch (Exception& e) { @@ -128,4 +100,44 @@ private: IllegalArgumentException&); } + private: + void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) + { + std::vector<Expr> worklist; + worklist.push_back(expr); + + unsigned int childrenFound = 0; + + while (!worklist.empty()) + { + Expr current = worklist.back(); + worklist.pop_back(); + if (current.getKind() == kind) + { + for (unsigned int i = 0; i < current.getNumChildren(); ++i) + { + worklist.push_back(current[i]); + } + } + else + { + childrenFound++; + } + } + + TS_ASSERT_EQUALS(childrenFound, numChildren); + } + + std::vector<Expr> mkVars(Type type, unsigned int n) + { + std::vector<Expr> vars; + for (unsigned int i = 0; i < n; ++i) + { + vars.push_back(d_exprManager->mkVar(type)); + } + return vars; + } + + api::Solver* d_slv; + ExprManager* d_exprManager; }; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index ce1a23655..86de45fe9 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,9 +19,10 @@ #include <sstream> #include <string> +#include "api/cvc4cpp.h" #include "base/exception.h" -#include "expr/expr_manager.h" #include "expr/expr.h" +#include "expr/expr_manager.h" #include "options/options.h" using namespace CVC4; @@ -29,27 +30,6 @@ using namespace CVC4::kind; using namespace std; class ExprPublic : public CxxTest::TestSuite { -private: - - Options opts; - - ExprManager* d_em; - - Expr* a_bool; - Expr* b_bool; - Expr* c_bool_and; - Expr* and_op; - Expr* plus_op; - Type* fun_type; - Expr* fun_op; - Expr* d_apply_fun_bool; - Expr* null; - - Expr* i1; - Expr* i2; - Expr* r1; - Expr* r2; - public: void setUp() override { @@ -62,7 +42,8 @@ private: free(argv[0]); free(argv[1]); - d_em = new ExprManager(opts); + d_slv = new api::Solver(&opts); + d_em = d_slv->getExprManager(); a_bool = new Expr(d_em->mkVar("a", d_em->booleanType())); b_bool = new Expr(d_em->mkVar("b", d_em->booleanType())); @@ -105,7 +86,7 @@ private: delete b_bool; delete a_bool; - delete d_em; + delete d_slv; } catch (Exception& e) { @@ -466,4 +447,25 @@ private: TS_ASSERT(r1->getExprManager() == d_em); TS_ASSERT(r2->getExprManager() == d_em); } + + private: + Options opts; + + api::Solver* d_slv; + ExprManager* d_em; + + Expr* a_bool; + Expr* b_bool; + Expr* c_bool_and; + Expr* and_op; + Expr* plus_op; + Type* fun_type; + Expr* fun_op; + Expr* d_apply_fun_bool; + Expr* null; + + Expr* i1; + Expr* i2; + Expr* r1; + Expr* r2; }; diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index d1b777c0d..9bae598e2 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h index e03b11b1e..cb7b4f33f 100644 --- a/test/unit/expr/kind_map_black.h +++ b/test/unit/expr/kind_map_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h index 2151eef72..7505215e7 100644 --- a/test/unit/expr/node_algorithm_black.h +++ b/test/unit/expr/node_algorithm_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -24,6 +24,7 @@ #include "expr/node_manager.h" #include "util/integer.h" #include "util/rational.h" +#include "theory/bv/theory_bv_utils.h" using namespace CVC4; using namespace CVC4::expr; @@ -31,12 +32,6 @@ using namespace CVC4::kind; class NodeAlgorithmBlack : public CxxTest::TestSuite { - private: - NodeManager* d_nodeManager; - NodeManagerScope* d_scope; - TypeNode* d_intTypeNode; - TypeNode* d_boolTypeNode; - public: void setUp() override { @@ -44,12 +39,14 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite d_scope = new NodeManagerScope(d_nodeManager); d_intTypeNode = new TypeNode(d_nodeManager->integerType()); d_boolTypeNode = new TypeNode(d_nodeManager->booleanType()); + d_bvTypeNode = new TypeNode(d_nodeManager->mkBitVectorType(2)); } void tearDown() override { - delete d_intTypeNode; + delete d_bvTypeNode; delete d_boolTypeNode; + delete d_intTypeNode; delete d_scope; delete d_nodeManager; } @@ -107,16 +104,24 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); Node plus = d_nodeManager->mkNode(PLUS, x, x); Node mul = d_nodeManager->mkNode(MULT, x, x); - Node eq = d_nodeManager->mkNode(EQUAL, plus, mul); + Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4)); + Node ext1 = theory::bv::utils::mkExtract(y, 1, 0); + Node ext2 = theory::bv::utils::mkExtract(y, 3, 2); + Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2); + + Node formula = d_nodeManager->mkNode(AND, eq1, eq2); + // call function - expr::getOperatorsMap(eq, result); + expr::getOperatorsMap(formula, result); // Verify result - // We should have only integer and boolean as types - TS_ASSERT(result.size() == 2); + // We should have only integer, bv and boolean as types + TS_ASSERT(result.size() == 3); TS_ASSERT(result.find(*d_intTypeNode) != result.end()); TS_ASSERT(result.find(*d_boolTypeNode) != result.end()); + TS_ASSERT(result.find(*d_bvTypeNode) != result.end()); // in integers, we should only have plus and mult as operators TS_ASSERT(result[*d_intTypeNode].size() == 2); @@ -125,9 +130,91 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite TS_ASSERT(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)) != result[*d_intTypeNode].end()); - // in booleans, we should only have "=" as an operator. - TS_ASSERT(result[*d_boolTypeNode].size() == 1); + // in booleans, we should only have "=" and "and" as an operator. + TS_ASSERT(result[*d_boolTypeNode].size() == 2); TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)) != result[*d_boolTypeNode].end()); + TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)) + != result[*d_boolTypeNode].end()); + + //in bv, we should only have "extract" as an operator. + TS_ASSERT(result[*d_boolTypeNode].size() == 2); + Node extractOp1 = d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0)); + Node extractOp2 = d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2)); + TS_ASSERT(result[*d_bvTypeNode].find(extractOp1) + != result[*d_bvTypeNode].end()); + TS_ASSERT(result[*d_bvTypeNode].find(extractOp2) + != result[*d_bvTypeNode].end()); } + + void testMatch() + { + TypeNode integer = d_nodeManager->integerType(); + + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + + Node x = d_nodeManager->mkBoundVar(integer); + Node a = d_nodeManager->mkSkolem("a", integer); + + Node n1 = d_nodeManager->mkNode(MULT, two, x); + std::unordered_map<Node, Node, NodeHashFunction> subs; + + // check reflexivity + TS_ASSERT(match(n1, n1, subs)); + TS_ASSERT_EQUALS(subs.size(), 0); + + Node n2 = d_nodeManager->mkNode(MULT, two, a); + subs.clear(); + + // check instance + TS_ASSERT(match(n1, n2, subs)); + TS_ASSERT_EQUALS(subs.size(), 1); + TS_ASSERT_EQUALS(subs[x], a); + + // should return false for flipped arguments (match is not symmetric) + TS_ASSERT(!match(n2, n1, subs)); + + n2 = d_nodeManager->mkNode(MULT, one, a); + + // should return false since n2 is not an instance of n1 + TS_ASSERT(!match(n1, n2, subs)); + + n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a); + + // should return false for similar operators + TS_ASSERT(!match(n1, n2, subs)); + + n2 = d_nodeManager->mkNode(MULT, two, a, one); + + // should return false for different number of arguments + TS_ASSERT(!match(n1, n2, subs)); + + n1 = x; + n2 = d_nodeManager->mkConst(true); + + // should return false for different types + TS_ASSERT(!match(n1, n2, subs)); + + n1 = d_nodeManager->mkNode(MULT, x, x); + n2 = d_nodeManager->mkNode(MULT, two, a); + + // should return false for contradictory substitutions + TS_ASSERT(!match(n1, n2, subs)); + + n2 = d_nodeManager->mkNode(MULT, a, a); + subs.clear(); + + // implementation: check if the cache works correctly + TS_ASSERT(match(n1, n2, subs)); + TS_ASSERT_EQUALS(subs.size(), 1); + TS_ASSERT_EQUALS(subs[x], a); + } + + private: + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; + TypeNode* d_intTypeNode; + TypeNode* d_boolTypeNode; + TypeNode* d_bvTypeNode; }; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 5aafaeaa2..1b8a7c92f 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 473557e07..c179b76ee 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -2,9 +2,9 @@ /*! \file node_builder_black.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andres Noetzli + ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 4b9c42bd0..84d8fc957 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 6f7729f74..161b2ccae 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index d4e9e551a..10415c8a2 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Christopher L. Conway, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/node_traversal_black.h b/test/unit/expr/node_traversal_black.h index b751a0999..6f5dfaf04 100644 --- a/test/unit/expr/node_traversal_black.h +++ b/test/unit/expr/node_traversal_black.h @@ -2,7 +2,7 @@ /*! \file node_traversal_black.h ** \verbatim ** Top contributors (to current version): - ** Alex Ozdemir + ** Alex Ozdemir, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -58,7 +58,7 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - auto traversal = NodeDfsIterable(cnd).inPostorder(); + auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER); NodeDfsIterator i = traversal.begin(); NodeDfsIterator end = traversal.end(); TS_ASSERT_EQUALS(*i, tb); @@ -79,7 +79,7 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - auto traversal = NodeDfsIterable(cnd).inPostorder(); + auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER); NodeDfsIterator i = traversal.begin(); NodeDfsIterator end = traversal.end(); TS_ASSERT_EQUALS(*(i++), tb); @@ -108,7 +108,7 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node cnd = d_nodeManager->mkNode(XOR, tb, eb); size_t count = 0; - for (auto i : NodeDfsIterable(cnd).inPostorder()) + for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER)) { ++count; } @@ -122,7 +122,7 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node cnd = d_nodeManager->mkNode(XOR, tb, eb); size_t count = 0; - for (auto i : NodeDfsIterable(cnd).inPostorder()) + for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER)) { if (i.isConst()) { @@ -139,7 +139,7 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node top = d_nodeManager->mkNode(XOR, cnd, cnd); - auto traversal = NodeDfsIterable(top).inPostorder(); + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER); size_t count = std::count_if(traversal.begin(), traversal.end(), @@ -155,7 +155,7 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node top = d_nodeManager->mkNode(XOR, cnd, cnd); std::vector<TNode> expected = {tb, eb, cnd, top}; - auto traversal = NodeDfsIterable(top).inPostorder(); + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER); std::vector<TNode> actual; std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); @@ -170,8 +170,24 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite Node top = d_nodeManager->mkNode(XOR, cnd, cnd); std::vector<TNode> expected = {top}; - auto traversal = NodeDfsIterable(top).inPostorder().skipIf( - [&cnd](TNode n) { return n == cnd; }); + auto traversal = NodeDfsIterable( + top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; }); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + TS_ASSERT_EQUALS(actual, expected); + } + + void testSkipAll() + { + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); + Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {}; + + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER, + [](TNode n) { return true; }); std::vector<TNode> actual; std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); @@ -204,7 +220,7 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - auto traversal = NodeDfsIterable(cnd).inPreorder(); + auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER); NodeDfsIterator i = traversal.begin(); NodeDfsIterator end = traversal.end(); TS_ASSERT_EQUALS(*i, cnd); @@ -225,7 +241,7 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - auto traversal = NodeDfsIterable(cnd).inPreorder(); + auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER); NodeDfsIterator i = traversal.begin(); NodeDfsIterator end = traversal.end(); TS_ASSERT_EQUALS(*(i++), cnd); @@ -241,7 +257,7 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node cnd = d_nodeManager->mkNode(XOR, tb, eb); size_t count = 0; - for (auto i : NodeDfsIterable(cnd).inPreorder()) + for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER)) { ++count; } @@ -255,7 +271,7 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node cnd = d_nodeManager->mkNode(XOR, tb, eb); size_t count = 0; - for (auto i : NodeDfsIterable(cnd).inPreorder()) + for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER)) { if (i.isConst()) { @@ -272,7 +288,7 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node top = d_nodeManager->mkNode(XOR, cnd, cnd); - auto traversal = NodeDfsIterable(top).inPreorder(); + auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER); size_t count = std::count_if(traversal.begin(), traversal.end(), @@ -288,7 +304,7 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node top = d_nodeManager->mkNode(XOR, cnd, cnd); std::vector<TNode> expected = {top, cnd, tb, eb}; - auto traversal = NodeDfsIterable(top).inPreorder(); + auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER); std::vector<TNode> actual; std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); @@ -303,8 +319,8 @@ class NodePreorderTraversalBlack : public CxxTest::TestSuite Node top = d_nodeManager->mkNode(XOR, cnd, cnd); std::vector<TNode> expected = {top, cnd, eb}; - auto traversal = NodeDfsIterable(top).inPreorder().skipIf( - [&tb](TNode n) { return n == tb; }); + auto traversal = NodeDfsIterable( + top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; }); std::vector<TNode> actual; std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index c95c46e02..b8f50d5e8 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 1ac1fa315..12a55560d 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,6 +19,7 @@ #include <sstream> #include <string> +#include "api/cvc4cpp.h" #include "base/check.h" #include "base/exception.h" #include "context/context.h" @@ -33,16 +34,13 @@ using namespace CVC4::context; using namespace std; class SymbolTableBlack : public CxxTest::TestSuite { -private: - - ExprManager* d_exprManager; - public: void setUp() override { try { - d_exprManager = new ExprManager; + d_slv = new api::Solver(); + d_exprManager = d_slv->getExprManager(); } catch (Exception& e) { @@ -54,7 +52,7 @@ private: void tearDown() override { try { - delete d_exprManager; + delete d_slv; } catch (Exception& e) { @@ -164,4 +162,8 @@ private: // TODO: What kind of exception gets thrown here? TS_ASSERT_THROWS(symtab.popScope(), ScopeException&); } + + private: + api::Solver* d_slv; + ExprManager* d_exprManager; };/* class SymbolTableBlack */ diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 39e528c43..49d6bd9fd 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,12 +17,13 @@ #include <cxxtest/TestSuite.h> #include <iostream> -#include <string> #include <sstream> +#include <string> +#include "api/cvc4cpp.h" +#include "expr/expr_manager.h" #include "expr/kind.h" #include "expr/type.h" -#include "expr/expr_manager.h" #include "util/cardinality.h" using namespace CVC4; @@ -30,12 +31,14 @@ using namespace CVC4::kind; using namespace std; class TypeCardinalityPublic : public CxxTest::TestSuite { - ExprManager* d_em; - public: - void setUp() override { d_em = new ExprManager(); } + void setUp() override + { + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); + } - void tearDown() override { delete d_em; } + void tearDown() override { delete d_slv; } void testTheBasics() { @@ -226,4 +229,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite { } } + private: + api::Solver* d_slv; + ExprManager* d_em; };/* TypeCardinalityPublic */ diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index ebd2a718a..8a5722f2e 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim |