summaryrefslogtreecommitdiff
path: root/test/unit/expr
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/expr')
-rw-r--r--test/unit/expr/attribute_black.h32
-rw-r--r--test/unit/expr/attribute_white.h2
-rw-r--r--test/unit/expr/expr_manager_public.h88
-rw-r--r--test/unit/expr/expr_public.h52
-rw-r--r--test/unit/expr/kind_black.h2
-rw-r--r--test/unit/expr/kind_map_black.h2
-rw-r--r--test/unit/expr/node_algorithm_black.h115
-rw-r--r--test/unit/expr/node_black.h2
-rw-r--r--test/unit/expr/node_builder_black.h4
-rw-r--r--test/unit/expr/node_manager_black.h2
-rw-r--r--test/unit/expr/node_manager_white.h2
-rw-r--r--test/unit/expr/node_self_iterator_black.h2
-rw-r--r--test/unit/expr/node_traversal_black.h50
-rw-r--r--test/unit/expr/node_white.h2
-rw-r--r--test/unit/expr/symbol_table_black.h16
-rw-r--r--test/unit/expr/type_cardinality_public.h20
-rw-r--r--test/unit/expr/type_node_white.h2
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback