diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/api/ouroborous.cpp | 2 | ||||
-rw-r--r-- | test/api/smt2_compliance.cpp | 1 | ||||
-rw-r--r-- | test/unit/expr/node_black.cpp | 1 | ||||
-rw-r--r-- | test/unit/expr/node_traversal_black.cpp | 1 | ||||
-rw-r--r-- | test/unit/expr/symbol_table_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_black.cpp | 1 | ||||
-rw-r--r-- | test/unit/expr/type_node_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/main/interactive_shell_black.cpp | 1 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/test_node.h | 2 | ||||
-rw-r--r-- | test/unit/test_smt.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.cpp | 26 | ||||
-rw-r--r-- | test/unit/util/array_store_all_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/util/datatype_black.cpp | 2 |
15 files changed, 18 insertions, 35 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 442a57e34..7b42d6a76 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -29,8 +29,6 @@ #include <string> #include "api/cvc4cpp.h" -#include "expr/expr.h" -#include "expr/expr_iomanip.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index c008018b2..223028d4c 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -19,7 +19,6 @@ #include <sstream> #include "api/cvc4cpp.h" -#include "expr/expr_manager.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp index b536fb932..3c1651155 100644 --- a/test/unit/expr/node_black.cpp +++ b/test/unit/expr/node_black.cpp @@ -22,7 +22,6 @@ #include "api/cvc4cpp.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" diff --git a/test/unit/expr/node_traversal_black.cpp b/test/unit/expr/node_traversal_black.cpp index 1c18abdb5..e443ff685 100644 --- a/test/unit/expr/node_traversal_black.cpp +++ b/test/unit/expr/node_traversal_black.cpp @@ -19,7 +19,6 @@ #include <string> #include <vector> -#include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" diff --git a/test/unit/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp index 68b822bac..10fb52f6d 100644 --- a/test/unit/expr/symbol_table_black.cpp +++ b/test/unit/expr/symbol_table_black.cpp @@ -20,10 +20,8 @@ #include "base/check.h" #include "base/exception.h" #include "context/context.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/kind.h" #include "expr/symbol_table.h" -#include "expr/type.h" #include "test_api.h" namespace CVC4 { diff --git a/test/unit/expr/type_cardinality_black.cpp b/test/unit/expr/type_cardinality_black.cpp index 08e863bc4..58024fa53 100644 --- a/test/unit/expr/type_cardinality_black.cpp +++ b/test/unit/expr/type_cardinality_black.cpp @@ -18,7 +18,6 @@ #include "expr/kind.h" #include "expr/node_manager.h" -#include "expr/type.h" #include "test_node.h" #include "util/cardinality.h" diff --git a/test/unit/expr/type_node_white.cpp b/test/unit/expr/type_node_white.cpp index 4412ec95a..f364e40fc 100644 --- a/test/unit/expr/type_node_white.cpp +++ b/test/unit/expr/type_node_white.cpp @@ -18,8 +18,6 @@ #include <sstream> #include <string> -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "expr/node_manager.h" #include "expr/type_node.h" #include "smt/smt_engine.h" diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index b35f07f18..c600e3477 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -18,7 +18,6 @@ #include <vector> #include "api/cvc4cpp.h" -#include "expr/expr_manager.h" #include "expr/symbol_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index ece6168e9..87556d53d 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -19,8 +19,6 @@ #include "api/cvc4cpp.h" #include "base/output.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "expr/symbol_manager.h" #include "options/base_options.h" #include "options/language.h" diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 978914d3e..cf343f006 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -28,7 +28,7 @@ class TestNode : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager(nullptr)); + d_nodeManager.reset(new NodeManager()); d_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 718a9d2b6..e55c00e65 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -41,7 +41,7 @@ class TestSmt : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager(nullptr)); + d_nodeManager.reset(new NodeManager()); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); d_smtEngine->finishInit(); @@ -57,7 +57,7 @@ class TestSmtNoFinishInit : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager(nullptr)); + d_nodeManager.reset(new NodeManager()); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); } diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 6952fb320..1447670f3 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -86,7 +86,7 @@ TEST_F(TestTheoryWhiteBv, mkUmulo) kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w)); Node rhs = mkUmulo(x, y); Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs); - d_smtEngine->assertFormula(eq.toExpr()); + d_smtEngine->assertFormula(eq); Result res = d_smtEngine->checkSat(); ASSERT_EQ(res.isSat(), Result::UNSAT); d_smtEngine->pop(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 54b4ce55b..7b6a73d2c 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -88,7 +88,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit } Node body = d_nodeManager->mkNode(k, x, d_t); Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, body); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); ASSERT_EQ(res.d_sat, Result::UNSAT); } @@ -117,14 +117,14 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit litk, d_nodeManager->mkNode(k, d_s, d_x), d_t); Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode()); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; - std::cout << "s " << d_smtEngine->getValue(d_s.toExpr()) << std::endl; - std::cout << "t " << d_smtEngine->getValue(d_t.toExpr()) << std::endl; - std::cout << "x " << d_smtEngine->getValue(d_x.toExpr()) << std::endl; + std::cout << "s " << d_smtEngine->getValue(d_s) << std::endl; + std::cout << "t " << d_smtEngine->getValue(d_t) << std::endl; + std::cout << "x " << d_smtEngine->getValue(d_x) << std::endl; } ASSERT_EQ(res.d_sat, Result::UNSAT); } @@ -173,17 +173,17 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x}); Node scr = d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode()); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; if (!s1.isNull()) - std::cout << "s1 " << d_smtEngine->getValue(s1.toExpr()) << std::endl; + std::cout << "s1 " << d_smtEngine->getValue(s1) << std::endl; if (!s2.isNull()) - std::cout << "s2 " << d_smtEngine->getValue(s2.toExpr()) << std::endl; - std::cout << "t " << d_smtEngine->getValue(t.toExpr()) << std::endl; - std::cout << "x " << d_smtEngine->getValue(x.toExpr()) << std::endl; + std::cout << "s2 " << d_smtEngine->getValue(s2) << std::endl; + std::cout << "t " << d_smtEngine->getValue(t) << std::endl; + std::cout << "x " << d_smtEngine->getValue(x) << std::endl; } ASSERT_TRUE(res.d_sat == Result::UNSAT); } @@ -213,13 +213,13 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x}); Node scr = d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode()); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; - std::cout << "t " << d_smtEngine->getValue(t.toExpr()) << std::endl; - std::cout << "x " << d_smtEngine->getValue(x.toExpr()) << std::endl; + std::cout << "t " << d_smtEngine->getValue(t) << std::endl; + std::cout << "x " << d_smtEngine->getValue(x) << std::endl; } ASSERT_TRUE(res.d_sat == Result::UNSAT); } diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 693bc0423..540fca6f2 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -15,8 +15,6 @@ **/ #include "expr/array_store_all.h" -#include "expr/expr.h" -#include "expr/type.h" #include "test_smt.h" namespace CVC4 { diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 18dc479be..ef24d870d 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -16,10 +16,8 @@ #include <sstream> -#include "api/cvc4cpp.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/expr.h" #include "expr/type_node.h" #include "test_smt.h" |