From e37d0c385d698d46f14fb30e5a44de63c686fadb Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 16 Jun 2020 13:48:05 -0700 Subject: Update copyright headers. --- test/unit/util/array_store_all_black.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test/unit/util/array_store_all_black.h') diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index c0d1474e9..3b00fa192 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -2,9 +2,9 @@ /*! \file array_store_all_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 -- cgit v1.2.3 From 19054b3b1d427e662d30d4322df2b2f2361353da Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 29 Jun 2020 15:35:44 -0700 Subject: 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. --- examples/CMakeLists.txt | 39 +++++----- examples/api/java/CMakeLists.txt | 29 ++++---- examples/simple_vc_cxx.cpp | 45 ++++++----- examples/simple_vc_quant_cxx.cpp | 79 ++++++++++---------- src/expr/expr_manager_template.h | 9 ++- .../quantifiers/candidate_rewrite_database.cpp | 14 +++- src/theory/quantifiers/expr_miner.cpp | 15 +++- src/theory/quantifiers/expr_miner.h | 4 +- src/theory/quantifiers/query_generator.cpp | 13 +++- .../quantifiers/sygus/cegis_core_connective.cpp | 10 ++- .../quantifiers/sygus/sygus_repair_const.cpp | 76 ++++++++++--------- src/theory/quantifiers/sygus/sygus_repair_const.h | 20 ----- src/theory/quantifiers/sygus/synth_engine.cpp | 5 +- src/theory/smt_engine_subsolver.cpp | 36 ++++++--- src/theory/smt_engine_subsolver.h | 12 +-- test/system/CMakeLists.txt | 2 +- test/system/boilerplate.cpp | 14 ++-- test/system/reset_assertions.cpp | 49 ++++++------ test/system/statistics.cpp | 38 +++++----- test/system/two_smt_engines.cpp | 36 --------- test/system/two_solvers.cpp | 32 ++++++++ test/unit/expr/attribute_black.h | 30 ++++---- test/unit/expr/expr_manager_public.h | 86 ++++++++++++---------- test/unit/expr/expr_public.h | 50 +++++++------ test/unit/expr/symbol_table_black.h | 14 ++-- test/unit/expr/type_cardinality_public.h | 18 +++-- test/unit/theory/regexp_operation_black.h | 21 +++--- test/unit/theory/theory_black.h | 16 ++-- test/unit/util/array_store_all_black.h | 14 ++-- test/unit/util/datatype_black.h | 15 ++-- 30 files changed, 448 insertions(+), 393 deletions(-) delete mode 100644 test/system/two_smt_engines.cpp create mode 100644 test/system/two_solvers.cpp (limited to 'test/unit/util/array_store_all_black.h') diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 6168a8e22..cd74698d7 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -58,31 +58,34 @@ endmacro() cvc4_add_example(simple_vc_cxx "" "") cvc4_add_example(simple_vc_quant_cxx "" "") -cvc4_add_example(translator "" "" - # argument to binary (for testing) - ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) +# TODO(project issue $206): Port example to new API +# cvc4_add_example(translator "" "" +# # argument to binary (for testing) +# ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) add_subdirectory(api) -add_subdirectory(hashsmt) -add_subdirectory(nra-translate) -add_subdirectory(sets-translate) +# TODO(project issue $206): Port example to new API +# add_subdirectory(hashsmt) +# add_subdirectory(nra-translate) +# add_subdirectory(sets-translate) if(TARGET CVC4::cvc4jar) find_package(Java REQUIRED) include(UseJava) - get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE) - - add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}") - - add_test( - NAME java/SimpleVC - COMMAND - ${Java_JAVA_EXECUTABLE} - -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar" - -Djava.library.path=${CVC4_JNI_PATH} - SimpleVC - ) + ## disabled until bindings for the new API are in place (issue #2284) + # get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE) + # + # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}") + # + # add_test( + # NAME java/SimpleVC + # COMMAND + # ${Java_JAVA_EXECUTABLE} + # -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar" + # -Djava.library.path=${CVC4_JNI_PATH} + # SimpleVC + # ) add_subdirectory(api/java) endif() diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 31f62db56..0afcec0e4 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -1,20 +1,19 @@ set(EXAMPLES_API_JAVA - BitVectors - BitVectorsAndArrays ## disabled until bindings for the new API are in place (issue #2284) - #CVC4Streams - Combination - Datatypes - Exceptions - FloatingPointArith - HelloWorld - LinearArith - ## disabled until bindings for the new API are in place (issue #2284) - #PipedInput - Relations - Statistics - Strings - UnsatCores + # BitVectors + # BitVectorsAndArrays + # CVC4Streams + # Combination + # Datatypes + # Exceptions + # FloatingPointArith + # HelloWorld + # LinearArith + # PipedInput + # Relations + # Statistics + # Strings + # UnsatCores ) foreach(example ${EXAMPLES_API_JAVA}) diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 26d785edc..64c2b12c1 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -16,43 +16,42 @@ ** identical. **/ -#include +#include -#include +#include -using namespace std; -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); + Solver slv; // Prove that for integers x and y: // x > 0 AND y > 0 => 2x + y >= 3 - Type integer = em.integerType(); + Sort integer = slv.getIntegerSort(); - Expr x = em.mkVar("x", integer); - Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(Rational(0)); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(integer, "y"); + Term zero = slv.mkReal(0); - Expr x_positive = em.mkExpr(kind::GT, x, zero); - Expr y_positive = em.mkExpr(kind::GT, y, zero); + Term x_positive = slv.mkTerm(Kind::GT, x, zero); + Term y_positive = slv.mkTerm(Kind::GT, y, zero); - Expr two = em.mkConst(Rational(2)); - Expr twox = em.mkExpr(kind::MULT, two, x); - Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); + Term two = slv.mkReal(2); + Term twox = slv.mkTerm(Kind::MULT, two, x); + Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y); - Expr three = em.mkConst(Rational(3)); - Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); + Term three = slv.mkReal(3); + Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); - Expr formula = - em.mkExpr(kind::AND, x_positive, y_positive). - impExpr(twox_plus_y_geq_3); + Term formula = + slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); - cout << "Checking entailment of formula " << formula << " with CVC4." << endl; - cout << "CVC4 should report ENTAILED." << endl; - cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl; + std::cout << "Checking entailment of formula " << formula << " with CVC4." + << std::endl; + std::cout << "CVC4 should report ENTAILED." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula) + << std::endl; return 0; } diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 83d011993..4d5767ebb 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -14,64 +14,63 @@ ** A simple demonstration of the C++ interface for quantifiers. **/ -#include +#include -#include +#include -using namespace std; -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); + Solver slv; // Prove that the following is unsatisfiable: // forall x. P( x ) ^ ~P( 5 ) - Type integer = em.integerType(); - Type boolean = em.booleanType(); - Type integerPredicate = em.mkFunctionType(integer, boolean); - - Expr p = em.mkVar("P", integerPredicate); - Expr x = em.mkBoundVar("x", integer); - + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + Sort integerPredicate = slv.mkFunctionSort(integer, boolean); + + Term p = slv.mkConst(integerPredicate, "P"); + Term x = slv.mkVar(integer, "x"); + // make forall x. P( x ) - Expr var_list = em.mkExpr(kind::BOUND_VAR_LIST, x); - Expr px = em.mkExpr(kind::APPLY_UF, p, x); - Expr quantpospx = em.mkExpr(kind::FORALL, var_list, px); - cout << "Made expression : " << quantpospx << endl; - + Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x); + Term px = slv.mkTerm(Kind::APPLY_UF, p, x); + Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px); + std::cout << "Made expression : " << quantpospx << std::endl; + //make ~P( 5 ) - Expr five = em.mkConst(Rational(5)); - Expr pfive = em.mkExpr(kind::APPLY_UF, p, five); - Expr negpfive = em.mkExpr(kind::NOT, pfive); - cout << "Made expression : " << negpfive << endl; - - Expr formula = em.mkExpr(kind::AND, quantpospx, negpfive); + Term five = slv.mkReal(5); + Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five); + Term negpfive = slv.mkTerm(Kind::NOT, pfive); + std::cout << "Made expression : " << negpfive << std::endl; - smt.assertFormula(formula); + Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive); - cout << "Checking SAT after asserting " << formula << " to CVC4." << endl; - cout << "CVC4 should report unsat." << endl; - cout << "Result from CVC4 is: " << smt.checkSat() << endl; + slv.assertFormula(formula); + std::cout << "Checking SAT after asserting " << formula << " to CVC4." + << std::endl; + std::cout << "CVC4 should report unsat." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; - SmtEngine smtp(&em); - - // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) - Expr pattern = em.mkExpr(kind::INST_PATTERN, px); - Expr pattern_list = em.mkExpr(kind::INST_PATTERN_LIST, pattern); - Expr quantpospx_pattern = em.mkExpr(kind::FORALL, var_list, px, pattern_list); - cout << "Made expression : " << quantpospx_pattern << endl; + slv.resetAssertions(); - Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive); + // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) + Term pattern = slv.mkTerm(Kind::INST_PATTERN, px); + Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern); + Term quantpospx_pattern = + slv.mkTerm(Kind::FORALL, var_list, px, pattern_list); + std::cout << "Made expression : " << quantpospx_pattern << std::endl; - smtp.assertFormula(formula_pattern); + Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive); - cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl; - cout << "CVC4 should report unsat." << endl; - cout << "Result from CVC4 is: " << smtp.checkSat() << endl; + slv.assertFormula(formula_pattern); + std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." + << std::endl; + std::cout << "CVC4 should report unsat." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; return 0; } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 1809eb2d0..3a4498ab7 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -36,6 +36,10 @@ ${includes} namespace CVC4 { +namespace api { +class Solver; +} + class Expr; class SmtEngine; class NodeManager; @@ -45,7 +49,8 @@ struct ExprManagerMapCollection; class ResourceManager; class CVC4_PUBLIC ExprManager { -private: + private: + friend api::Solver; /** The internal node manager */ NodeManager* d_nodeManager; @@ -83,7 +88,6 @@ private: /** A list of datatypes owned by this expr manager. */ std::vector > d_ownedDatatypes; - public: /** * Creates an expression manager with default options. */ @@ -97,6 +101,7 @@ private: */ explicit ExprManager(const Options& options); + public: /** * Destroys the expression manager. No will be deallocated at this point, so * any expression references that used to be managed by this expression diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 0454b6412..fc3474df4 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/candidate_rewrite_database.h" +#include "api/cvc4cpp.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -137,8 +138,15 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // options as the SmtEngine we belong to, where we ensure that // produce-models is set. bool needExport = false; - ExprManager em(nm->getOptions()); - std::unique_ptr rrChecker; + + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // This is only temporarily until we have separate options for each + // SmtEngine instance. We should reuse the same ExprManager with + // a different SmtEngine (and different options) here, eventually. + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + api::Solver slv(&nm->getOptions()); + ExprManager* em = slv.getExprManager(); + SmtEngine* rrChecker = slv.getSmtEngine(); ExprManagerMapCollection varMap; initializeChecker(rrChecker, em, varMap, crr, needExport); Result r = rrChecker->checkSat(); @@ -175,7 +183,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); if (needExport) { - Expr erefv = refv.toExpr().exportTo(&em, varMap); + Expr erefv = refv.toExpr().exportTo(em, varMap); val = Node::fromExpr(rrChecker->getValue(erefv).exportTo( nm->toExprManager(), varMap)); } diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 01a46d84a..b209fc6ff 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/expr_miner.h" +#include "api/cvc4cpp.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -68,8 +69,8 @@ Node ExprMiner::convertToSkolem(Node n) return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end()); } -void ExprMiner::initializeChecker(std::unique_ptr& checker, - ExprManager& em, +void ExprMiner::initializeChecker(SmtEngine* checker, + ExprManager* em, ExprManagerMapCollection& varMap, Node query, bool& needExport) @@ -110,10 +111,16 @@ Result ExprMiner::doCheck(Node query) return Result(Result::SAT); } } + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // This is only temporarily until we have separate options for each + // SmtEngine instance. We should reuse the same ExprManager with + // a different SmtEngine (and different options) here, eventually. + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! NodeManager* nm = NodeManager::currentNM(); bool needExport = false; - ExprManager em(nm->getOptions()); - std::unique_ptr smte; + api::Solver slv(&nm->getOptions()); + ExprManager* em = slv.getExprManager(); + SmtEngine* smte = slv.getSmtEngine(); ExprManagerMapCollection varMap; initializeChecker(smte, em, varMap, queryr, needExport); return smte->checkSat(); diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index d69ef45b4..eebcebf88 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -89,8 +89,8 @@ class ExprMiner * (for instance, model values) must be exported to the current expression * manager. */ - void initializeChecker(std::unique_ptr& smte, - ExprManager& em, + void initializeChecker(SmtEngine* smte, + ExprManager* em, ExprManagerMapCollection& varMap, Node query, bool& needExport); diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 9f08ebec7..4cf65b24a 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/query_generator.h" #include + +#include "api/cvc4cpp.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -157,9 +159,16 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl; NodeManager* nm = NodeManager::currentNM(); // make the satisfiability query + // + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // This is only temporarily until we have separate options for each + // SmtEngine instance. We should reuse the same ExprManager with + // a different SmtEngine (and different options) here, eventually. + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! bool needExport = false; - ExprManager em(nm->getOptions()); - std::unique_ptr queryChecker; + api::Solver slv(&nm->getOptions()); + ExprManager* em = slv.getExprManager(); + SmtEngine* queryChecker = slv.getSmtEngine(); ExprManagerMapCollection varMap; initializeChecker(queryChecker, em, varMap, qy, needExport); Result r = queryChecker->checkSat(); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index de75af083..5784e42c0 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -735,8 +735,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { addSuccess = false; // try a new core - std::unique_ptr checkSol; - initializeSubsolver(checkSol); + std::unique_ptr checkSol( + new SmtEngine(NodeManager::currentNM()->toExprManager())); + initializeSubsolver(checkSol.get()); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector rasserts = asserts; rasserts.push_back(d_sc); @@ -775,8 +776,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { // In terms of Variant #2, this is the check "if S ^ U is unsat" Trace("sygus-ccore") << "----- Check side condition" << std::endl; - std::unique_ptr checkSc; - initializeSubsolver(checkSc); + std::unique_ptr checkSc( + new SmtEngine(NodeManager::currentNM()->toExprManager())); + initializeSubsolver(checkSc.get()); std::vector scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); scasserts.push_back(d_sc); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 1c34bd73a..d34903805 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_repair_const.h" +#include "api/cvc4cpp.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -100,36 +101,6 @@ bool SygusRepairConst::isActive() const return !d_base_inst.isNull() && d_allow_constant_grammar; } -void SygusRepairConst::initializeChecker(std::unique_ptr& checker, - ExprManager& em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport) -{ - if (options::sygusRepairConstTimeout.wasSetByUser()) - { - // To support a separate timeout for the subsolver, we need to create - // a separate ExprManager with its own options. This requires that - // the expressions sent to the subsolver can be exported from on - // ExprManager to another. - initializeSubsolverWithExport(checker, - em, - varMap, - query.toExpr(), - true, - options::sygusRepairConstTimeout()); - // renable options disabled by sygus - checker->setOption("miniscope-quant", true); - checker->setOption("miniscope-quant-fv", true); - checker->setOption("quant-split", true); - } - else - { - needExport = false; - initializeSubsolver(checker, query.toExpr()); - } -} - bool SygusRepairConst::repairSolution(const std::vector& candidates, const std::vector& candidate_values, std::vector& repair_cv, @@ -258,11 +229,48 @@ bool SygusRepairConst::repairSolution(Node sygusBody, Trace("sygus-engine") << "Repairing previous solution..." << std::endl; // make the satisfiability query + // + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // This is only temporarily until we have separate options for each + // SmtEngine instance. We should reuse the same ExprManager with + // a different SmtEngine (and different options) here, eventually. + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! bool needExport = true; + std::unique_ptr simpleSmte; + std::unique_ptr slv; + ExprManager* em = nullptr; + SmtEngine* repcChecker = nullptr; ExprManagerMapCollection varMap; - ExprManager em(nm->getOptions()); - std::unique_ptr repcChecker; - initializeChecker(repcChecker, em, varMap, fo_body, needExport); + + if (options::sygusRepairConstTimeout.wasSetByUser()) + { + // To support a separate timeout for the subsolver, we need to create + // a separate ExprManager with its own options. This requires that + // the expressions sent to the subsolver can be exported from on + // ExprManager to another. + slv.reset(new api::Solver(&nm->getOptions())); + em = slv->getExprManager(); + repcChecker = slv->getSmtEngine(); + initializeSubsolverWithExport(repcChecker, + em, + varMap, + fo_body.toExpr(), + true, + options::sygusRepairConstTimeout()); + // renable options disabled by sygus + repcChecker->setOption("miniscope-quant", true); + repcChecker->setOption("miniscope-quant-fv", true); + repcChecker->setOption("quant-split", true); + } + else + { + needExport = false; + em = nm->toExprManager(); + simpleSmte.reset(new SmtEngine(em)); + repcChecker = simpleSmte.get(); + initializeSubsolver(repcChecker, fo_body.toExpr()); + } + Result r = repcChecker->checkSat(); Trace("sygus-repair-const") << "...got : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT @@ -279,7 +287,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, Node fov_m; if (needExport) { - Expr e_fov = fov.toExpr().exportTo(&em, varMap); + Expr e_fov = fov.toExpr().exportTo(em, varMap); fov_m = Node::fromExpr( repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap)); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index dc721b42d..e02ca1f3e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -209,26 +209,6 @@ class SygusRepairConst * If n is in the given logic, this method returns true. */ bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar); - /** initialize checker - * - * This function initializes the smt engine checker to check the - * satisfiability of the argument "query" - * - * The arguments em and varMap are used for supporting cases where we - * want checker to use a different expression manager instead of the current - * expression manager. The motivation for this so that different options can - * be set for the subcall. - * - * We update the flag needExport to true if checker is using the expression - * manager em. In this case, subsequent expressions extracted from smte - * (for instance, model values) must be exported to the current expression - * manager. - */ - void initializeChecker(std::unique_ptr& checker, - ExprManager& em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f8349c834..590fdaa56 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -169,8 +169,9 @@ void SynthEngine::assignConjecture(Node q) if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) { // create new smt engine to do quantifier elimination - std::unique_ptr smt_qe; - initializeSubsolver(smt_qe); + std::unique_ptr smt_qe( + new SmtEngine(NodeManager::currentNM()->toExprManager())); + initializeSubsolver(smt_qe.get()); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 3386f3691..f529d3fea 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -15,6 +15,7 @@ #include "theory/smt_engine_subsolver.h" +#include "api/cvc4cpp.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/rewriter.h" @@ -40,16 +41,14 @@ Result quickCheck(Node& query) return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); } -void initializeSubsolver(std::unique_ptr& smte) +void initializeSubsolver(SmtEngine* smte) { - NodeManager* nm = NodeManager::currentNM(); - smte.reset(new SmtEngine(nm->toExprManager())); smte->setIsInternalSubsolver(); smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); } -void initializeSubsolverWithExport(std::unique_ptr& smte, - ExprManager& em, +void initializeSubsolverWithExport(SmtEngine* smte, + ExprManager* em, ExprManagerMapCollection& varMap, Node query, bool needsTimeout, @@ -62,14 +61,13 @@ void initializeSubsolverWithExport(std::unique_ptr& smte, // OptionException. try { - smte.reset(new SmtEngine(&em)); smte->setIsInternalSubsolver(); if (needsTimeout) { smte->setTimeLimit(timeout, true); } smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); - Expr equery = query.toExpr().exportTo(&em, varMap); + Expr equery = query.toExpr().exportTo(em, varMap); smte->assertFormula(equery); } catch (const CVC4::ExportUnsupportedException& e) @@ -82,13 +80,13 @@ void initializeSubsolverWithExport(std::unique_ptr& smte, } } -void initializeSubsolver(std::unique_ptr& smte, Node query) +void initializeSubsolver(SmtEngine* smte, Node query) { initializeSubsolver(smte); smte->assertFormula(query.toExpr()); } -Result checkWithSubsolver(std::unique_ptr& smte, Node query) +Result checkWithSubsolver(SmtEngine* smte, Node query) { Assert(query.getType().isBoolean()); Result r = quickCheck(query); @@ -130,19 +128,33 @@ Result checkWithSubsolver(Node query, } return r; } - std::unique_ptr smte; + + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // This is only temporarily until we have separate options for each + // SmtEngine instance. We should reuse the same ExprManager with + // a different SmtEngine (and different options) here, eventually. + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + std::unique_ptr simpleSmte; + std::unique_ptr slv; + ExprManager* em = nullptr; + SmtEngine* smte = nullptr; ExprManagerMapCollection varMap; NodeManager* nm = NodeManager::currentNM(); - ExprManager em(nm->getOptions()); bool needsExport = false; if (needsTimeout) { + slv.reset(new api::Solver(&nm->getOptions())); + em = slv->getExprManager(); + smte = slv->getSmtEngine(); needsExport = true; initializeSubsolverWithExport( smte, em, varMap, query, needsTimeout, timeout); } else { + em = nm->toExprManager(); + simpleSmte.reset(new SmtEngine(em)); + smte = simpleSmte.get(); initializeSubsolver(smte, query); } r = smte->checkSat(); @@ -153,7 +165,7 @@ Result checkWithSubsolver(Node query, Expr val; if (needsExport) { - Expr ev = v.toExpr().exportTo(&em, varMap); + Expr ev = v.toExpr().exportTo(em, varMap); val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap); } else diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 23308e12e..b606657bb 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -34,7 +34,7 @@ namespace theory { * This function initializes the smt engine smte as a subsolver, e.g. it * creates a new SMT engine and sets the options of the current SMT engine. */ -void initializeSubsolver(std::unique_ptr& smte); +void initializeSubsolver(SmtEngine* smte); /** * Initialize Smt subsolver with exporting @@ -52,14 +52,14 @@ void initializeSubsolver(std::unique_ptr& smte); * manager. * * @param smte The smt engine pointer to initialize - * @param em Reference to the expression manager to use + * @param em Reference to the expression manager used by smte * @param varMap Map used for exporting expressions * @param query The query to check * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ -void initializeSubsolverWithExport(std::unique_ptr& smte, - ExprManager& em, +void initializeSubsolverWithExport(SmtEngine* smte, + ExprManager* em, ExprManagerMapCollection& varMap, Node query, bool needsTimeout = false, @@ -73,7 +73,7 @@ void initializeSubsolverWithExport(std::unique_ptr& smte, * exporting since the Options and ExprManager are tied together. * TODO: eliminate this dependency (cvc4-projects #120). */ -void initializeSubsolver(std::unique_ptr& smte, Node query); +void initializeSubsolver(SmtEngine* smte, Node query); /** * This returns the result of checking the satisfiability of formula query. @@ -81,7 +81,7 @@ void initializeSubsolver(std::unique_ptr& smte, Node query); * If necessary, smte is initialized to the SMT engine that checked its * satisfiability. */ -Result checkWithSubsolver(std::unique_ptr& smte, Node query); +Result checkWithSubsolver(SmtEngine* smte, Node query); /** * This returns the result of checking the satisfiability of formula query. diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt index 420ce8e6f..041d14295 100644 --- a/test/system/CMakeLists.txt +++ b/test/system/CMakeLists.txt @@ -32,5 +32,5 @@ cvc4_add_system_test(reset_assertions) cvc4_add_system_test(sep_log_api) cvc4_add_system_test(smt2_compliance) cvc4_add_system_test(statistics) -cvc4_add_system_test(two_smt_engines) +cvc4_add_system_test(two_solvers) # TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration) diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index 93f5dceb8..315cec7bf 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -19,18 +19,14 @@ #include #include -#include "expr/expr.h" -#include "smt/smt_engine.h" +#include "api/cvc4cpp.h" -using namespace CVC4; +using namespace CVC4::api; using namespace std; int main() { - ExprManager em; - Options opts; - SmtEngine smt(&em); - Result r = smt.checkEntailed(em.mkConst(true)); - - return (Result::ENTAILED == r) ? 0 : 1; + Solver slv; + Result r = slv.checkEntailed(slv.mkBoolean(true)); + return r.isEntailed() ? 0 : 1; } diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp index 2a94dbd98..dc9bd24f6 100644 --- a/test/system/reset_assertions.cpp +++ b/test/system/reset_assertions.cpp @@ -20,34 +20,31 @@ #include #include -#include "expr/expr.h" -#include "smt/smt_engine.h" +#include "api/cvc4cpp.h" -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); - - smt.setOption("incremental", SExpr(true)); - - Type real = em.realType(); - Expr x = em.mkVar("x", real); - Expr four = em.mkConst(Rational(4)); - Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four); - smt.assertFormula(xEqFour); - std::cout << smt.checkSat() << std::endl; - - smt.resetAssertions(); - - Type elementType = em.integerType(); - Type indexType = em.integerType(); - Type arrayType = em.mkArrayType(indexType, elementType); - Expr array = em.mkVar("array", arrayType); - Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four); - Expr ten = em.mkConst(Rational(10)); - Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten); - smt.assertFormula(arrayAtFour_eq_ten); - std::cout << smt.checkSat() << std::endl; + Solver slv; + slv.setOption("incremental", "true"); + + Sort real = slv.getRealSort(); + Term x = slv.mkConst(real, "x"); + Term four = slv.mkReal(4); + Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four); + slv.assertFormula(xEqFour); + std::cout << slv.checkSat() << std::endl; + + slv.resetAssertions(); + + Sort elementType = slv.getIntegerSort(); + Sort indexType = slv.getIntegerSort(); + Sort arrayType = slv.mkArraySort(indexType, elementType); + Term array = slv.mkConst(arrayType, "array"); + Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four); + Term ten = slv.mkReal(10); + Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten); + slv.assertFormula(arrayAtFour_eq_ten); + std::cout << slv.checkSat() << std::endl; } diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index 025aaed11..234246112 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -15,48 +15,52 @@ ** minimally functional. **/ +#include "util/statistics.h" + #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "smt/smt_engine.h" #include "util/sexpr.h" -#include "util/statistics.h" using namespace CVC4; using namespace std; int main() { - ExprManager em; - Options opts; - SmtEngine smt(&em); - smt.setOption("incremental", SExpr("true")); - Expr x = em.mkVar("x", em.integerType()); - Expr y = em.mkVar("y", em.integerType()); - smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5)))); - Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0))); - Result r = smt.checkEntailed(q); + api::Solver slv; + ExprManager* em = slv.getExprManager(); + SmtEngine* smt = slv.getSmtEngine(); + smt->setOption("incremental", SExpr("true")); + Expr x = em->mkVar("x", em->integerType()); + Expr y = em->mkVar("y", em->integerType()); + smt->assertFormula(em->mkExpr( + kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5)))); + Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0))); + Result r = smt->checkEntailed(q); if (r != Result::NOT_ENTAILED) { exit(1); } - Statistics stats = smt.getStatistics(); + Statistics stats = smt->getStatistics(); for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) { cout << "stat " << (*i).first << " is " << (*i).second << endl; } - smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5)))); - r = smt.checkEntailed(q); - Statistics stats2 = smt.getStatistics(); + smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5)))); + r = smt->checkEntailed(q); + Statistics stats2 = smt->getStatistics(); bool different = false; for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) { cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl; cout << "stat2 " << (*i).first << " is " << (*i).second << endl; - if(smt.getStatistic((*i).first) != (*i).second) { - cout << "SMT engine reports different value for statistic " - << (*i).first << ": " << smt.getStatistic((*i).first) << endl; + if (smt->getStatistic((*i).first) != (*i).second) + { + cout << "SMT engine reports different value for statistic " << (*i).first + << ": " << smt->getStatistic((*i).first) << endl; exit(1); } different = different || stats.getStatistic((*i).first) != (*i).second; diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp deleted file mode 100644 index 71676482e..000000000 --- a/test/system/two_smt_engines.cpp +++ /dev/null @@ -1,36 +0,0 @@ -/********************* */ -/*! \file two_smt_engines.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz - ** 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. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple test of multiple SmtEngines - ** - ** A simple test of multiple SmtEngines. - **/ - -#include -#include - -#include "expr/expr.h" -#include "smt/smt_engine.h" - -using namespace CVC4; -using namespace std; - -int main() { - ExprManager em; - Options opts; - SmtEngine smt(&em); - SmtEngine smt2(&em); - Result r = smt.checkEntailed(em.mkConst(true)); - Result r2 = smt2.checkEntailed(em.mkConst(true)); - - return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1; -} - diff --git a/test/system/two_solvers.cpp b/test/system/two_solvers.cpp new file mode 100644 index 000000000..c5bea4860 --- /dev/null +++ b/test/system/two_solvers.cpp @@ -0,0 +1,32 @@ +/********************* */ +/*! \file two_smt_engines.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Aina Niemetz + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple test of multiple SmtEngines + ** + ** A simple test of multiple SmtEngines. + **/ + +#include +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; +using namespace std; + +int main() { + Solver s1; + Solver s2; + Result r = s1.checkEntailed(s1.mkBoolean(true)); + Result r2 = s2.checkEntailed(s2.mkBoolean(true)); + return r.isEntailed() && r2.isEntailed() ? 0 : 1; +} + 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 //Used in some of the tests -#include #include +#include +#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 #include -#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 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 mkVars(Type type, unsigned int n) { - std::vector 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 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 mkVars(Type type, unsigned int n) + { + std::vector 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 #include +#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 #include +#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 #include -#include #include +#include +#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 + +#include +#include +#include + +#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 -#include -#include -#include - 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 //Used in some of the tests -#include #include +#include +#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 +#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 + #include +#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 */ -- cgit v1.2.3