diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-29 15:35:44 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 17:35:44 -0500 |
commit | 19054b3b1d427e662d30d4322df2b2f2361353da (patch) | |
tree | 1ee878fd6c2c36b78ea33607a5668e6a6d8f7144 /test/unit | |
parent | 5cd6f0e5e910ad61ebc5045170842078818a3b80 (diff) |
Make ExprManager constructor private (#4669)
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/expr/attribute_black.h | 30 | ||||
-rw-r--r-- | test/unit/expr/expr_manager_public.h | 86 | ||||
-rw-r--r-- | test/unit/expr/expr_public.h | 50 | ||||
-rw-r--r-- | test/unit/expr/symbol_table_black.h | 14 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 18 | ||||
-rw-r--r-- | test/unit/theory/regexp_operation_black.h | 21 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 16 | ||||
-rw-r--r-- | test/unit/util/array_store_all_black.h | 14 | ||||
-rw-r--r-- | test/unit/util/datatype_black.h | 15 |
9 files changed, 147 insertions, 117 deletions
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index f07612119..f671fc869 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -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/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index d28553e08..c632b913e 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -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 09452cc7a..86de45fe9 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -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/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 17bab05a4..12a55560d 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -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 29d9f5dc2..49d6bd9fd 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -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/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h index f42207c49..6e01392ab 100644 --- a/test/unit/theory/regexp_operation_black.h +++ b/test/unit/theory/regexp_operation_black.h @@ -14,17 +14,19 @@ ** Unit tests for symbolic regular expression operations. **/ +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <memory> +#include <vector> + +#include "api/cvc4cpp.h" #include "expr/node.h" #include "expr/node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/strings/regexp_operation.h" -#include <cxxtest/TestSuite.h> -#include <iostream> -#include <memory> -#include <vector> - using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::smt; @@ -40,8 +42,9 @@ class RegexpOperationBlack : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); + d_smt = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smt); d_regExpOpr = new RegExpOpr(); @@ -56,8 +59,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite { delete d_regExpOpr; delete d_scope; - delete d_smt; - delete d_em; + delete d_slv; } void includes(Node r1, Node r2) @@ -147,6 +149,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite } private: + api::Solver* d_slv; ExprManager* d_em; SmtEngine* d_smt; SmtScope* d_scope; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 37999b73a..45d13d416 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -17,14 +17,15 @@ #include <cxxtest/TestSuite.h> //Used in some of the tests -#include <vector> #include <sstream> +#include <vector> +#include "api/cvc4cpp.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/node_value.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/rewriter.h" @@ -40,8 +41,9 @@ class TheoryBlack : public CxxTest::TestSuite { public: void setUp() override { - d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); + d_smt = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smt); // Ensure that the SMT engine is fully initialized (required for the // rewriter) @@ -53,8 +55,7 @@ class TheoryBlack : public CxxTest::TestSuite { void tearDown() override { delete d_scope; - delete d_smt; - delete d_em; + delete d_slv; } void testArrayConst() { @@ -149,6 +150,7 @@ class TheoryBlack : public CxxTest::TestSuite { } private: + api::Solver* d_slv; ExprManager* d_em; SmtEngine* d_smt; NodeManager* d_nm; diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 3b00fa192..bf0163317 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -16,6 +16,7 @@ #include <cxxtest/TestSuite.h> +#include "api/cvc4cpp.h" #include "expr/array_store_all.h" #include "expr/expr.h" #include "expr/expr_manager.h" @@ -27,18 +28,14 @@ using namespace CVC4; using namespace std; class ArrayStoreAllBlack : public CxxTest::TestSuite { - ExprManager* d_em; - public: void setUp() override { - d_em = new ExprManager(); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); } - void tearDown() override - { - delete d_em; - } + void tearDown() override { delete d_slv; } void testStoreAll() { Type usort = d_em->mkSort("U"); @@ -80,4 +77,7 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite { d_em->mkConst(Rational(0))))); } + private: + api::Solver* d_slv; + ExprManager* d_em; }; /* class ArrayStoreAllBlack */ diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index f69cc12ea..ac27acfb5 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -15,8 +15,10 @@ **/ #include <cxxtest/TestSuite.h> + #include <sstream> +#include "api/cvc4cpp.h" #include "expr/datatype.h" #include "expr/expr.h" #include "expr/expr_manager.h" @@ -27,14 +29,11 @@ using namespace CVC4; using namespace std; class DatatypeBlack : public CxxTest::TestSuite { - - ExprManager* d_em; - ExprManagerScope* d_scope; - public: void setUp() override { - d_em = new ExprManager(); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); d_scope = new ExprManagerScope(*d_em); Debug.on("datatypes"); Debug.on("groundterms"); @@ -43,7 +42,7 @@ class DatatypeBlack : public CxxTest::TestSuite { void tearDown() override { delete d_scope; - delete d_em; + delete d_slv; } void testEnumeration() { @@ -436,4 +435,8 @@ class DatatypeBlack : public CxxTest::TestSuite { TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt); } + private: + api::Solver* d_slv; + ExprManager* d_em; + ExprManagerScope* d_scope; };/* class DatatypeBlack */ |