From 19f223e580b527bc17add2ea4e61e85df2977c87 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 30 Sep 2021 18:57:24 -0700 Subject: [PATCH] Rename SmtEngine to SolverEngine. (#7282) --- src/api/cpp/cvc5.cpp | 244 ++++++------ src/api/cpp/cvc5.h | 4 +- src/decision/decision_engine.h | 2 +- src/decision/decision_engine_old.h | 2 +- src/main/command_executor.cpp | 2 +- src/main/interactive_shell.cpp | 2 +- src/omt/bitvector_optimizer.cpp | 4 +- src/omt/bitvector_optimizer.h | 4 +- src/omt/integer_optimizer.cpp | 6 +- src/omt/integer_optimizer.h | 6 +- src/omt/omt_optimizer.h | 4 +- src/parser/smt2/Smt2.g | 6 +- src/parser/smt2/smt2.cpp | 2 +- src/preprocessing/passes/apply_substs.cpp | 2 +- src/preprocessing/passes/sygus_inference.cpp | 2 +- .../preprocessing_pass_context.cpp | 8 +- .../preprocessing_pass_context.h | 8 +- src/printer/smt2/smt2_printer.h | 4 +- src/printer/tptp/tptp_printer.h | 7 +- src/prop/cnf_stream.h | 2 +- src/prop/minisat/CVC4-README | 2 +- src/prop/prop_engine.h | 2 +- src/smt/abduction_solver.cpp | 42 +- src/smt/abduction_solver.h | 8 +- src/smt/assertions.cpp | 3 +- src/smt/check_models.cpp | 22 +- src/smt/dump_manager.h | 8 +- src/smt/env.h | 16 +- src/smt/interpolation_solver.cpp | 29 +- src/smt/interpolation_solver.h | 5 +- src/smt/listeners.cpp | 6 +- src/smt/listeners.h | 10 +- src/smt/optimization_solver.cpp | 8 +- src/smt/optimization_solver.h | 14 +- src/smt/output_manager.cpp | 6 +- src/smt/output_manager.h | 8 +- src/smt/preprocessor.cpp | 12 +- src/smt/preprocessor.h | 10 +- src/smt/process_assertions.cpp | 20 +- src/smt/process_assertions.h | 6 +- src/smt/proof_manager.cpp | 19 +- src/smt/proof_manager.h | 24 +- src/smt/proof_post_processor.h | 4 +- src/smt/quant_elim_solver.cpp | 2 +- src/smt/quant_elim_solver.h | 6 +- src/smt/set_defaults.cpp | 62 +-- src/smt/set_defaults.h | 6 +- src/smt/smt_engine_scope.cpp | 32 +- src/smt/smt_engine_scope.h | 12 +- src/smt/smt_engine_state.cpp | 16 +- src/smt/smt_engine_state.h | 60 +-- src/smt/smt_engine_stats.h | 2 +- src/smt/smt_mode.cpp | 2 +- src/smt/smt_mode.h | 2 +- src/smt/smt_solver.cpp | 2 +- src/smt/smt_solver.h | 22 +- src/smt/smt_statistics_registry.cpp | 2 +- src/smt/smt_statistics_registry.h | 5 +- src/smt/solver_engine.cpp | 359 +++++++++--------- src/smt/solver_engine.h | 101 ++--- src/smt/sygus_solver.cpp | 2 +- src/smt/unsat_core_manager.cpp | 2 +- src/smt/unsat_core_manager.h | 4 +- .../builtin/theory_builtin_type_rules.h | 4 +- src/theory/bv/int_blaster.h | 2 +- src/theory/bv/theory_bv_rewrite_rules.h | 2 +- src/theory/datatypes/datatypes_rewriter.h | 2 +- src/theory/logic_info.h | 12 +- .../candidate_rewrite_database.cpp | 4 +- .../quantifiers/candidate_rewrite_database.h | 2 +- src/theory/quantifiers/cegqi/nested_qe.cpp | 2 +- src/theory/quantifiers/expr_miner.cpp | 4 +- src/theory/quantifiers/expr_miner.h | 4 +- src/theory/quantifiers/query_generator.cpp | 2 +- .../sygus/ce_guided_single_inv.cpp | 2 +- .../sygus/cegis_core_connective.cpp | 8 +- .../quantifiers/sygus/cegis_core_connective.h | 6 +- .../quantifiers/sygus/sygus_interpol.cpp | 16 +- src/theory/quantifiers/sygus/sygus_interpol.h | 4 +- .../quantifiers/sygus/sygus_qe_preproc.cpp | 2 +- .../quantifiers/sygus/sygus_repair_const.cpp | 2 +- .../quantifiers/sygus/sygus_repair_const.h | 2 +- src/theory/rewriter.cpp | 2 +- src/theory/rewriter.h | 4 +- src/theory/smt_engine_subsolver.cpp | 12 +- src/theory/smt_engine_subsolver.h | 9 +- src/theory/theory.h | 2 +- src/theory/theory_engine.h | 2 +- src/util/resource_manager.h | 2 +- test/api/reset_assertions.cpp | 2 +- test/unit/node/node_black.cpp | 4 +- test/unit/node/type_node_white.cpp | 6 +- .../preprocessing/pass_bv_gauss_white.cpp | 2 +- .../pass_foreign_theory_rewrite_white.cpp | 2 +- test/unit/prop/cnf_stream_white.cpp | 6 +- test/unit/test_smt.h | 12 +- test/unit/theory/evaluator_white.cpp | 8 +- test/unit/theory/sequences_rewriter_white.cpp | 2 +- test/unit/theory/theory_arith_pow2_white.cpp | 4 +- test/unit/theory/theory_arith_white.cpp | 8 +- .../theory/theory_bv_int_blaster_white.cpp | 12 +- test/unit/theory/theory_bv_opt_white.cpp | 36 +- test/unit/theory/theory_bv_white.cpp | 26 +- test/unit/theory/theory_engine_white.cpp | 6 +- test/unit/theory/theory_int_opt_white.cpp | 32 +- .../theory/theory_opt_multigoal_white.cpp | 40 +- .../theory_quantifiers_bv_inverter_white.cpp | 32 +- test/unit/theory/theory_white.cpp | 12 +- 108 files changed, 845 insertions(+), 828 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a8b60a94d..7ee33f143 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4728,15 +4728,15 @@ DriverOptions::DriverOptions(const Solver& solver) : d_solver(solver) {} std::istream& DriverOptions::in() const { - return *d_solver.d_smtEngine->getOptions().base.in; + return *d_solver.d_slv->getOptions().base.in; } std::ostream& DriverOptions::err() const { - return *d_solver.d_smtEngine->getOptions().base.err; + return *d_solver.d_slv->getOptions().base.err; } std::ostream& DriverOptions::out() const { - return *d_solver.d_smtEngine->getOptions().base.out; + return *d_solver.d_slv->getOptions().base.out; } /* -------------------------------------------------------------------------- */ @@ -4946,9 +4946,9 @@ Solver::Solver(std::unique_ptr&& original) d_nodeMgr = NodeManager::currentNM(); d_nodeMgr->init(); d_originalOptions = std::move(original); - d_smtEngine.reset(new SmtEngine(d_nodeMgr, d_originalOptions.get())); - d_smtEngine->setSolver(this); - d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); + d_slv.reset(new SolverEngine(d_nodeMgr, d_originalOptions.get())); + d_slv->setSolver(this); + d_rng.reset(new Random(d_slv->getOptions().driver.seed)); resetStatistics(); } @@ -5058,7 +5058,7 @@ Term Solver::getValueHelper(const Term& term) const { // Note: Term is checked in the caller to avoid double checks //////// all checks before this line - Node value = d_smtEngine->getValue(*term.d_node); + Node value = d_slv->getValue(*term.d_node); Term res = Term(this, value); // May need to wrap in real cast so that user know this is a real. TypeNode tn = (*term.d_node).getType(); @@ -5265,7 +5265,7 @@ Term Solver::synthFunHelper(const std::string& symbol, std::vector bvns = Term::termVectorToNodes(boundVars); - d_smtEngine->declareSynthFun( + d_slv->declareSynthFun( fun, grammar == nullptr ? funType : *grammar->resolve().d_type, isInv, @@ -5366,19 +5366,18 @@ void Solver::resetStatistics() if constexpr (Configuration::isStatisticsBuild()) { d_stats.reset(new APIStatistics{ - d_smtEngine->getStatisticsRegistry().registerHistogram( + d_slv->getStatisticsRegistry().registerHistogram( "api::CONSTANT"), - d_smtEngine->getStatisticsRegistry().registerHistogram( + d_slv->getStatisticsRegistry().registerHistogram( "api::VARIABLE"), - d_smtEngine->getStatisticsRegistry().registerHistogram( - "api::TERM"), + d_slv->getStatisticsRegistry().registerHistogram("api::TERM"), }); } } void Solver::printStatisticsSafe(int fd) const { - d_smtEngine->printStatisticsSafe(fd); + d_slv->printStatisticsSafe(fd); } /* Helpers for mkTerm checks. */ @@ -6535,7 +6534,7 @@ Term Solver::simplify(const Term& term) CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(term); //////// all checks before this line - return Term(this, d_smtEngine->simplify(*term.d_node)); + return Term(this, d_slv->simplify(*term.d_node)); //////// CVC5_API_TRY_CATCH_END; } @@ -6543,13 +6542,13 @@ Term Solver::simplify(const Term& term) Result Solver::checkEntailed(const Term& term) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(!d_slv->isQueryMade() + || d_slv->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); //////// all checks before this line - return d_smtEngine->checkEntailed(*term.d_node); + return d_slv->checkEntailed(*term.d_node); //////// CVC5_API_TRY_CATCH_END; } @@ -6557,13 +6556,13 @@ Result Solver::checkEntailed(const Term& term) const Result Solver::checkEntailed(const std::vector& terms) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(!d_slv->isQueryMade() + || d_slv->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); //////// all checks before this line - return d_smtEngine->checkEntailed(Term::termVectorToNodes(terms)); + return d_slv->checkEntailed(Term::termVectorToNodes(terms)); //////// CVC5_API_TRY_CATCH_END; } @@ -6577,7 +6576,7 @@ void Solver::assertFormula(const Term& term) const CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, getBooleanSort()); //////// all checks before this line - d_smtEngine->assertFormula(*term.d_node); + d_slv->assertFormula(*term.d_node); //////// CVC5_API_TRY_CATCH_END; } @@ -6585,12 +6584,12 @@ void Solver::assertFormula(const Term& term) const Result Solver::checkSat(void) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(!d_slv->isQueryMade() + || d_slv->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line - return d_smtEngine->checkSat(); + return d_slv->checkSat(); //////// CVC5_API_TRY_CATCH_END; } @@ -6598,13 +6597,13 @@ Result Solver::checkSat(void) const Result Solver::checkSatAssuming(const Term& assumption) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(!d_slv->isQueryMade() + || d_slv->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); //////// all checks before this line - return d_smtEngine->checkSat(*assumption.d_node); + return d_slv->checkSat(*assumption.d_node); //////// CVC5_API_TRY_CATCH_END; } @@ -6612,8 +6611,8 @@ Result Solver::checkSatAssuming(const Term& assumption) const Result Solver::checkSatAssuming(const std::vector& assumptions) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(!d_slv->isQueryMade() || assumptions.size() == 0 + || d_slv->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6623,7 +6622,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const CVC5_API_SOLVER_CHECK_TERM(term); } std::vector eassumptions = Term::termVectorToNodes(assumptions); - return d_smtEngine->checkSat(eassumptions); + return d_slv->checkSat(eassumptions); //////// CVC5_API_TRY_CATCH_END; } @@ -6709,7 +6708,7 @@ Term Solver::defineFun(const std::string& symbol, CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); //////// all checks before this line - d_smtEngine->defineFunction( + d_slv->defineFunction( *fun.d_node, Term::termVectorToNodes(bound_vars), *term.d_node, global); return fun; //////// @@ -6741,7 +6740,7 @@ Term Solver::defineFun(const Term& fun, } //////// all checks before this line std::vector ebound_vars = Term::termVectorToNodes(bound_vars); - d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); + d_slv->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); return fun; //////// CVC5_API_TRY_CATCH_END; @@ -6755,10 +6754,9 @@ Term Solver::defineFunRec(const std::string& symbol, { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) + CVC5_API_CHECK(d_slv->getUserLogicInfo().isQuantified()) << "recursive function definitions require a logic with quantifiers"; - CVC5_API_CHECK( - d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) + CVC5_API_CHECK(d_slv->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) << "recursive function definitions require a logic with uninterpreted " "functions"; @@ -6784,7 +6782,7 @@ Term Solver::defineFunRec(const std::string& symbol, CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); //////// all checks before this line - d_smtEngine->defineFunctionRec( + d_slv->defineFunctionRec( *fun.d_node, Term::termVectorToNodes(bound_vars), *term.d_node, global); return fun; @@ -6799,10 +6797,9 @@ Term Solver::defineFunRec(const Term& fun, { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) + CVC5_API_CHECK(d_slv->getUserLogicInfo().isQuantified()) << "recursive function definitions require a logic with quantifiers"; - CVC5_API_CHECK( - d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) + CVC5_API_CHECK(d_slv->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) << "recursive function definitions require a logic with uninterpreted " "functions"; @@ -6826,8 +6823,7 @@ Term Solver::defineFunRec(const Term& fun, //////// all checks before this line std::vector ebound_vars = Term::termVectorToNodes(bound_vars); - d_smtEngine->defineFunctionRec( - *fun.d_node, ebound_vars, *term.d_node, global); + d_slv->defineFunctionRec(*fun.d_node, ebound_vars, *term.d_node, global); return fun; //////// CVC5_API_TRY_CATCH_END; @@ -6840,10 +6836,9 @@ void Solver::defineFunsRec(const std::vector& funs, { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) + CVC5_API_CHECK(d_slv->getUserLogicInfo().isQuantified()) << "recursive function definitions require a logic with quantifiers"; - CVC5_API_CHECK( - d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) + CVC5_API_CHECK(d_slv->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) << "recursive function definitions require a logic with uninterpreted " "functions"; CVC5_API_SOLVER_CHECK_TERMS(funs); @@ -6892,7 +6887,7 @@ void Solver::defineFunsRec(const std::vector& funs, ebound_vars.push_back(Term::termVectorToNodes(v)); } std::vector nodes = Term::termVectorToNodes(terms); - d_smtEngine->defineFunctionsRec(efuns, ebound_vars, nodes, global); + d_slv->defineFunctionsRec(efuns, ebound_vars, nodes, global); //////// CVC5_API_TRY_CATCH_END; } @@ -6906,7 +6901,7 @@ std::vector Solver::getAssertions(void) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - std::vector assertions = d_smtEngine->getAssertions(); + std::vector assertions = d_slv->getAssertions(); /* Can not use * return std::vector(assertions.begin(), assertions.end()); * here since constructor is private */ @@ -6923,10 +6918,10 @@ std::vector Solver::getAssertions(void) const std::string Solver::getInfo(const std::string& flag) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) + CVC5_API_RECOVERABLE_CHECK(d_slv->isValidGetInfoFlag(flag)) << "Unrecognized flag for getInfo."; //////// all checks before this line - return d_smtEngine->getInfo(flag); + return d_slv->getInfo(flag); //////// CVC5_API_TRY_CATCH_END; } @@ -6935,7 +6930,7 @@ std::string Solver::getOption(const std::string& option) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_smtEngine->getOption(option); + return d_slv->getOption(option); //////// CVC5_API_TRY_CATCH_END; } @@ -7071,7 +7066,7 @@ OptionInfo Solver::getOptionInfo(const std::string& option) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - auto info = options::getInfo(d_smtEngine->getOptions(), option); + auto info = options::getInfo(d_slv->getOptions(), option); CVC5_API_CHECK(info.name != "") << "Querying invalid or unknown option " << option; return std::visit( @@ -7138,17 +7133,17 @@ DriverOptions Solver::getDriverOptions() const { return DriverOptions(*this); } std::vector Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) + CVC5_API_CHECK(d_slv->getOptions().smt.unsatAssumptions) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; - CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) + CVC5_API_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat assumptions unless in unsat mode."; //////// all checks before this line - std::vector uassumptions = d_smtEngine->getUnsatAssumptions(); + std::vector uassumptions = d_slv->getUnsatAssumptions(); /* Can not use * return std::vector(uassumptions.begin(), uassumptions.end()); * here since constructor is private */ @@ -7165,13 +7160,13 @@ std::vector Solver::getUnsatAssumptions(void) const std::vector Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores) + CVC5_API_CHECK(d_slv->getOptions().smt.unsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) + CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat core unless in unsat mode."; //////// all checks before this line - UnsatCore core = d_smtEngine->getUnsatCore(); + UnsatCore core = d_slv->getUnsatCore(); /* Can not use * return std::vector(core.begin(), core.end()); * here since constructor is private */ @@ -7188,15 +7183,14 @@ std::vector Solver::getUnsatCore(void) const std::map Solver::getDifficulty() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT - || d_smtEngine->getSmtMode() == SmtMode::SAT - || d_smtEngine->getSmtMode() - == SmtMode::SAT_UNKNOWN) + CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT + || d_slv->getSmtMode() == SmtMode::SAT + || d_slv->getSmtMode() == SmtMode::SAT_UNKNOWN) << "Cannot get difficulty unless after a UNSAT, SAT or unknown response."; //////// all checks before this line std::map res; std::map dmap; - d_smtEngine->getDifficultyMap(dmap); + d_slv->getDifficultyMap(dmap); for (const std::pair& d : dmap) { res[Term(this, d.first)] = Term(this, d.second); @@ -7209,11 +7203,11 @@ std::map Solver::getDifficulty() const std::string Solver::getProof(void) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceProofs) + CVC5_API_CHECK(d_slv->getOptions().smt.produceProofs) << "Cannot get proof explicitly enabled (try --produce-proofs)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) + CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT) << "Cannot get proof unless in unsat mode."; - return d_smtEngine->getProof(); + return d_slv->getProof(); CVC5_API_TRY_CATCH_END; } @@ -7230,10 +7224,10 @@ Term Solver::getValue(const Term& term) const std::vector Solver::getValue(const std::vector& terms) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Cannot get value unless after a SAT or unknown response."; CVC5_API_SOLVER_CHECK_TERMS(terms); //////// all checks before this line @@ -7252,10 +7246,10 @@ std::vector Solver::getValue(const std::vector& terms) const std::vector Solver::getModelDomainElements(const Sort& s) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get domain elements unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Cannot get domain elements unless after a SAT or unknown response."; CVC5_API_SOLVER_CHECK_SORT(s); CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort()) @@ -7263,8 +7257,7 @@ std::vector Solver::getModelDomainElements(const Sort& s) const "getModelDomainElements."; //////// all checks before this line std::vector res; - std::vector elements = - d_smtEngine->getModelDomainElements(s.getTypeNode()); + std::vector elements = d_slv->getModelDomainElements(s.getTypeNode()); for (const Node& n : elements) { res.push_back(Term(this, n)); @@ -7277,17 +7270,17 @@ std::vector Solver::getModelDomainElements(const Sort& s) const bool Solver::isModelCoreSymbol(const Term& v) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot check if model core symbol unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Cannot check if model core symbol unless after a SAT or unknown " "response."; CVC5_API_SOLVER_CHECK_TERM(v); CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT) << "Expecting a free constant as argument to isModelCoreSymbol."; //////// all checks before this line - return d_smtEngine->isModelCoreSymbol(v.getNode()); + return d_slv->isModelCoreSymbol(v.getNode()); //////// CVC5_API_TRY_CATCH_END; } @@ -7296,10 +7289,10 @@ std::string Solver::getModel(const std::vector& sorts, const std::vector& vars) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get model unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Cannot get model unless after a SAT or unknown response."; CVC5_API_SOLVER_CHECK_SORTS(sorts); for (const Sort& s : sorts) @@ -7315,8 +7308,8 @@ std::string Solver::getModel(const std::vector& sorts, << "Expecting a free constant as argument to getModel."; } //////// all checks before this line - return d_smtEngine->getModel(Sort::sortVectorToTypeNodes(sorts), - Term::termVectorToNodes(vars)); + return d_slv->getModel(Sort::sortVectorToTypeNodes(sorts), + Term::termVectorToNodes(vars)); //////// CVC5_API_TRY_CATCH_END; } @@ -7326,8 +7319,7 @@ Term Solver::getQuantifierElimination(const Term& q) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term(this, - d_smtEngine->getQuantifierElimination(q.getNode(), true, true)); + return Term(this, d_slv->getQuantifierElimination(q.getNode(), true, true)); //////// CVC5_API_TRY_CATCH_END; } @@ -7337,8 +7329,7 @@ Term Solver::getQuantifierEliminationDisjunct(const Term& q) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term(this, - d_smtEngine->getQuantifierElimination(q.getNode(), false, true)); + return Term(this, d_slv->getQuantifierElimination(q.getNode(), false, true)); //////// CVC5_API_TRY_CATCH_END; } @@ -7349,12 +7340,11 @@ void Solver::declareSeparationHeap(const Sort& locSort, CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(locSort); CVC5_API_SOLVER_CHECK_SORT(dataSort); - CVC5_API_CHECK( - d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; //////// all checks before this line - d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode()); + d_slv->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode()); //////// CVC5_API_TRY_CATCH_END; } @@ -7362,17 +7352,16 @@ void Solver::declareSeparationHeap(const Sort& locSort, Term Solver::getSeparationHeap() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK( - d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only get separtion heap term after sat or unknown response."; //////// all checks before this line - return Term(this, d_smtEngine->getSepHeapExpr()); + return Term(this, d_slv->getSepHeapExpr()); //////// CVC5_API_TRY_CATCH_END; } @@ -7380,17 +7369,16 @@ Term Solver::getSeparationHeap() const Term Solver::getSeparationNilTerm() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK( - d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only get separtion nil term after sat or unknown response."; //////// all checks before this line - return Term(this, d_smtEngine->getSepNilExpr()); + return Term(this, d_slv->getSepNilExpr()); //////// CVC5_API_TRY_CATCH_END; } @@ -7406,7 +7394,7 @@ Term Solver::declarePool(const std::string& symbol, TypeNode setType = getNodeManager()->mkSetType(*sort.d_type); Node pool = getNodeManager()->mkBoundVar(symbol, setType); std::vector initv = Term::termVectorToNodes(initValue); - d_smtEngine->declarePool(pool, initv); + d_slv->declarePool(pool, initv); return Term(this, pool); //////// CVC5_API_TRY_CATCH_END; @@ -7415,14 +7403,14 @@ Term Solver::declarePool(const std::string& symbol, void Solver::pop(uint32_t nscopes) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; - CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) + CVC5_API_CHECK(nscopes <= d_slv->getNumUserLevels()) << "Cannot pop beyond first pushed context"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) { - d_smtEngine->pop(); + d_slv->pop(); } //////// CVC5_API_TRY_CATCH_END; @@ -7434,7 +7422,7 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const CVC5_API_SOLVER_CHECK_TERM(conj); //////// all checks before this line Node result; - bool success = d_smtEngine->getInterpol(*conj.d_node, result); + bool success = d_slv->getInterpol(*conj.d_node, result); if (success) { output = Term(this, result); @@ -7453,7 +7441,7 @@ bool Solver::getInterpolant(const Term& conj, //////// all checks before this line Node result; bool success = - d_smtEngine->getInterpol(*conj.d_node, *grammar.resolve().d_type, result); + d_slv->getInterpol(*conj.d_node, *grammar.resolve().d_type, result); if (success) { output = Term(this, result); @@ -7469,7 +7457,7 @@ bool Solver::getAbduct(const Term& conj, Term& output) const CVC5_API_SOLVER_CHECK_TERM(conj); //////// all checks before this line Node result; - bool success = d_smtEngine->getAbduct(*conj.d_node, result); + bool success = d_slv->getAbduct(*conj.d_node, result); if (success) { output = Term(this, result); @@ -7486,7 +7474,7 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const //////// all checks before this line Node result; bool success = - d_smtEngine->getAbduct(*conj.d_node, *grammar.resolve().d_type, result); + d_slv->getAbduct(*conj.d_node, *grammar.resolve().d_type, result); if (success) { output = Term(this, result); @@ -7499,13 +7487,13 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const void Solver::blockModel() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only block model after sat or unknown response."; //////// all checks before this line - d_smtEngine->blockModel(); + d_slv->blockModel(); //////// CVC5_API_TRY_CATCH_END; } @@ -7513,16 +7501,16 @@ void Solver::blockModel() const void Solver::blockModelValues(const std::vector& terms) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) + CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only block model values after sat or unknown response."; CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "a non-empty set of terms"; CVC5_API_SOLVER_CHECK_TERMS(terms); //////// all checks before this line - d_smtEngine->blockModelValues(Term::termVectorToNodes(terms)); + d_slv->blockModelValues(Term::termVectorToNodes(terms)); //////// CVC5_API_TRY_CATCH_END; } @@ -7531,7 +7519,7 @@ void Solver::printInstantiations(std::ostream& out) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - d_smtEngine->printInstantiations(out); + d_slv->printInstantiations(out); //////// CVC5_API_TRY_CATCH_END; } @@ -7539,12 +7527,12 @@ void Solver::printInstantiations(std::ostream& out) const void Solver::push(uint32_t nscopes) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) { - d_smtEngine->push(); + d_slv->push(); } //////// CVC5_API_TRY_CATCH_END; @@ -7554,7 +7542,7 @@ void Solver::resetAssertions(void) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - d_smtEngine->resetAssertions(); + d_slv->resetAssertions(); //////// CVC5_API_TRY_CATCH_END; } @@ -7580,7 +7568,7 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const value) << "'sat', 'unsat' or 'unknown'"; //////// all checks before this line - d_smtEngine->setInfo(keyword, value); + d_slv->setInfo(keyword, value); //////// CVC5_API_TRY_CATCH_END; } @@ -7588,11 +7576,11 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const void Solver::setLogic(const std::string& logic) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_smtEngine->isFullyInited()) + CVC5_API_CHECK(!d_slv->isFullyInited()) << "Invalid call to 'setLogic', solver is already fully initialized"; cvc5::LogicInfo logic_info(logic); //////// all checks before this line - d_smtEngine->setLogic(logic_info); + d_slv->setLogic(logic_info); //////// CVC5_API_TRY_CATCH_END; } @@ -7609,12 +7597,12 @@ void Solver::setOption(const std::string& option, if (std::find(mutableOpts.begin(), mutableOpts.end(), option) == mutableOpts.end()) { - CVC5_API_CHECK(!d_smtEngine->isFullyInited()) + CVC5_API_CHECK(!d_slv->isFullyInited()) << "Invalid call to 'setOption' for option '" << option << "', solver is already fully initialized"; } //////// all checks before this line - d_smtEngine->setOption(option, value); + d_slv->setOption(option, value); //////// CVC5_API_TRY_CATCH_END; } @@ -7627,7 +7615,7 @@ Term Solver::mkSygusVar(const Sort& sort, const std::string& symbol) const Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ - d_smtEngine->declareSygusVar(res); + d_slv->declareSygusVar(res); return Term(this, res); //////// @@ -7711,7 +7699,7 @@ void Solver::addSygusConstraint(const Term& term) const term.d_node->getType() == getNodeManager()->booleanType(), term) << "boolean term"; //////// all checks before this line - d_smtEngine->assertSygusConstraint(*term.d_node, false); + d_slv->assertSygusConstraint(*term.d_node, false); //////// CVC5_API_TRY_CATCH_END; } @@ -7724,7 +7712,7 @@ void Solver::addSygusAssume(const Term& term) const term.d_node->getType() == getNodeManager()->booleanType(), term) << "boolean term"; //////// all checks before this line - d_smtEngine->assertSygusConstraint(*term.d_node, true); + d_slv->assertSygusConstraint(*term.d_node, true); //////// CVC5_API_TRY_CATCH_END; } @@ -7772,7 +7760,7 @@ void Solver::addSygusInvConstraint(Term inv, CVC5_API_CHECK(trans.d_node->getType() == expectedTransType) << "Expected trans's sort to be " << invType; - d_smtEngine->assertSygusInvConstraint( + d_slv->assertSygusInvConstraint( *inv.d_node, *pre.d_node, *trans.d_node, *post.d_node); //////// CVC5_API_TRY_CATCH_END; @@ -7782,7 +7770,7 @@ Result Solver::checkSynth() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_smtEngine->checkSynth(); + return d_slv->checkSynth(); //////// CVC5_API_TRY_CATCH_END; } @@ -7793,7 +7781,7 @@ Term Solver::getSynthSolution(Term term) const CVC5_API_SOLVER_CHECK_TERM(term); std::map map; - CVC5_API_CHECK(d_smtEngine->getSynthSolutions(map)) + CVC5_API_CHECK(d_slv->getSynthSolutions(map)) << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; @@ -7814,7 +7802,7 @@ std::vector Solver::getSynthSolutions( CVC5_API_SOLVER_CHECK_TERMS(terms); std::map map; - CVC5_API_CHECK(d_smtEngine->getSynthSolutions(map)) + CVC5_API_CHECK(d_slv->getSynthSolutions(map)) << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; //////// all checks before this line @@ -7840,7 +7828,7 @@ std::vector Solver::getSynthSolutions( Statistics Solver::getStatistics() const { - return Statistics(d_smtEngine->getStatisticsRegistry()); + return Statistics(d_slv->getStatisticsRegistry()); } bool Solver::isOutputOn(const std::string& tag) const @@ -7850,7 +7838,7 @@ bool Solver::isOutputOn(const std::string& tag) const // here but roll our own. try { - return d_smtEngine->getEnv().isOutputOn(tag); + return d_slv->getEnv().isOutputOn(tag); } catch (const cvc5::Exception& e) { @@ -7865,7 +7853,7 @@ std::ostream& Solver::getOutput(const std::string& tag) const // here but roll our own. try { - return d_smtEngine->getEnv().getOutput(tag); + return d_slv->getEnv().getOutput(tag); } catch (const cvc5::Exception& e) { diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index bfc266f56..8302ce750 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -44,7 +44,7 @@ class DType; class DTypeConstructor; class DTypeSelector; class NodeManager; -class SmtEngine; +class SolverEngine; class TypeNode; class Options; class Random; @@ -4489,7 +4489,7 @@ class CVC5_EXPORT Solver /** The statistics collected on the Api level. */ std::unique_ptr d_stats; /** The SMT engine of this solver. */ - std::unique_ptr d_smtEngine; + std::unique_ptr d_slv; /** The random number generator of this solver. */ std::unique_ptr d_rng; }; diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 4cf057840..aa4c43e89 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -71,7 +71,7 @@ class DecisionEngine virtual prop::SatLiteral getNextInternal(bool& stopSearch) = 0; /** Pointer to the SAT context */ context::Context* d_context; - /** Pointer to resource manager for associated SmtEngine */ + /** Pointer to resource manager for associated SolverEngine */ ResourceManager* d_resourceManager; /** Pointer to the CNF stream */ prop::CnfStream* d_cnfStream; diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h index 3e9a563b7..93f581143 100644 --- a/src/decision/decision_engine_old.h +++ b/src/decision/decision_engine_old.h @@ -50,7 +50,7 @@ class DecisionEngineOld : public decision::DecisionEngine } /** - * This is called by SmtEngine, at shutdown time, just before + * This is called by SolverEngine, at shutdown time, just before * destruction. It is important because there are destruction * ordering issues between some parts of the system. */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 6a6ae4658..4f5fd5c24 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -60,7 +60,7 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::storeOptionsAsOriginal() { - d_solver->d_originalOptions->copyValues(d_solver->d_smtEngine->getOptions()); + d_solver->d_originalOptions->copyValues(d_solver->d_slv->getOptions()); } void CommandExecutor::printStatistics(std::ostream& out) const diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index d5759db1b..c178a637c 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -355,7 +355,7 @@ restart: } // We can't really clear out the sequence and abort the current line, // because the parse error might be for the second command on the - // line. The first ones haven't yet been executed by the SmtEngine, + // line. The first ones haven't yet been executed by the SolverEngine, // but the parser state has already made the variables and the mappings // in the symbol table. So unfortunately, either we exit cvc5 entirely, // or we commit to the current line up to the command with the parse diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index 72219d995..6e202cb70 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -44,7 +44,7 @@ BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a, + aMod2PlusbMod2Div2)); } -OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, +OptimizationResult OMTOptimizerBitVector::minimize(SolverEngine* optChecker, TNode target) { // the smt engine to which we send intermediate queries @@ -133,7 +133,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, return OptimizationResult(lastSatResult, value); } -OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, +OptimizationResult OMTOptimizerBitVector::maximize(SolverEngine* optChecker, TNode target) { // the smt engine to which we send intermediate queries diff --git a/src/omt/bitvector_optimizer.h b/src/omt/bitvector_optimizer.h index 3b1bdebca..671dd1a56 100644 --- a/src/omt/bitvector_optimizer.h +++ b/src/omt/bitvector_optimizer.h @@ -28,9 +28,9 @@ class OMTOptimizerBitVector : public OMTOptimizer public: OMTOptimizerBitVector(bool isSigned); virtual ~OMTOptimizerBitVector() = default; - smt::OptimizationResult minimize(SmtEngine* optChecker, + smt::OptimizationResult minimize(SolverEngine* optChecker, TNode target) override; - smt::OptimizationResult maximize(SmtEngine* optChecker, + smt::OptimizationResult maximize(SolverEngine* optChecker, TNode target) override; private: diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index b3047b390..caa29fcea 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -21,7 +21,7 @@ using namespace cvc5::smt; namespace cvc5::omt { -OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, +OptimizationResult OMTOptimizerInteger::optimize(SolverEngine* optChecker, TNode target, bool isMinimize) { @@ -71,12 +71,12 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, return OptimizationResult(lastSatResult, value); } -OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker, +OptimizationResult OMTOptimizerInteger::minimize(SolverEngine* optChecker, TNode target) { return this->optimize(optChecker, target, true); } -OptimizationResult OMTOptimizerInteger::maximize(SmtEngine* optChecker, +OptimizationResult OMTOptimizerInteger::maximize(SolverEngine* optChecker, TNode target) { return this->optimize(optChecker, target, false); diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index 0b62c0816..141597449 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -28,9 +28,9 @@ class OMTOptimizerInteger : public OMTOptimizer public: OMTOptimizerInteger() = default; virtual ~OMTOptimizerInteger() = default; - smt::OptimizationResult minimize(SmtEngine* optChecker, + smt::OptimizationResult minimize(SolverEngine* optChecker, TNode target) override; - smt::OptimizationResult maximize(SmtEngine* optChecker, + smt::OptimizationResult maximize(SolverEngine* optChecker, TNode target) override; private: @@ -39,7 +39,7 @@ class OMTOptimizerInteger : public OMTOptimizer * isMinimize = true will trigger minimization, * otherwise trigger maximization **/ - smt::OptimizationResult optimize(SmtEngine* optChecker, + smt::OptimizationResult optimize(SolverEngine* optChecker, TNode target, bool isMinimize); }; diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 1e8d9e763..f92385816 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -105,7 +105,7 @@ class OMTOptimizer * @return smt::OptimizationResult the result of optimization, containing * whether it's optimal and the optimized value. **/ - virtual smt::OptimizationResult minimize(SmtEngine* optChecker, + virtual smt::OptimizationResult minimize(SolverEngine* optChecker, TNode target) = 0; /** * Maximize the target node with constraints encoded in optChecker @@ -116,7 +116,7 @@ class OMTOptimizer * @return smt::OptimizationResult the result of optimization, containing * whether it's optimal and the optimized value. **/ - virtual smt::OptimizationResult maximize(SmtEngine* optChecker, + virtual smt::OptimizationResult maximize(SolverEngine* optChecker, TNode target) = 0; }; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 982063b6e..478edb651 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -743,7 +743,7 @@ setOptionInternal[std::unique_ptr* cmd] { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr))); // Ugly that this changes the state of the parser; but // global-declarations affects parsing, so we can't hold off - // on this until some SmtEngine eventually (if ever) executes it. + // on this until some SolverEngine eventually (if ever) executes it. if(name == ":global-declarations") { SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true"); @@ -2134,7 +2134,7 @@ symbol[std::string& id, : SIMPLE_SYMBOL { id = AntlrInput::tokenText($SIMPLE_SYMBOL); if(!PARSER_STATE->isAbstractValue(id)) { - // if an abstract value, SmtEngine handles declaration + // if an abstract value, SolverEngine handles declaration PARSER_STATE->checkDeclaration(id, check, type); } } @@ -2143,7 +2143,7 @@ symbol[std::string& id, /* strip off the quotes */ id = id.substr(1, id.size() - 2); if(!PARSER_STATE->isAbstractValue(id)) { - // if an abstract value, SmtEngine handles declaration + // if an abstract value, SolverEngine handles declaration PARSER_STATE->checkDeclaration(id, check, type); } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 0daddea40..b186c2b2a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -686,7 +686,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) { // If not from a command, just set the logic directly. Notice this is // important since we do not want to enqueue a set-logic command and - // fully initialize the underlying SmtEngine in the meantime before the + // fully initialize the underlying SolverEngine in the meantime before the // command has a chance to execute, which would lead to an error. d_solver->setLogic(logic); return nullptr; diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 2e40cbd5b..90685b9c7 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -37,7 +37,7 @@ PreprocessingPassResult ApplySubsts::applyInternal( AssertionPipeline* assertionsToPreprocess) { Chat() << "applying substitutions..." << std::endl; - Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): " + Trace("apply-substs") << "ApplySubsts::processAssertions(): " << "applying substitutions" << std::endl; // TODO(#1255): Substitutions in incremental mode should be managed with a // proper data structure. diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 9a35c2909..16ecc2d6a 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -295,7 +295,7 @@ bool SygusInference::solveSygus(const std::vector& assertions, Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; // make a separate smt call - std::unique_ptr rrSygus; + std::unique_ptr rrSygus; theory::initializeSubsolver(rrSygus, options(), logicInfo()); rrSygus->assertFormula(body); Trace("sygus-infer") << "*** Check sat..." << std::endl; diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 9d7c80812..a0d607032 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -25,11 +25,11 @@ namespace cvc5 { namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( - SmtEngine* smt, + SolverEngine* slv, Env& env, theory::booleans::CircuitPropagator* circuitPropagator) : EnvObj(env), - d_smt(smt), + d_slv(slv), d_circuitPropagator(circuitPropagator), d_llm( env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()), @@ -45,11 +45,11 @@ PreprocessingPassContext::getTopLevelSubstitutions() const TheoryEngine* PreprocessingPassContext::getTheoryEngine() const { - return d_smt->getTheoryEngine(); + return d_slv->getTheoryEngine(); } prop::PropEngine* PreprocessingPassContext::getPropEngine() const { - return d_smt->getPropEngine(); + return d_slv->getPropEngine(); } void PreprocessingPassContext::spendResource(Resource r) diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 79b89dda8..ec9d39920 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -31,7 +31,7 @@ namespace cvc5 { class Env; -class SmtEngine; +class SolverEngine; class TheoryEngine; namespace theory::booleans { @@ -49,7 +49,7 @@ class PreprocessingPassContext : protected EnvObj public: /** Constructor. */ PreprocessingPassContext( - SmtEngine* smt, + SolverEngine* smt, Env& env, theory::booleans::CircuitPropagator* circuitPropagator); @@ -120,8 +120,8 @@ class PreprocessingPassContext : protected EnvObj ProofNodeManager* getProofNodeManager() const; private: - /** Pointer to the SmtEngine that this context was created in. */ - SmtEngine* d_smt; + /** Pointer to the SolverEngine that this context was created in. */ + SolverEngine* d_slv; /** Instance of the circuit propagator */ theory::booleans::CircuitPropagator* d_circuitPropagator; /** diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 06404170c..e0b6fedbc 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -47,8 +47,8 @@ class Smt2Printer : public cvc5::Printer void toStream(std::ostream& out, const smt::Model& m) const override; /** * Writes the unsat core to the stream out. - * We use the expression names that are stored in the SMT engine associated - * with the core (UnsatCore::getSmtEngine) for printing named assertions. + * We use the expression names that are associated with the core + * (UnsatCore::getCoreNames) for printing named assertions. */ void toStream(std::ostream& out, const UnsatCore& core) const override; diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 9d288b4ed..1896edab7 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -36,9 +36,10 @@ class TptpPrinter : public cvc5::Printer size_t dag) const override; void toStream(std::ostream& out, const CommandStatus* s) const override; void toStream(std::ostream& out, const smt::Model& m) const override; - /** print unsat core to stream - * We use the expression names stored in the SMT engine associated with the - * unsat core with UnsatCore::getSmtEngine. + /** + * Print unsat core to stream. + * We use the expression names associated with the unsat core + * (UnsatCore::getCoreNames). */ void toStream(std::ostream& out, const UnsatCore& core) const override; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 664a2bf61..5a0b5f0b3 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -307,7 +307,7 @@ class CnfStream { */ SatLiteral convertAtom(TNode node); - /** Pointer to resource manager for associated SmtEngine */ + /** Pointer to resource manager for associated SolverEngine */ ResourceManager* d_resourceManager; private: diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README index 2fcf2ed49..75bdfecd7 100644 --- a/src/prop/minisat/CVC4-README +++ b/src/prop/minisat/CVC4-README @@ -1,7 +1,7 @@ ================ CHANGES TO THE ORIGINAL CODE ================================== The only cvc5 connections passed to minisat are the proxy (defined in sat.h) and -the context. The context is obtained from the SmtEngine, and the proxy is an +the context. The context is obtained from the SolverEngine, and the proxy is an intermediary class that has all-access to the SatSolver so as to simplify the interface to (possible) other sat solvers. These two are passed to minisat at construction time and some additional flags are set. We use the SimpSolver diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d26a425c8..ba2c80f46 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -71,7 +71,7 @@ class PropEngine void finishInit(); /** - * This is called by SmtEngine, at shutdown time, just before + * This is called by SolverEngine, at shutdown time, just before * destruction. It is important because there are destruction * ordering issues between some parts of the system (notably between * PropEngine and Theory). For now, there's nothing to do here in diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 0c6ff5a68..501e0c939 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -45,7 +45,8 @@ bool AbductionSolver::getAbduct(const std::vector& axioms, const char* msg = "Cannot get abduct when produce-abducts options is off."; throw ModalException(msg); } - Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl; + Trace("sygus-abduct") << "SolverEngine::getAbduct: goal " << goal + << std::endl; std::vector asserts(axioms.begin(), axioms.end()); // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(goal); @@ -60,8 +61,8 @@ bool AbductionSolver::getAbduct(const std::vector& axioms, Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1); // remember the abduct-to-synthesize d_sssf = aconj[0][0]; - Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj - << ", solving for " << d_sssf << std::endl; + Trace("sygus-abduct") << "SolverEngine::getAbduct: made conjecture : " + << aconj << ", solving for " << d_sssf << std::endl; // we generate a new smt engine to do the abduction query initializeSubsolver(d_subsolver, d_env); // get the logic @@ -87,9 +88,11 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, { // should have initialized the subsolver by now Assert(d_subsolver != nullptr); - Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl; + Trace("sygus-abduct") << " SolverEngine::getAbduct check sat..." + << std::endl; Result r = d_subsolver->checkSat(); - Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl; + Trace("sygus-abduct") << " SolverEngine::getAbduct result: " << r + << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { // get the synthesis solution @@ -99,8 +102,8 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, std::map::iterator its = sols.find(d_sssf); if (its != sols.end()) { - Trace("sygus-abduct") - << "SmtEngine::getAbduct: solution is " << its->second << std::endl; + Trace("sygus-abduct") << "SolverEngine::getAbduct: solution is " + << its->second << std::endl; abd = its->second; if (abd.getKind() == kind::LAMBDA) { @@ -132,7 +135,7 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, } return true; } - Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" + Trace("sygus-abduct") << "SolverEngine::getAbduct: could not find solution!" << std::endl; throw RecoverableModalException("Could not find solution for get-abduct."); } @@ -142,7 +145,7 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, void AbductionSolver::checkAbduct(const std::vector& axioms, Node a) { Assert(a.getType().isBoolean()); - Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions" + Trace("check-abduct") << "SolverEngine::checkAbduct: get expanded assertions" << std::endl; std::vector asserts(axioms.begin(), axioms.end()); @@ -152,21 +155,21 @@ void AbductionSolver::checkAbduct(const std::vector& axioms, Node a) // is unsatisfiable. for (unsigned j = 0; j < 2; j++) { - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j << ": make new SMT engine" << std::endl; // Start new SMT engine to check solution - std::unique_ptr abdChecker; + std::unique_ptr abdChecker; initializeSubsolver(abdChecker, d_env); - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j << ": asserting formulas" << std::endl; for (const Node& e : asserts) { abdChecker->assertFormula(e); } - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j << ": check the assertions" << std::endl; Result r = abdChecker->checkSat(); - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j << ": result is " << r << std::endl; std::stringstream serr; bool isError = false; @@ -175,12 +178,13 @@ void AbductionSolver::checkAbduct(const std::vector& axioms, Node a) if (r.asSatisfiabilityResult().isSat() != Result::SAT) { isError = true; - serr << "SmtEngine::checkAbduct(): produced solution cannot be shown " - "to be consisconsistenttent with assertions, result was " - << r; + serr + << "SolverEngine::checkAbduct(): produced solution cannot be shown " + "to be consisconsistenttent with assertions, result was " + << r; } Trace("check-abduct") - << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl; + << "SolverEngine::checkAbduct: goal is " << d_abdConj << std::endl; // add the goal to the set of assertions Assert(!d_abdConj.isNull()); asserts.push_back(d_abdConj); @@ -190,7 +194,7 @@ void AbductionSolver::checkAbduct(const std::vector& axioms, Node a) if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { isError = true; - serr << "SmtEngine::checkAbduct(): negated goal cannot be shown " + serr << "SolverEngine::checkAbduct(): negated goal cannot be shown " "unsatisfiable with produced solution, result was " << r; } diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index 3ea2755ae..326713418 100644 --- a/src/smt/abduction_solver.h +++ b/src/smt/abduction_solver.h @@ -24,7 +24,7 @@ namespace cvc5 { -class SmtEngine; +class SolverEngine; namespace smt { @@ -32,7 +32,7 @@ namespace smt { * A solver for abduction queries. * * This class is responsible for responding to get-abduct commands. It spawns - * a subsolver SmtEngine for a sygus conjecture that captures the abduction + * a subsolver SolverEngine for a sygus conjecture that captures the abduction * query, and implements supporting utility methods such as checkAbduct. */ class AbductionSolver : protected EnvObj @@ -108,10 +108,10 @@ class AbductionSolver : protected EnvObj * assertion stack unchaged. This copy of the SMT engine can be further * queried for information regarding further solutions. */ - std::unique_ptr d_subsolver; + std::unique_ptr d_subsolver; /** * The conjecture of the current abduction problem. This expression is only - * valid while the parent SmtEngine is in mode SMT_MODE_ABDUCT. + * valid while the parent SolverEngine is in mode SMT_MODE_ABDUCT. */ Node d_abdConj; /** diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 02ae86317..704a36915 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -155,8 +155,7 @@ void Assertions::addFormula(TNode n, // true, nothing to do return; } - Trace("smt") << "SmtEnginePrivate::addFormula(" << n - << ", inInput = " << inInput + Trace("smt") << "Assertions::addFormula(" << n << ", inInput = " << inInput << ", isAssumption = " << isAssumption << ", isFunDef = " << isFunDef << std::endl; if (isFunDef) diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 304d261a6..f928a2ce8 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -59,7 +59,7 @@ void CheckModels::checkModel(TheoryModel* m, // Now go through all our user assertions checking if they're satisfied. for (const Node& assertion : *al) { - Notice() << "SmtEngine::checkModel(): checking assertion " << assertion + Notice() << "SolverEngine::checkModel(): checking assertion " << assertion << std::endl; // Apply any define-funs from the problem. We do not expand theory symbols @@ -68,16 +68,17 @@ void CheckModels::checkModel(TheoryModel* m, // is not trustworthy, since the UF introduced by expanding definitions may // not be properly constrained. Node n = sm.apply(assertion, false); - Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::endl; + Notice() << "SolverEngine::checkModel(): -- substitutes to " << n + << std::endl; n = Rewriter::rewrite(n); - Notice() << "SmtEngine::checkModel(): -- rewrites to " << n << std::endl; + Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl; // We look up the value before simplifying. If n contains quantifiers, // this may increases the chance of finding its value before the node is // altered by simplification below. n = m->getValue(n); - Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl; + Notice() << "SolverEngine::checkModel(): -- get value : " << n << std::endl; if (n.isConst() && n.getConst()) { @@ -103,18 +104,19 @@ void CheckModels::checkModel(TheoryModel* m, if (!n.isConst()) { // Not constant, print a less severe warning message here. - Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified " - "assertion : " - << n << std::endl; + Warning() + << "Warning : SolverEngine::checkModel(): cannot check simplified " + "assertion : " + << n << std::endl; noCheckList.push_back(n); continue; } // Assertions that simplify to false result in an InternalError or // Warning being thrown below (when hardFailure is false). - Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" + Notice() << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << std::endl; std::stringstream ss; - ss << "SmtEngine::checkModel(): " + ss << "SolverEngine::checkModel(): " << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl << "assertion: " << assertion << std::endl << "simplifies to: " << n << std::endl @@ -132,7 +134,7 @@ void CheckModels::checkModel(TheoryModel* m, } if (noCheckList.empty()) { - Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" + Notice() << "SolverEngine::checkModel(): all assertions checked out OK !" << std::endl; return; } diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 27c7cc574..b6e0ccfa2 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The dump manager of the SmtEngine. + * The dump manager of the SolverEngine. */ #include "cvc5_private.h" @@ -44,12 +44,12 @@ class DumpManager DumpManager(context::UserContext* u); ~DumpManager(); /** - * Finish init, called during SmtEngine::finishInit, which is triggered + * Finish init, called during SolverEngine::finishInit, which is triggered * when initialization of options is finished. */ void finishInit(); /** - * Reset assertions, called on SmtEngine::resetAssertions. + * Reset assertions, called on SolverEngine::resetAssertions. */ void resetAssertions(); /** @@ -68,7 +68,7 @@ class DumpManager bool d_fullyInited; /** * A vector of declaration commands waiting to be dumped out. - * Once the SmtEngine is fully initialized, we'll dump them. + * Once the SolverEngine is fully initialized, we'll dump them. * This ensures the declarations come after the set-logic and * any necessary set-option commands are dumped. */ diff --git a/src/smt/env.h b/src/smt/env.h index 426749f5c..e3a34cf4a 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -54,12 +54,12 @@ class TrustSubstitutionMap; /** * The environment class. * - * This class lives in the SmtEngine and contains all utilities that are + * This class lives in the SolverEngine and contains all utilities that are * globally available to all internal code. */ class Env { - friend class SmtEngine; + friend class SolverEngine; friend class smt::PfManager; public: @@ -82,8 +82,8 @@ class Env /** * Get the underlying proof node manager. Note since proofs depend on option - * initialization, this is only available after the SmtEngine that owns this - * environment is initialized, and only non-null if proofs are enabled. + * initialization, this is only available after the SolverEngine that owns + * this environment is initialized, and only non-null if proofs are enabled. */ ProofNodeManager* getProofNodeManager(); @@ -217,12 +217,12 @@ class Env std::unique_ptr d_userContext; /** * A pointer to the node manager of this environment. A node manager is - * not necessarily unique to an SmtEngine instance. + * not necessarily unique to an SolverEngine instance. */ NodeManager* d_nodeManager; /** * A pointer to the proof node manager, which is non-null if proofs are - * enabled. This is owned by the proof manager of the SmtEngine that owns + * enabled. This is owned by the proof manager of the SolverEngine that owns * this environment. */ ProofNodeManager* d_proofNodeManager; @@ -230,7 +230,7 @@ class Env * The rewriter owned by this Env. We have a different instance * of the rewriter for each Env instance. This is because rewriters may * hold references to objects that belong to theory solvers, which are - * specific to an SmtEngine/TheoryEngine instance. + * specific to an SolverEngine/TheoryEngine instance. */ std::unique_ptr d_rewriter; /** Evaluator that also invokes the rewriter */ @@ -256,7 +256,7 @@ class Env std::unique_ptr d_statisticsRegistry; /** * The options object, which contains the modified version of the options - * provided as input to the SmtEngine that owns this environment. Note + * provided as input to the SolverEngine that owns this environment. Note * that d_options may be modified by the options manager, e.g. based * on the input logic. * diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 923f14272..51be8db51 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -47,7 +47,7 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, "Cannot get interpolation when produce-interpol options is off."; throw ModalException(msg); } - Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj + Trace("sygus-interpol") << "SolverEngine::getInterpol: conjecture " << conj << std::endl; // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(conj); @@ -79,8 +79,8 @@ void InterpolationSolver::checkInterpol(Node interpol, const Node& conj) { Assert(interpol.getType().isBoolean()); - Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions" - << std::endl; + Trace("check-interpol") + << "SolverEngine::checkInterpol: get expanded assertions" << std::endl; // two checks: first, axioms imply interpol, second, interpol implies conj. for (unsigned j = 0; j < 2; j++) @@ -88,14 +88,14 @@ void InterpolationSolver::checkInterpol(Node interpol, if (j == 1) { Trace("check-interpol") - << "SmtEngine::checkInterpol: conjecture is " << conj << std::endl; + << "SolverEngine::checkInterpol: conjecture is " << conj << std::endl; } - Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j << ": make new SMT engine" << std::endl; // Start new SMT engine to check solution - std::unique_ptr itpChecker; + std::unique_ptr itpChecker; initializeSubsolver(itpChecker, d_env); - Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j << ": asserting formulas" << std::endl; if (j == 0) { @@ -112,27 +112,28 @@ void InterpolationSolver::checkInterpol(Node interpol, Assert(!conj.isNull()); itpChecker->assertFormula(conj.notNode()); } - Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j << ": check the assertions" << std::endl; Result r = itpChecker->checkSat(); - Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j << ": result is " << r << std::endl; std::stringstream serr; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { if (j == 0) { - serr << "SmtEngine::checkInterpol(): negated produced solution cannot " + serr << "SolverEngine::checkInterpol(): negated produced solution " + "cannot " "be shown " "satisfiable with assertions, result was " << r; } else { - serr - << "SmtEngine::checkInterpol(): negated conjecture cannot be shown " - "satisfiable with produced solution, result was " - << r; + serr << "SolverEngine::checkInterpol(): negated conjecture cannot be " + "shown " + "satisfiable with produced solution, result was " + << r; } InternalError() << serr.str(); } diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 03c899ead..39a241816 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -29,8 +29,9 @@ namespace smt { * A solver for interpolation queries. * * This class is responsible for responding to get-interpol commands. It spawns - * a subsolver SmtEngine for a sygus conjecture that captures the interpolation - * query, and implements supporting utility methods such as checkInterpol. + * a subsolver SolverEngine for a sygus conjecture that captures the + * interpolation query, and implements supporting utility methods such as + * checkInterpol. */ class InterpolationSolver : protected EnvObj { diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 816a49a85..f10d039b8 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -29,13 +29,13 @@ namespace cvc5 { namespace smt { -ResourceOutListener::ResourceOutListener(SmtEngine& smt) : d_smt(smt) {} +ResourceOutListener::ResourceOutListener(SolverEngine& slv) : d_slv(slv) {} void ResourceOutListener::notify() { - SmtScope scope(&d_smt); + SmtScope scope(&d_slv); Assert(smt::smtEngineInScope()); - d_smt.interrupt(); + d_slv.interrupt(); } SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm, diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 5c96d45fd..60ec6b4ed 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -26,7 +26,7 @@ namespace cvc5 { class OutputManager; -class SmtEngine; +class SolverEngine; namespace smt { @@ -34,13 +34,13 @@ namespace smt { class ResourceOutListener : public Listener { public: - ResourceOutListener(SmtEngine& smt); - /** notify method, interupts SmtEngine */ + ResourceOutListener(SolverEngine& smt); + /** notify method, interupts SolverEngine */ void notify() override; private: - /** Reference to the SmtEngine */ - SmtEngine& d_smt; + /** Reference to the SolverEngine */ + SolverEngine& d_slv; }; class DumpManager; diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index a62a315c1..30c338d65 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -92,7 +92,7 @@ std::ostream& operator<<(std::ostream& out, return out; } -OptimizationSolver::OptimizationSolver(SmtEngine* parent) +OptimizationSolver::OptimizationSolver(SolverEngine* parent) : d_parent(parent), d_optChecker(), d_objectives(parent->getUserContext()), @@ -142,10 +142,10 @@ std::vector OptimizationSolver::getValues() return d_results; } -std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( - SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) +std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( + SolverEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { - std::unique_ptr optChecker; + std::unique_ptr optChecker; // initializeSubSolver will copy the options and theories enabled // from the current solver to optChecker and adds timeout theory::initializeSubsolver( diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 04a960282..044500c14 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -27,7 +27,7 @@ namespace cvc5 { class Env; -class SmtEngine; +class SolverEngine; namespace smt { @@ -186,7 +186,7 @@ std::ostream& operator<<(std::ostream& out, * A solver for optimization queries. * * This class is responsible for responding to optmization queries. It - * spawns a subsolver SmtEngine that captures the parent assertions and + * spawns a subsolver SolverEngine that captures the parent assertions and * implements a linear optimization loop. Supports activateObjective, * checkOpt, and objectiveGetValue in that order. */ @@ -222,7 +222,7 @@ class OptimizationSolver * Constructor * @param parent the smt_solver that the user added their assertions to **/ - OptimizationSolver(SmtEngine* parent); + OptimizationSolver(SolverEngine* parent); ~OptimizationSolver() = default; /** @@ -263,8 +263,8 @@ class OptimizationSolver * @param timeout the timeout value, given in milliseconds (ms) * @return a unique_pointer of SMT subsolver **/ - static std::unique_ptr createOptCheckerWithTimeout( - SmtEngine* parentSMTSolver, + static std::unique_ptr createOptCheckerWithTimeout( + SolverEngine* parentSMTSolver, bool needsTimeout = false, unsigned long timeout = 0); @@ -311,10 +311,10 @@ class OptimizationSolver Result optimizeParetoNaiveGIA(); /** A pointer to the parent SMT engine **/ - SmtEngine* d_parent; + SolverEngine* d_parent; /** A subsolver for offline optimization **/ - std::unique_ptr d_optChecker; + std::unique_ptr d_optChecker; /** The objectives to optimize for **/ context::CDList d_objectives; diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index 03995fdc5..0a363c08a 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -20,13 +20,13 @@ namespace cvc5 { -OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {} +OutputManager::OutputManager(SolverEngine* slv) : d_slv(slv) {} -const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); } +const Printer& OutputManager::getPrinter() const { return d_slv->getPrinter(); } std::ostream& OutputManager::getDumpOut() const { - return *d_smt->getOptions().base.out; + return *d_slv->getOptions().base.out; } } // namespace cvc5 diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h index bb7645f75..34dcc41b4 100644 --- a/src/smt/output_manager.h +++ b/src/smt/output_manager.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The output manager for the SmtEngine. + * The output manager for the SolverEngine. * * The output manager provides helper functions for printing commands * internally. @@ -24,7 +24,7 @@ namespace cvc5 { class Printer; -class SmtEngine; +class SolverEngine; /** This utility class provides helper functions for printing commands * internally */ @@ -35,7 +35,7 @@ class OutputManager * * @param smt SMT engine to manage output for */ - explicit OutputManager(SmtEngine* smt); + explicit OutputManager(SolverEngine* smt); /** Get the current printer based on the current options * @@ -50,7 +50,7 @@ class OutputManager std::ostream& getDumpOut() const; private: - SmtEngine* d_smt; + SolverEngine* d_slv; }; } // namespace cvc5 diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index e63877c22..fd736860d 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -35,17 +35,17 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -Preprocessor::Preprocessor(SmtEngine& smt, +Preprocessor::Preprocessor(SolverEngine& slv, Env& env, AbstractValues& abs, SmtEngineStatistics& stats) - : d_smt(smt), + : d_slv(slv), d_env(env), d_absValues(abs), d_propagator(true, true), d_assertionsProcessed(env.getUserContext(), false), d_exDefs(env, stats), - d_processor(smt, *env.getResourceManager(), stats), + d_processor(slv, *env.getResourceManager(), stats), d_pnm(nullptr) { } @@ -62,7 +62,7 @@ Preprocessor::~Preprocessor() void Preprocessor::finishInit() { d_ppContext.reset(new preprocessing::PreprocessingPassContext( - &d_smt, d_env, &d_propagator)); + &d_slv, d_env, &d_propagator)); // initialize the preprocessing passes d_processor.finishInit(d_ppContext.get()); @@ -149,8 +149,8 @@ Node Preprocessor::simplify(const Node& node) Trace("smt") << "SMT simplify(" << node << ")" << endl; if (Dump.isOn("benchmark")) { - d_smt.getOutputManager().getPrinter().toStreamCmdSimplify( - d_smt.getOutputManager().getDumpOut(), node); + d_slv.getOutputManager().getPrinter().toStreamCmdSimplify( + d_slv.getOutputManager().getDumpOut(), node); } Node ret = expandDefinitions(node); ret = theory::Rewriter::rewrite(ret); diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 03246ed67..2f5775ceb 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The preprocessor of the SmtEngine. + * The preprocessor of the SolverEngine. */ #include "cvc5_private.h" @@ -46,7 +46,7 @@ class PreprocessProofGenerator; class Preprocessor { public: - Preprocessor(SmtEngine& smt, + Preprocessor(SolverEngine& smt, Env& env, AbstractValues& abs, SmtEngineStatistics& stats); @@ -67,7 +67,7 @@ class Preprocessor /** * Cleanup, which deletes the processing passes owned by this module. This * is required to be done explicitly so that passes are deleted before the - * objects they refer to in the SmtEngine destructor. + * objects they refer to in the SolverEngine destructor. */ void cleanup(); /** @@ -98,8 +98,8 @@ class Preprocessor void setProofGenerator(PreprocessProofGenerator* pppg); private: - /** Reference to the parent SmtEngine */ - SmtEngine& d_smt; + /** Reference to the parent SolverEngine */ + SolverEngine& d_slv; /** Reference to the env */ Env& d_env; /** Reference to the abstract values utility */ diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 1fd47352e..c1f60530d 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -57,10 +57,10 @@ class ScopeCounter unsigned& d_depth; }; -ProcessAssertions::ProcessAssertions(SmtEngine& smt, +ProcessAssertions::ProcessAssertions(SolverEngine& slv, ResourceManager& rm, SmtEngineStatistics& stats) - : d_smt(smt), + : d_slv(slv), d_resourceManager(rm), d_smtStats(stats), d_preprocessingPassContext(nullptr) @@ -229,7 +229,7 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["sep-skolem-emp"]->apply(&assertions); } - if (d_smt.getLogicInfo().isQuantified()) + if (d_slv.getLogicInfo().isQuantified()) { // remove rewrite rules, apply pre-skolemization to existential quantifiers d_passes["quantifiers-preprocess"]->apply(&assertions); @@ -256,7 +256,7 @@ bool ProcessAssertions::apply(Assertions& as) } // rephrasing normal inputs as sygus problems - if (!d_smt.isInternalSubsolver()) + if (!d_slv.isInternalSubsolver()) { if (options::sygusInference()) { @@ -347,7 +347,7 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["bv-eager-atoms"]->apply(&assertions); } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; + Trace("smt-proc") << "ProcessAssertions::apply() end" << endl; dumpAssertions("post-everything", assertions); return noConflict; @@ -361,7 +361,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) { ScopeCounter depth(d_simplifyAssertionsDepth); - Trace("simplify") << "SmtEnginePrivate::simplify()" << endl; + Trace("simplify") << "ProcessAssertions::simplify()" << endl; if (options::simplificationMode() != options::SimplificationMode::NONE) { @@ -378,7 +378,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) if ( // check that option is on options::arithMLTrick() && // only useful in arith - d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) && + d_slv.getLogicInfo().isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) @@ -388,7 +388,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) } else { - Trace("simplify") << "SmtEnginePrivate::simplify(): " + Trace("simplify") << "ProcessAssertions::simplify(): " << "skipping miplib pseudobooleans pass..." << endl; } } @@ -453,8 +453,8 @@ void ProcessAssertions::dumpAssertions(const char* key, for (unsigned i = 0; i < assertionList.size(); ++i) { TNode n = assertionList[i]; - d_smt.getOutputManager().getPrinter().toStreamCmdAssert( - d_smt.getOutputManager().getDumpOut(), n); + d_slv.getOutputManager().getPrinter().toStreamCmdAssert( + d_slv.getOutputManager().getDumpOut(), n); } } } diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 80219eb3c..d04663fe2 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -26,7 +26,7 @@ namespace cvc5 { -class SmtEngine; +class SolverEngine; namespace preprocessing { class AssertionPipeline; @@ -60,7 +60,7 @@ class ProcessAssertions typedef std::unordered_map NodeToBoolHashMap; public: - ProcessAssertions(SmtEngine& smt, + ProcessAssertions(SolverEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats); ~ProcessAssertions(); @@ -82,7 +82,7 @@ class ProcessAssertions private: /** Reference to the SMT engine */ - SmtEngine& d_smt; + SolverEngine& d_slv; /** Reference to resource manager */ ResourceManager& d_resourceManager; /** Reference to the SMT stats */ diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index d5e07991a..6aaa6e267 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -105,12 +105,12 @@ void PfManager::setFinalProof(std::shared_ptr pfn, Assertions& as) { // Note this assumes that setFinalProof is only called once per unsat // response. This method would need to cache its result otherwise. - Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n"; + Trace("smt-proof") << "SolverEngine::setFinalProof(): get proof body...\n"; if (Trace.isOn("smt-proof-debug")) { Trace("smt-proof-debug") - << "SmtEngine::setFinalProof(): Proof node for false:\n"; + << "SolverEngine::setFinalProof(): Proof node for false:\n"; Trace("smt-proof-debug") << *pfn.get() << std::endl; Trace("smt-proof-debug") << "=====" << std::endl; } @@ -120,18 +120,19 @@ void PfManager::setFinalProof(std::shared_ptr pfn, Assertions& as) if (Trace.isOn("smt-proof")) { - Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..." - << std::endl; + Trace("smt-proof") + << "SolverEngine::setFinalProof(): get free assumptions..." + << std::endl; std::vector fassumps; expr::getFreeAssumptions(pfn.get(), fassumps); Trace("smt-proof") - << "SmtEngine::setFinalProof(): initial free assumptions are:\n"; + << "SolverEngine::setFinalProof(): initial free assumptions are:\n"; for (const Node& a : fassumps) { Trace("smt-proof") << "- " << a << std::endl; } - Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n"; + Trace("smt-proof") << "SolverEngine::setFinalProof(): assertions are:\n"; for (const Node& n : assertions) { Trace("smt-proof") << "- " << n << std::endl; @@ -139,16 +140,16 @@ void PfManager::setFinalProof(std::shared_ptr pfn, Assertions& as) Trace("smt-proof") << "=====" << std::endl; } - Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n"; + Trace("smt-proof") << "SolverEngine::setFinalProof(): postprocess...\n"; Assert(d_pfpp != nullptr); d_pfpp->process(pfn); - Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n"; + Trace("smt-proof") << "SolverEngine::setFinalProof(): make scope...\n"; // Now make the final scope, which ensures that the only open leaves of the // proof are the assertions. d_finalProof = d_pnm->mkScope(pfn, assertions); - Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; + Trace("smt-proof") << "SolverEngine::setFinalProof(): finished.\n"; } void PfManager::printProof(std::ostream& out, diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 45be71771..266644668 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The proof manager of SmtEngine. + * The proof manager of SolverEngine. */ #include "cvc5_private.h" @@ -27,7 +27,7 @@ namespace cvc5 { class ProofChecker; class ProofNode; class ProofNodeManager; -class SmtEngine; +class SolverEngine; namespace rewriter { class RewriteDb; @@ -40,18 +40,18 @@ class PreprocessProofGenerator; class ProofPostproccess; /** - * This class is responsible for managing the proof output of SmtEngine, as + * This class is responsible for managing the proof output of SolverEngine, as * well as setting up the global proof checker and proof node manager. * - * The proof production of an SmtEngine is directly impacted by whether, and + * The proof production of an SolverEngine is directly impacted by whether, and * how, we are producing unsat cores: * * - If we are producing unsat cores using the old proof infrastructure, then - * SmtEngine will not have proofs in the sense of this proof manager. + * SolverEngine will not have proofs in the sense of this proof manager. * * - If we are producing unsat cores using this proof infrastructure, then the - * SmtEngine will have proofs using this proof manager, according to the unsat - * core mode: + * SolverEngine will have proofs using this proof manager, according to the + * unsat core mode: * * - assumption mode: proofs only for preprocessing, not in sat solver or * theory engine, and level of granularity set to off (unless otherwise @@ -66,11 +66,11 @@ class ProofPostproccess; * Note that if --produce-proofs is set then full-proof mode of unsat cores is * forced. * - * - If we are not producing unsat cores then the SmtEngine will have proofs as - * long as --produce-proofs is on. + * - If we are not producing unsat cores then the SolverEngine will have proofs + * as long as --produce-proofs is on. * - * - If SmtEngine has been configured in a way that is incompatible with proofs - * then unsat core production will be disabled. + * - If SolverEngine has been configured in a way that is incompatible with + * proofs then unsat core production will be disabled. */ class PfManager : protected EnvObj { @@ -157,7 +157,7 @@ class PfManager : protected EnvObj * connected by setFinalProof(). */ std::shared_ptr d_finalProof; -}; /* class SmtEngine */ +}; /* class SolverEngine */ } // namespace smt } // namespace cvc5 diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index c0cc7bc17..27adc5eed 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -39,7 +39,7 @@ class RewriteDb; namespace smt { /** - * A callback class used by SmtEngine for post-processing proof nodes by + * A callback class used by SolverEngine for post-processing proof nodes by * connecting proofs of preprocessing, and expanding macro PfRule applications. */ class ProofPostprocessCallback : public ProofNodeUpdaterCallback @@ -244,7 +244,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback /** * The proof postprocessor module. This postprocesses the final proof - * produced by an SmtEngine. Its main two tasks are to: + * produced by an SolverEngine. Its main two tasks are to: * (1) Connect proofs of preprocessing, * (2) Expand macro PfRule applications. */ diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 08ba5b416..5ccb2cf14 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -103,7 +103,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, std::vector insts; qe->getInstantiations(topq, insts); // note we do not convert to witness form here, since we could be - // an internal subsolver (SmtEngine::isInternalSubsolver). + // an internal subsolver (SolverEngine::isInternalSubsolver). ret = nm->mkAnd(insts); Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; if (q.getKind() == EXISTS) diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index a0b43d09d..3c9c5989e 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -51,7 +51,7 @@ class QuantElimSolver : protected EnvObj * elimination is LRA and LIA. * * This function returns a formula ret such that, given - * the current set of formulas A asserted to this SmtEngine : + * the current set of formulas A asserted to this SolverEngine : * * If doFull = true, then * - ( A ^ q ) and ( A ^ ret ) are equivalent @@ -82,10 +82,10 @@ class QuantElimSolver : protected EnvObj * for incrementally computing the result of a * quantifier elimination. * - * @param as The assertions of the SmtEngine + * @param as The assertions of the SolverEngine * @param q The quantified formula we are eliminating quantifiers from * @param doFull Whether we are doing full quantifier elimination on q - * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * @param isInternalSubsolver Whether the SolverEngine we belong to is an * internal subsolver. If it is not, then we convert the final result to * witness form. * @return The result of eliminating quantifiers from q. diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4d5e898fe..e174570fb 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -156,12 +156,12 @@ void SetDefaults::setDefaultsPre(Options& opts) if (opts.bv.bitvectorAigSimplificationsWasSetByUser) { - Notice() << "SmtEngine: setting bitvectorAig" << std::endl; + Notice() << "SolverEngine: setting bitvectorAig" << std::endl; opts.bv.bitvectorAig = true; } if (opts.bv.bitvectorAlgebraicBudgetWasSetByUser) { - Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; + Notice() << "SolverEngine: setting bitvectorAlgebraicSolver" << std::endl; opts.bv.bitvectorAlgebraicSolver = true; } @@ -173,7 +173,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { opts.smt.unsatCores = false; opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - Notice() << "SmtEngine: turning off produce-proofs due to " + Notice() << "SolverEngine: turning off produce-proofs due to " << reasonNoProofs.str() << "." << std::endl; opts.smt.produceProofs = false; opts.smt.checkProofs = false; @@ -213,8 +213,9 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const "for the combination of bit-vectors with arrays or uinterpreted " "functions. Try --bitblast=lazy")); } - Notice() << "SmtEngine: setting bit-blast mode to lazy to support model" - << "generation" << std::endl; + Notice() + << "SolverEngine: setting bit-blast mode to lazy to support model" + << "generation" << std::endl; opts.bv.bitblastMode = options::BitblastMode::LAZY; } else if (!opts.base.incrementalSolving) @@ -271,7 +272,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const throw OptionException(std::string( "Ackermannization currently does not support model generation.")); } - Notice() << "SmtEngine: turn off ackermannization to support model" + Notice() << "SolverEngine: turn off ackermannization to support model" << "generation" << std::endl; opts.smt.ackermann = false; } @@ -378,7 +379,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.produceProofs) && !opts.smt.produceAssertions) { - Notice() << "SmtEngine: turning on produce-assertions to support " + Notice() << "SolverEngine: turning on produce-assertions to support " << "option requiring assertions." << std::endl; opts.smt.produceAssertions = true; } @@ -466,8 +467,9 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const "bool-to-bv != off not supported with CBQI BV for quantified " "logics"); } - Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" - << std::endl; + Notice() + << "SolverEngine: turning off bool-to-bitvector to support CBQI BV" + << std::endl; opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } } @@ -477,7 +479,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck || usesSygus(opts))) { - Notice() << "SmtEngine: turning on produce-models" << std::endl; + Notice() << "SolverEngine: turning on produce-models" << std::endl; opts.smt.produceModels = true; } @@ -582,7 +584,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const throw OptionException( "bool-to-bv=all not supported for non-bitvector logics."); } - Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: " + Notice() << "SolverEngine: turning off bool-to-bv for non-bv logic: " << logic.getLogicString() << std::endl; opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } @@ -731,7 +733,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (opts.theory.relevanceFilterWasSetByUser) { - Warning() << "SmtEngine: turning on relevance filtering to support " + Warning() << "SolverEngine: turning on relevance filtering to support " "--nl-ext-rlv=" << opts.arith.nlRlvMode << std::endl; } @@ -768,7 +770,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const ss << "Cannot use " << sOptNoModel << " with model generation."; throw OptionException(ss.str()); } - Notice() << "SmtEngine: turning off produce-models to support " + Notice() << "SolverEngine: turning off produce-models to support " << sOptNoModel << std::endl; opts.smt.produceModels = false; } @@ -781,7 +783,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << " with model generation (produce-assignments)."; throw OptionException(ss.str()); } - Notice() << "SmtEngine: turning off produce-assignments to support " + Notice() << "SolverEngine: turning off produce-assignments to support " << sOptNoModel << std::endl; opts.smt.produceAssignments = false; } @@ -794,7 +796,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << " with model generation (check-models)."; throw OptionException(ss.str()); } - Notice() << "SmtEngine: turning off check-models to support " + Notice() << "SolverEngine: turning off check-models to support " << sOptNoModel << std::endl; opts.smt.checkModels = false; } @@ -963,7 +965,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "unconstrained simplification"; return true; } - Notice() << "SmtEngine: turning off unconstrained simplification to " + Notice() << "SolverEngine: turning off unconstrained simplification to " "support incremental solving" << std::endl; opts.smt.unconstrainedSimp = false; @@ -982,7 +984,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inference"; return true; } - Notice() << "SmtEngine: turning off sygus inference to support " + Notice() << "SolverEngine: turning off sygus inference to support " "incremental solving" << std::endl; opts.quantifiers.sygusInference = false; @@ -1014,7 +1016,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "simplification"; return true; } - Notice() << "SmtEngine: turning off simplification to support unsat " + Notice() << "SolverEngine: turning off simplification to support unsat " "cores" << std::endl; opts.smt.simplificationMode = options::SimplificationMode::NONE; @@ -1027,7 +1029,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "learned rewrites"; return true; } - Notice() << "SmtEngine: turning off learned rewrites to support " + Notice() << "SolverEngine: turning off learned rewrites to support " "unsat cores\n"; opts.smt.learnedRewrite = false; } @@ -1039,7 +1041,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pseudoboolean rewrites"; return true; } - Notice() << "SmtEngine: turning off pseudoboolean rewrites to support " + Notice() << "SolverEngine: turning off pseudoboolean rewrites to support " "unsat cores\n"; opts.arith.pbRewrites = false; } @@ -1051,7 +1053,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "sort inference"; return true; } - Notice() << "SmtEngine: turning off sort inference to support unsat " + Notice() << "SolverEngine: turning off sort inference to support unsat " "cores\n"; opts.smt.sortInference = false; } @@ -1063,7 +1065,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pre-skolemization"; return true; } - Notice() << "SmtEngine: turning off pre-skolemization to support " + Notice() << "SolverEngine: turning off pre-skolemization to support " "unsat cores\n"; opts.quantifiers.preSkolemQuant = false; } @@ -1075,7 +1077,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bv-to-bool"; return true; } - Notice() << "SmtEngine: turning off bitvector-to-bool to support " + Notice() << "SolverEngine: turning off bitvector-to-bool to support " "unsat cores\n"; opts.bv.bitvectorToBool = false; } @@ -1087,7 +1089,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bool-to-bv != off"; return true; } - Notice() << "SmtEngine: turning off bool-to-bv to support unsat cores\n"; + Notice() << "SolverEngine: turning off bool-to-bv to support unsat cores\n"; opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } @@ -1098,7 +1100,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bv-intro-pow2"; return true; } - Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat cores"; + Notice() + << "SolverEngine: turning off bv-intro-pow2 to support unsat cores"; opts.bv.bvIntroducePow2 = false; } @@ -1109,7 +1112,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "repeat-simp"; return true; } - Notice() << "SmtEngine: turning off repeat-simp to support unsat cores\n"; + Notice() + << "SolverEngine: turning off repeat-simp to support unsat cores\n"; opts.smt.repeatSimp = false; } @@ -1120,7 +1124,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "global-negate"; return true; } - Notice() << "SmtEngine: turning off global-negate to support unsat " + Notice() << "SolverEngine: turning off global-negate to support unsat " "cores\n"; opts.quantifiers.globalNegate = false; } @@ -1143,7 +1147,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "unconstrained simplification"; return true; } - Notice() << "SmtEngine: turning off unconstrained simplification to " + Notice() << "SolverEngine: turning off unconstrained simplification to " "support unsat cores" << std::endl; opts.smt.unconstrainedSimp = false; @@ -1287,7 +1291,7 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, if (opts.quantifiers.instMaxLevel != -1) { - Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" + Notice() << "SolverEngine: turning off cbqi to support instMaxLevel" << std::endl; opts.quantifiers.cegqi = false; } diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 4d1bf5bcb..31e2c3e41 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -31,17 +31,17 @@ class SetDefaults public: /** * @param isInternalSubsolver Whether we are setting the options for an - * internal subsolver (see SmtEngine::isInternalSubsolver). + * internal subsolver (see SolverEngine::isInternalSubsolver). */ SetDefaults(bool isInternalSubsolver); /** * The purpose of this method is to set the default options and update the * logic info for an SMT engine. * - * @param logic A reference to the logic of SmtEngine, which can be + * @param logic A reference to the logic of SolverEngine, which can be * updated by this method based on the current options and the logic itself. * @param opts The options to modify, typically the main options of the - * SmtEngine in scope. + * SolverEngine in scope. */ void setDefaults(LogicInfo& logic, Options& opts); diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 2dcb4fa23..07a0c1e4c 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -26,39 +26,41 @@ namespace cvc5 { namespace smt { -thread_local SmtEngine* s_smtEngine_current = NULL; +thread_local SolverEngine* s_slvEngine_current = nullptr; -SmtEngine* currentSmtEngine() { - Assert(s_smtEngine_current != NULL); - return s_smtEngine_current; +SolverEngine* currentSolverEngine() +{ + Assert(s_slvEngine_current != nullptr); + return s_slvEngine_current; } -bool smtEngineInScope() { return s_smtEngine_current != NULL; } +bool smtEngineInScope() { return s_slvEngine_current != nullptr; } ResourceManager* currentResourceManager() { - return s_smtEngine_current->getResourceManager(); + return s_slvEngine_current->getResourceManager(); } -SmtScope::SmtScope(const SmtEngine* smt) - : d_oldSmtEngine(s_smtEngine_current), - d_optionsScope(smt ? &const_cast(smt)->getOptions() : nullptr) +SmtScope::SmtScope(const SolverEngine* smt) + : d_oldSlvEngine(s_slvEngine_current), + d_optionsScope(smt ? &const_cast(smt)->getOptions() + : nullptr) { - Assert(smt != NULL); - s_smtEngine_current = const_cast(smt); - Debug("current") << "smt scope: " << s_smtEngine_current << std::endl; + Assert(smt != nullptr); + s_slvEngine_current = const_cast(smt); + Debug("current") << "smt scope: " << s_slvEngine_current << std::endl; } SmtScope::~SmtScope() { - s_smtEngine_current = d_oldSmtEngine; - Debug("current") << "smt scope: returning to " << s_smtEngine_current + s_slvEngine_current = d_oldSlvEngine; + Debug("current") << "smt scope: returning to " << s_slvEngine_current << std::endl; } StatisticsRegistry& SmtScope::currentStatisticsRegistry() { Assert(smtEngineInScope()); - return s_smtEngine_current->getStatisticsRegistry(); + return s_slvEngine_current->getStatisticsRegistry(); } } // namespace smt diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index f9b024a3b..a4c1f0eaf 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -27,12 +27,12 @@ namespace cvc5 { -class SmtEngine; +class SolverEngine; class StatisticsRegistry; namespace smt { -SmtEngine* currentSmtEngine(); +SolverEngine* currentSolverEngine(); bool smtEngineInScope(); /** get the current resource manager */ @@ -41,17 +41,17 @@ ResourceManager* currentResourceManager(); class SmtScope { public: - SmtScope(const SmtEngine* smt); + SmtScope(const SolverEngine* smt); ~SmtScope(); /** * This returns the StatisticsRegistry attached to the currently in scope - * SmtEngine. + * SolverEngine. */ static StatisticsRegistry& currentStatisticsRegistry(); private: - /** The old SmtEngine, to be restored on destruction. */ - SmtEngine* d_oldSmtEngine; + /** The old SolverEngine, to be restored on destruction. */ + SolverEngine* d_oldSlvEngine; /** Options scope */ Options::OptionsScope d_optionsScope; };/* class SmtScope */ diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 6fb997c95..37b057048 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -26,8 +26,8 @@ namespace cvc5 { namespace smt { -SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt) - : d_smt(smt), +SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv) + : d_slv(slv), d_env(env), d_pendingPops(0), d_fullyInited(false), @@ -256,11 +256,11 @@ void SmtEngineState::internalPush() doPendingPops(); if (options::incrementalSolving()) { - // notifies the SmtEngine to process the assertions immediately - d_smt.notifyPushPre(); + // notifies the SolverEngine to process the assertions immediately + d_slv.notifyPushPre(); getUserContext()->push(); // the context push is done inside of the SAT solver - d_smt.notifyPushPost(); + d_slv.notifyPushPost(); } } @@ -285,12 +285,12 @@ void SmtEngineState::doPendingPops() // check to see if a postsolve() is pending if (d_needPostsolve) { - d_smt.notifyPostSolvePre(); + d_slv.notifyPostSolvePre(); } while (d_pendingPops > 0) { // the context pop is done inside of the SAT solver - d_smt.notifyPopPre(); + d_slv.notifyPopPre(); // pop the context getUserContext()->pop(); --d_pendingPops; @@ -298,7 +298,7 @@ void SmtEngineState::doPendingPops() } if (d_needPostsolve) { - d_smt.notifyPostSolvePost(); + d_slv.notifyPostSolvePost(); d_needPostsolve = false; } } diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index f20180672..535be2092 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -26,30 +26,32 @@ namespace cvc5 { -class SmtEngine; +class SolverEngine; class Env; namespace smt { /** - * This utility is responsible for maintaining the basic state of the SmtEngine. + * This utility is responsible for maintaining the basic state of the + * SolverEngine. * - * It has no concept of anything related to the assertions of the SmtEngine, + * It has no concept of anything related to the assertions of the SolverEngine, * or more generally it does not depend on Node. * * This class has three sets of interfaces: - * (1) notification methods that are used by SmtEngine to notify when an event - * occurs (e.g. the beginning of a check-sat call), - * (2) maintaining the SAT and user contexts to be used by the SmtEngine, - * (3) general information queries, including the mode that the SmtEngine is - * in, based on the notifications it has received. + * (1) notification methods that are used by SolverEngine to notify when an + * event occurs (e.g. the beginning of a check-sat call), (2) maintaining the + * SAT and user contexts to be used by the SolverEngine, (3) general information + * queries, including the mode that the SolverEngine is in, based on the + * notifications it has received. * - * It maintains a reference to the SmtEngine for the sake of making callbacks. + * It maintains a reference to the SolverEngine for the sake of making + * callbacks. */ class SmtEngineState { public: - SmtEngineState(Env& env, SmtEngine& smt); + SmtEngineState(Env& env, SolverEngine& smt); ~SmtEngineState() {} /** * Notify that the expected status of the next check-sat is given by the @@ -57,7 +59,7 @@ class SmtEngineState */ void notifyExpectedStatus(const std::string& status); /** - * Notify that the SmtEngine is fully initialized, which is called when + * Notify that the SolverEngine is fully initialized, which is called when * options are finalized. */ void notifyFullyInited(); @@ -89,7 +91,7 @@ class SmtEngineState * Notify that we finished an abduction query, where success is whether the * command was successful. This is managed independently of the above * calls for notifying check-sat. In other words, if a get-abduct command - * is issued to an SmtEngine, it may use a satisfiability call (if desired) + * is issued to an SolverEngine, it may use a satisfiability call (if desired) * to solve the abduction query. This method is called *in addition* to * the above calls to notifyCheckSat / notifyCheckSatResult in this case. * In particular, it is called after these two methods are completed. @@ -101,7 +103,7 @@ class SmtEngineState * Notify that we finished an interpolation query, where success is whether * the command was successful. This is managed independently of the above * calls for notifying check-sat. In other words, if a get-interpol command - * is issued to an SmtEngine, it may use a satisfiability call (if desired) + * is issued to an SolverEngine, it may use a satisfiability call (if desired) * to solve the interpolation query. This method is called *in addition* to * the above calls to notifyCheckSat / notifyCheckSatResult in this case. * In particular, it is called after these two methods are completed. @@ -119,7 +121,7 @@ class SmtEngineState */ void finishInit(); /** - * Prepare for a shutdown of the SmtEngine, which does pending pops and + * Prepare for a shutdown of the SolverEngine, which does pending pops and * pops the user context to zero. */ void shutdown(); @@ -131,17 +133,17 @@ class SmtEngineState //---------------------------- context management /** * Do all pending pops, which ensures that the context levels are up-to-date. - * This method should be called by the SmtEngine before using any of its + * This method should be called by the SolverEngine before using any of its * members that rely on the context (e.g. PropEngine or TheoryEngine). */ void doPendingPops(); /** - * Called when the user of SmtEngine issues a push. This corresponds to + * Called when the user of SolverEngine issues a push. This corresponds to * the SMT-LIB command push. */ void userPush(); /** - * Called when the user of SmtEngine issues a pop. This corresponds to + * Called when the user of SolverEngine issues a pop. This corresponds to * the SMT-LIB command pop. */ void userPop(); @@ -149,20 +151,20 @@ class SmtEngineState //---------------------------- queries /** - * Return true if the SmtEngine is fully initialized (post-construction). + * Return true if the SolverEngine is fully initialized (post-construction). * This post-construction initialization is automatically triggered by the - * use of the SmtEngine; e.g. when the first formula is asserted, a call + * use of the SolverEngine; e.g. when the first formula is asserted, a call * to simplify() is issued, a scope is pushed, etc. */ bool isFullyInited() const; /** - * Return true if the SmtEngine is fully initialized and there are no + * Return true if the SolverEngine is fully initialized and there are no * pending pops. */ bool isFullyReady() const; /** * Return true if a notifyCheckSat call has been made, e.g. a query has been - * issued to the SmtEngine. + * issued to the SolverEngine. */ bool isQueryMade() const; /** Return the user context level. */ @@ -195,9 +197,9 @@ class SmtEngineState * counter and does nothing. */ void internalPop(bool immediate = false); - /** Reference to the SmtEngine */ - SmtEngine& d_smt; - /** Reference to the env of the parent SmtEngine */ + /** Reference to the SolverEngine */ + SolverEngine& d_slv; + /** Reference to the env of the parent SolverEngine */ Env& d_env; /** The context levels of user pushes */ std::vector d_userLevels; @@ -208,9 +210,9 @@ class SmtEngineState unsigned d_pendingPops; /** - * Whether or not the SmtEngine is fully initialized (post-construction). + * Whether or not the SolverEngine is fully initialized (post-construction). * This post-construction initialization is automatically triggered by the - * use of the SmtEngine which calls the finishInit method above; e.g. when + * use of the SolverEngine which calls the finishInit method above; e.g. when * the first formula is asserted, a call to simplify() is issued, a scope is * pushed, etc. */ @@ -219,7 +221,7 @@ class SmtEngineState /** * Whether or not a notifyCheckSat call has been made, which corresponds to * when a checkEntailed() or checkSatisfiability() has already been - * made through the SmtEngine. If true, and incrementalSolving is false, + * made through the SolverEngine. If true, and incrementalSolving is false, * then attempting an additional checks for satisfiability will fail with * a ModalException during notifyCheckSat. */ @@ -228,13 +230,13 @@ class SmtEngineState /** * Internal status flag to indicate whether we have been issued a * notifyCheckSat call and have yet to process the "postsolve" methods of - * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost. + * SolverEngine via SolverEngine::notifyPostSolvePre/notifyPostSolvePost. */ bool d_needPostsolve; /** * Most recent result of last checkSatisfiability/checkEntailed in the - * SmtEngine. + * SolverEngine. */ Result d_status; diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index db914b560..31b479b5c 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -25,7 +25,7 @@ namespace smt { struct SmtEngineStatistics { - SmtEngineStatistics(const std::string& name = "smt::SmtEngine::"); + SmtEngineStatistics(const std::string& name = "smt::SolverEngine::"); /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; /** number of constant propagations found during nonclausal simp */ diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp index 2ac8bcdea..6a6e35dd9 100644 --- a/src/smt/smt_mode.cpp +++ b/src/smt/smt_mode.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Enumeration type for the mode of an SmtEngine. + * Enumeration type for the mode of an SolverEngine. */ #include "smt/smt_mode.h" diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index dbcb73e87..aff9b6366 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Enumeration type for the mode of an SmtEngine. + * Enumeration type for the mode of an SolverEngine. */ #include "cvc5_public.h" diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 48db0c45f..8064086ad 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The solver for SMT queries in an SmtEngine. + * The solver for SMT queries in an SolverEngine. */ #include "smt/smt_solver.h" diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index cdc98606c..d4e844b6c 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The solver for SMT queries in an SmtEngine. + * The solver for SMT queries in an SolverEngine. */ #include "cvc5_private.h" @@ -26,7 +26,7 @@ namespace cvc5 { -class SmtEngine; +class SolverEngine; class Env; class TheoryEngine; class ResourceManager; @@ -84,19 +84,19 @@ class SmtSolver */ void interrupt(); /** - * This is called by the destructor of SmtEngine, just before destroying the - * PropEngine, TheoryEngine, and DecisionEngine (in that order). It - * is important because there are destruction ordering issues - * between PropEngine and Theory. + * This is called by the destructor of SolverEngine, just before destroying + * the PropEngine, TheoryEngine, and DecisionEngine (in that order). It is + * important because there are destruction ordering issues between PropEngine + * and Theory. */ void shutdown(); /** * Check satisfiability (used to check satisfiability and entailment) - * in SmtEngine. This is done via adding assumptions (when necessary) to + * in SolverEngine. This is done via adding assumptions (when necessary) to * assertions as, preprocessing and pushing assertions into the prop engine * of this class, and checking for satisfiability via the prop engine. * - * @param as The object managing the assertions in SmtEngine. This class + * @param as The object managing the assertions in SolverEngine. This class * maintains a current set of (unprocessed) assertions which are pushed * into the internal members of this class (TheoryEngine and PropEngine) * during this call. @@ -128,11 +128,11 @@ class SmtSolver private: /** Reference to the environment */ Env& d_env; - /** Reference to the state of the SmtEngine */ + /** Reference to the state of the SolverEngine */ SmtEngineState& d_state; - /** Reference to the preprocessor of SmtEngine */ + /** Reference to the preprocessor of SolverEngine */ Preprocessor& d_pp; - /** Reference to the statistics of SmtEngine */ + /** Reference to the statistics of SolverEngine */ SmtEngineStatistics& d_stats; /** The theory engine */ std::unique_ptr d_theoryEngine; diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index bb1cfc9fa..1c948df60 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Accessor for the SmtEngine's StatisticsRegistry. + * Accessor for the SolverEngine's StatisticsRegistry. */ #include "smt/smt_statistics_registry.h" diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 31f55375c..66e8b522d 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Accessor for the SmtEngine's StatisticsRegistry. + * Accessor for the SolverEngine's StatisticsRegistry. */ #include "cvc5_private.h" @@ -24,7 +24,8 @@ namespace cvc5 { /** * This returns the StatisticsRegistry attached to the currently in scope - * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry(). + * SolverEngine. This is a synonym for + * smt::SmtScope::currentStatisticsRegistry(). */ StatisticsRegistry& smtStatisticsRegistry(); diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 1a03aea0a..094cc8e26 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -84,7 +84,7 @@ using namespace cvc5::theory; namespace cvc5 { -SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) +SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) : d_env(new Env(nm, optr)), d_state(new SmtEngineState(*d_env.get(), *this)), d_absValues(new AbstractValues(getNodeManager())), @@ -105,18 +105,17 @@ SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) d_pp(nullptr), d_scope(nullptr) { - // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine - // we are constructing the current SmtEngine in scope for the lifetime of - // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine - // is then in scope during its lifetime). This is mostly to ensure that - // options are always in scope, for e.g. printing expressions, which rely - // on knowing the output language. - // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally. - // These are created, used, and deleted in a modular fashion while not - // interleaving calls to the master SmtEngine. Thus the hack here does not - // break this use case. - // On the other hand, this hack breaks use cases where multiple SmtEngine - // objects are created by the user. + // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine + // we are constructing the current SolverEngine in scope for the lifetime of + // this SolverEngine, or until another SolverEngine is constructed (that + // SolverEngine is then in scope during its lifetime). This is mostly to + // ensure that options are always in scope, for e.g. printing expressions, + // which rely on knowing the output language. Notice that the SolverEngine may + // spawn new SolverEngine "subsolvers" internally. These are created, used, + // and deleted in a modular fashion while not interleaving calls to the master + // SolverEngine. Thus the hack here does not break this use case. On the other + // hand, this hack breaks use cases where multiple SolverEngine objects are + // created by the user. d_scope.reset(new SmtScope(this)); // listen to node manager events getNodeManager()->subscribeEvents(d_snmListener.get()); @@ -135,39 +134,39 @@ SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver)); } -bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } -bool SmtEngine::isQueryMade() const { return d_state->isQueryMade(); } -size_t SmtEngine::getNumUserLevels() const +bool SolverEngine::isFullyInited() const { return d_state->isFullyInited(); } +bool SolverEngine::isQueryMade() const { return d_state->isQueryMade(); } +size_t SolverEngine::getNumUserLevels() const { return d_state->getNumUserLevels(); } -SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); } -bool SmtEngine::isSmtModeSat() const +SmtMode SolverEngine::getSmtMode() const { return d_state->getMode(); } +bool SolverEngine::isSmtModeSat() const { SmtMode mode = getSmtMode(); return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN; } -Result SmtEngine::getStatusOfLastCommand() const +Result SolverEngine::getStatusOfLastCommand() const { return d_state->getStatus(); } -context::UserContext* SmtEngine::getUserContext() +context::UserContext* SolverEngine::getUserContext() { return d_env->getUserContext(); } -context::Context* SmtEngine::getContext() { return d_env->getContext(); } +context::Context* SolverEngine::getContext() { return d_env->getContext(); } -TheoryEngine* SmtEngine::getTheoryEngine() +TheoryEngine* SolverEngine::getTheoryEngine() { return d_smtSolver->getTheoryEngine(); } -prop::PropEngine* SmtEngine::getPropEngine() +prop::PropEngine* SolverEngine::getPropEngine() { return d_smtSolver->getPropEngine(); } -void SmtEngine::finishInit() +void SolverEngine::finishInit() { if (d_state->isFullyInited()) { @@ -209,7 +208,7 @@ void SmtEngine::finishInit() d_pp->setProofGenerator(pppg); } - Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; + Trace("smt-debug") << "SolverEngine::finishInit" << std::endl; d_smtSolver->finishInit(logic); // now can construct the SMT-level model object @@ -262,17 +261,17 @@ void SmtEngine::finishInit() d_pp->finishInit(); AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) - << "The PropEngine has pushed but the SmtEngine " + << "The PropEngine has pushed but the SolverEngine " "hasn't finished initializing!"; Assert(getLogicInfo().isLocked()); // store that we are finished initializing d_state->finishInit(); - Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; + Trace("smt-debug") << "SolverEngine::finishInit done" << std::endl; } -void SmtEngine::shutdown() +void SolverEngine::shutdown() { d_state->shutdown(); @@ -281,7 +280,7 @@ void SmtEngine::shutdown() d_env->shutdown(); } -SmtEngine::~SmtEngine() +SolverEngine::~SolverEngine() { SmtScope smts(this); @@ -324,13 +323,13 @@ SmtEngine::~SmtEngine() } } -void SmtEngine::setLogic(const LogicInfo& logic) +void SolverEngine::setLogic(const LogicInfo& logic) { SmtScope smts(this); if (d_state->isFullyInited()) { throw ModalException( - "Cannot set logic in SmtEngine after the engine has " + "Cannot set logic in SolverEngine after the engine has " "finished initializing."); } d_env->d_logic = logic; @@ -338,7 +337,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) setLogicInternal(); } -void SmtEngine::setLogic(const std::string& s) +void SolverEngine::setLogic(const std::string& s) { SmtScope smts(this); try @@ -351,14 +350,14 @@ void SmtEngine::setLogic(const std::string& s) } } -void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } +void SolverEngine::setLogic(const char* logic) { setLogic(string(logic)); } -const LogicInfo& SmtEngine::getLogicInfo() const +const LogicInfo& SolverEngine::getLogicInfo() const { return d_env->getLogicInfo(); } -LogicInfo SmtEngine::getUserLogicInfo() const +LogicInfo SolverEngine::getUserLogicInfo() const { // Lock the logic to make sure that this logic can be queried. We create a // copy of the user logic here to keep this method const. @@ -367,16 +366,16 @@ LogicInfo SmtEngine::getUserLogicInfo() const return res; } -void SmtEngine::setLogicInternal() +void SolverEngine::setLogicInternal() { Assert(!d_state->isFullyInited()) - << "setting logic in SmtEngine but the engine has already" + << "setting logic in SolverEngine but the engine has already" " finished initializing for this run"; d_env->d_logic.lock(); d_userLogic.lock(); } -void SmtEngine::setInfo(const std::string& key, const std::string& value) +void SolverEngine::setInfo(const std::string& key, const std::string& value) { SmtScope smts(this); @@ -423,7 +422,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) } } -bool SmtEngine::isValidGetInfoFlag(const std::string& key) const +bool SolverEngine::isValidGetInfoFlag(const std::string& key) const { if (key == "all-statistics" || key == "error-behavior" || key == "name" || key == "version" || key == "authors" || key == "status" @@ -435,7 +434,7 @@ bool SmtEngine::isValidGetInfoFlag(const std::string& key) const return false; } -std::string SmtEngine::getInfo(const std::string& key) const +std::string SolverEngine::getInfo(const std::string& key) const { SmtScope smts(this); @@ -515,7 +514,8 @@ std::string SmtEngine::getInfo(const std::string& key) const return toSExpr(res); } -void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) +void SolverEngine::debugCheckFormals(const std::vector& formals, + Node func) { for (std::vector::const_iterator i = formals.begin(); i != formals.end(); @@ -534,16 +534,16 @@ void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) } } -void SmtEngine::debugCheckFunctionBody(Node formula, - const std::vector& formals, - Node func) +void SolverEngine::debugCheckFunctionBody(Node formula, + const std::vector& formals, + Node func) { TypeNode formulaType = formula.getType(d_env->getOptions().expr.typeChecking); TypeNode funcType = func.getType(); // We distinguish here between definitions of constants and functions, // because the type checking for them is subtly different. Perhaps we - // should instead have SmtEngine::defineFunction() and - // SmtEngine::defineConstant() for better clarity, although then that + // should instead have SolverEngine::defineFunction() and + // SolverEngine::defineConstant() for better clarity, although then that // doesn't match the SMT-LIBv2 standard... if (formals.size() > 0) { @@ -574,10 +574,10 @@ void SmtEngine::debugCheckFunctionBody(Node formula, } } -void SmtEngine::defineFunction(Node func, - const std::vector& formals, - Node formula, - bool global) +void SolverEngine::defineFunction(Node func, + const std::vector& formals, + Node formula, + bool global) { SmtScope smts(this); finishInit(); @@ -611,7 +611,7 @@ void SmtEngine::defineFunction(Node func, d_asserts->addDefineFunDefinition(feq, global); } -void SmtEngine::defineFunctionsRec( +void SolverEngine::defineFunctionsRec( const std::vector& funcs, const std::vector>& formals, const std::vector& formulas, @@ -673,16 +673,16 @@ void SmtEngine::defineFunctionsRec( } // Assert the quantified formula. Notice we don't call assertFormula // directly, since we should call a private member method since we have - // already ensuring this SmtEngine is initialized above. + // already ensuring this SolverEngine is initialized above. // add define recursive definition to the assertions d_asserts->addDefineFunDefinition(lem, global); } } -void SmtEngine::defineFunctionRec(Node func, - const std::vector& formals, - Node formula, - bool global) +void SolverEngine::defineFunctionRec(Node func, + const std::vector& formals, + Node formula, + bool global) { std::vector funcs; funcs.push_back(func); @@ -693,7 +693,7 @@ void SmtEngine::defineFunctionRec(Node func, defineFunctionsRec(funcs, formals_multi, formulas, global); } -Result SmtEngine::quickCheck() +Result SolverEngine::quickCheck() { Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; @@ -702,7 +702,7 @@ Result SmtEngine::quickCheck() Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); } -TheoryModel* SmtEngine::getAvailableModel(const char* c) const +TheoryModel* SolverEngine::getAvailableModel(const char* c) const { if (!d_env->getOptions().theory.assignFunctionValues) { @@ -744,7 +744,8 @@ TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } -QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const +QuantifiersEngine* SolverEngine::getAvailableQuantifiersEngine( + const char* c) const { QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine(); if (qe == nullptr) @@ -756,16 +757,19 @@ QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const return qe; } -void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } +void SolverEngine::notifyPushPre() +{ + d_smtSolver->processAssertions(*d_asserts); +} -void SmtEngine::notifyPushPost() +void SolverEngine::notifyPushPost() { TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); Assert(getPropEngine() != nullptr); getPropEngine()->push(); } -void SmtEngine::notifyPopPre() +void SolverEngine::notifyPopPre() { TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); PropEngine* pe = getPropEngine(); @@ -773,27 +777,27 @@ void SmtEngine::notifyPopPre() pe->pop(); } -void SmtEngine::notifyPostSolvePre() +void SolverEngine::notifyPostSolvePre() { PropEngine* pe = getPropEngine(); Assert(pe != nullptr); pe->resetTrail(); } -void SmtEngine::notifyPostSolvePost() +void SolverEngine::notifyPostSolvePost() { TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); te->postsolve(); } -Result SmtEngine::checkSat() +Result SolverEngine::checkSat() { Node nullNode; return checkSat(nullNode); } -Result SmtEngine::checkSat(const Node& assumption) +Result SolverEngine::checkSat(const Node& assumption) { if (Dump.isOn("benchmark")) { @@ -807,7 +811,7 @@ Result SmtEngine::checkSat(const Node& assumption) return checkSatInternal(assump, false); } -Result SmtEngine::checkSat(const std::vector& assumptions) +Result SolverEngine::checkSat(const std::vector& assumptions) { if (Dump.isOn("benchmark")) { @@ -824,7 +828,7 @@ Result SmtEngine::checkSat(const std::vector& assumptions) return checkSatInternal(assumptions, false); } -Result SmtEngine::checkEntailed(const Node& node) +Result SolverEngine::checkEntailed(const Node& node) { if (Dump.isOn("benchmark")) { @@ -836,28 +840,29 @@ Result SmtEngine::checkEntailed(const Node& node) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const std::vector& nodes) +Result SolverEngine::checkEntailed(const std::vector& nodes) { return checkSatInternal(nodes, true).asEntailmentResult(); } -Result SmtEngine::checkSatInternal(const std::vector& assumptions, - bool isEntailmentCheck) +Result SolverEngine::checkSatInternal(const std::vector& assumptions, + bool isEntailmentCheck) { try { SmtScope smts(this); finishInit(); - Trace("smt") << "SmtEngine::" + Trace("smt") << "SolverEngine::" << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" << assumptions << ")" << endl; // check the satisfiability with the solver object Result r = d_smtSolver->checkSatisfiability( *d_asserts.get(), assumptions, isEntailmentCheck); - Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") - << "(" << assumptions << ") => " << r << endl; + Trace("smt") << "SolverEngine::" + << (isEntailmentCheck ? "query" : "checkSat") << "(" + << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. if (d_env->getOptions().smt.checkModels) @@ -920,7 +925,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, } } -std::vector SmtEngine::getUnsatAssumptions(void) +std::vector SolverEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); @@ -954,20 +959,20 @@ std::vector SmtEngine::getUnsatAssumptions(void) return res; } -Result SmtEngine::assertFormula(const Node& formula) +Result SolverEngine::assertFormula(const Node& formula) { SmtScope smts(this); finishInit(); d_state->doPendingPops(); - Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; + Trace("smt") << "SolverEngine::assertFormula(" << formula << ")" << endl; // Substitute out any abstract values in ex Node n = d_absValues->substituteAbstractValues(formula); d_asserts->assertFormula(n); return quickCheck().asEntailmentResult(); -} /* SmtEngine::assertFormula() */ +} /* SolverEngine::assertFormula() */ /* -------------------------------------------------------------------------- @@ -975,49 +980,49 @@ Result SmtEngine::assertFormula(const Node& formula) -------------------------------------------------------------------------- */ -void SmtEngine::declareSygusVar(Node var) +void SolverEngine::declareSygusVar(Node var) { SmtScope smts(this); d_sygusSolver->declareSygusVar(var); } -void SmtEngine::declareSynthFun(Node func, - TypeNode sygusType, - bool isInv, - const std::vector& vars) +void SolverEngine::declareSynthFun(Node func, + TypeNode sygusType, + bool isInv, + const std::vector& vars) { SmtScope smts(this); finishInit(); d_state->doPendingPops(); d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars); } -void SmtEngine::declareSynthFun(Node func, - bool isInv, - const std::vector& vars) +void SolverEngine::declareSynthFun(Node func, + bool isInv, + const std::vector& vars) { // use a null sygus type TypeNode sygusType; declareSynthFun(func, sygusType, isInv, vars); } -void SmtEngine::assertSygusConstraint(Node n, bool isAssume) +void SolverEngine::assertSygusConstraint(Node n, bool isAssume) { SmtScope smts(this); finishInit(); d_sygusSolver->assertSygusConstraint(n, isAssume); } -void SmtEngine::assertSygusInvConstraint(Node inv, - Node pre, - Node trans, - Node post) +void SolverEngine::assertSygusInvConstraint(Node inv, + Node pre, + Node trans, + Node post) { SmtScope smts(this); finishInit(); d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); } -Result SmtEngine::checkSynth() +Result SolverEngine::checkSynth() { SmtScope smts(this); finishInit(); @@ -1030,7 +1035,8 @@ Result SmtEngine::checkSynth() -------------------------------------------------------------------------- */ -void SmtEngine::declarePool(const Node& p, const std::vector& initValue) +void SolverEngine::declarePool(const Node& p, + const std::vector& initValue) { Assert(p.isVar() && p.getType().isSet()); finishInit(); @@ -1038,7 +1044,7 @@ void SmtEngine::declarePool(const Node& p, const std::vector& initValue) qe->declarePool(p, initValue); } -Node SmtEngine::simplify(const Node& ex) +Node SolverEngine::simplify(const Node& ex) { SmtScope smts(this); finishInit(); @@ -1048,7 +1054,7 @@ Node SmtEngine::simplify(const Node& ex) return d_pp->simplify(ex); } -Node SmtEngine::expandDefinitions(const Node& ex) +Node SolverEngine::expandDefinitions(const Node& ex) { getResourceManager()->spendResource(Resource::PreprocessStep); SmtScope smts(this); @@ -1058,7 +1064,7 @@ Node SmtEngine::expandDefinitions(const Node& ex) } // TODO(#1108): Simplify the error reporting of this method. -Node SmtEngine::getValue(const Node& ex) const +Node SolverEngine::getValue(const Node& ex) const { SmtScope smts(this); @@ -1114,7 +1120,7 @@ Node SmtEngine::getValue(const Node& ex) const return resultNode; } -std::vector SmtEngine::getValues(const std::vector& exprs) const +std::vector SolverEngine::getValues(const std::vector& exprs) const { std::vector result; for (const Node& e : exprs) @@ -1124,14 +1130,14 @@ std::vector SmtEngine::getValues(const std::vector& exprs) const return result; } -std::vector SmtEngine::getModelDomainElements(TypeNode tn) const +std::vector SolverEngine::getModelDomainElements(TypeNode tn) const { Assert(tn.isSort()); TheoryModel* m = getAvailableModel("getModelDomainElements"); return m->getDomainElements(tn); } -bool SmtEngine::isModelCoreSymbol(Node n) +bool SolverEngine::isModelCoreSymbol(Node n) { SmtScope smts(this); Assert(n.isVar()); @@ -1157,8 +1163,8 @@ bool SmtEngine::isModelCoreSymbol(Node n) return tm->isModelCoreSymbol(n); } -std::string SmtEngine::getModel(const std::vector& declaredSorts, - const std::vector& declaredFuns) +std::string SolverEngine::getModel(const std::vector& declaredSorts, + const std::vector& declaredFuns) { SmtScope smts(this); // !!! Note that all methods called here should have a version at the API @@ -1202,7 +1208,7 @@ std::string SmtEngine::getModel(const std::vector& declaredSorts, return ssm.str(); } -Result SmtEngine::blockModel() +Result SolverEngine::blockModel() { Trace("smt") << "SMT blockModel()" << endl; SmtScope smts(this); @@ -1231,7 +1237,7 @@ Result SmtEngine::blockModel() return assertFormula(eblocker); } -Result SmtEngine::blockModelValues(const std::vector& exprs) +Result SolverEngine::blockModelValues(const std::vector& exprs) { Trace("smt") << "SMT blockModelValues()" << endl; SmtScope smts(this); @@ -1253,7 +1259,7 @@ Result SmtEngine::blockModelValues(const std::vector& exprs) return assertFormula(eblocker); } -std::pair SmtEngine::getSepHeapAndNilExpr(void) +std::pair SolverEngine::getSepHeapAndNilExpr(void) { if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) { @@ -1275,7 +1281,7 @@ std::pair SmtEngine::getSepHeapAndNilExpr(void) return std::make_pair(heap, nil); } -std::vector SmtEngine::getAssertionsInternal() +std::vector SolverEngine::getAssertionsInternal() { Assert(d_state->isFullyInited()); context::CDList* al = d_asserts->getAssertionList(); @@ -1288,16 +1294,16 @@ std::vector SmtEngine::getAssertionsInternal() return res; } -std::vector SmtEngine::getExpandedAssertions() +std::vector SolverEngine::getExpandedAssertions() { std::vector easserts = getAssertions(); // must expand definitions d_pp->expandDefinitions(easserts); return easserts; } -Env& SmtEngine::getEnv() { return *d_env.get(); } +Env& SolverEngine::getEnv() { return *d_env.get(); } -void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) +void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT) { if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) { @@ -1311,7 +1317,7 @@ void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) te->declareSepHeap(locT, dataT); } -bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) +bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) { SmtScope smts(this); finishInit(); @@ -1319,11 +1325,11 @@ bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) return te->getSepHeapTypes(locT, dataT); } -Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } +Node SolverEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } -Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } +Node SolverEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } -void SmtEngine::checkProof() +void SolverEngine::checkProof() { Assert(d_env->getOptions().smt.produceProofs); // internal check the proof @@ -1341,12 +1347,12 @@ void SmtEngine::checkProof() } } -StatisticsRegistry& SmtEngine::getStatisticsRegistry() +StatisticsRegistry& SolverEngine::getStatisticsRegistry() { return d_env->getStatisticsRegistry(); } -UnsatCore SmtEngine::getUnsatCoreInternal() +UnsatCore SolverEngine::getUnsatCoreInternal() { if (!d_env->getOptions().smt.unsatCores) { @@ -1384,16 +1390,16 @@ UnsatCore SmtEngine::getUnsatCoreInternal() return UnsatCore(core); } -std::vector SmtEngine::reduceUnsatCore(const std::vector& core) +std::vector SolverEngine::reduceUnsatCore(const std::vector& core) { Assert(options::unsatCores()) << "cannot reduce unsat core if unsat cores are turned off"; - Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl; + Notice() << "SolverEngine::reduceUnsatCore(): reducing unsat core" << endl; std::unordered_set removed; for (const Node& skip : core) { - std::unique_ptr coreChecker; + std::unique_ptr coreChecker; initializeSubsolver(coreChecker, *d_env.get()); coreChecker->setLogic(getLogicInfo()); coreChecker->getOptions().smt.checkUnsatCores = false; @@ -1425,9 +1431,10 @@ std::vector SmtEngine::reduceUnsatCore(const std::vector& core) } else if (r.asSatisfiabilityResult().isUnknown()) { - Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core " - "due to " - "unknown result."; + Warning() + << "SolverEngine::reduceUnsatCore(): could not reduce unsat core " + "due to " + "unknown result."; } } @@ -1450,16 +1457,16 @@ std::vector SmtEngine::reduceUnsatCore(const std::vector& core) } } -void SmtEngine::checkUnsatCore() +void SolverEngine::checkUnsatCore() { Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; - Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; + Notice() << "SolverEngine::checkUnsatCore(): generating unsat core" << endl; UnsatCore core = getUnsatCore(); // initialize the core checker - std::unique_ptr coreChecker; + std::unique_ptr coreChecker; initializeSubsolver(coreChecker, *d_env.get()); coreChecker->getOptions().smt.checkUnsatCores = false; // disable all proof options @@ -1473,13 +1480,13 @@ void SmtEngine::checkUnsatCore() coreChecker->declareSepHeap(sepLocType, sepDataType); } - Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions" + Notice() << "SolverEngine::checkUnsatCore(): pushing core assertions" << std::endl; theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { Node assertionAfterExpansion = tls.apply(*i, false); - Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i + Notice() << "SolverEngine::checkUnsatCore(): pushing core member " << *i << ", expanded to " << assertionAfterExpansion << "\n"; coreChecker->assertFormula(assertionAfterExpansion); } @@ -1492,31 +1499,31 @@ void SmtEngine::checkUnsatCore() { throw; } - Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; + Notice() << "SolverEngine::checkUnsatCore(): result is " << r << endl; if (r.asSatisfiabilityResult().isUnknown()) { - Warning() - << "SmtEngine::checkUnsatCore(): could not check core result unknown." - << std::endl; + Warning() << "SolverEngine::checkUnsatCore(): could not check core result " + "unknown." + << std::endl; } else if (r.asSatisfiabilityResult().isSat()) { InternalError() - << "SmtEngine::checkUnsatCore(): produced core was satisfiable."; + << "SolverEngine::checkUnsatCore(): produced core was satisfiable."; } } -void SmtEngine::checkModel(bool hardFailure) +void SolverEngine::checkModel(bool hardFailure) { context::CDList* al = d_asserts->getAssertionList(); // --check-model implies --produce-assertions, which enables the // assertion list, so we should be ok. Assert(al != nullptr) - << "don't have an assertion list to check in SmtEngine::checkModel()"; + << "don't have an assertion list to check in SolverEngine::checkModel()"; TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); - Notice() << "SmtEngine::checkModel(): generating model" << endl; + Notice() << "SolverEngine::checkModel(): generating model" << endl; TheoryModel* m = getAvailableModel("check model"); Assert(m != nullptr); @@ -1533,7 +1540,7 @@ void SmtEngine::checkModel(bool hardFailure) d_checkModels->checkModel(m, al, hardFailure); } -UnsatCore SmtEngine::getUnsatCore() +UnsatCore SolverEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << std::endl; SmtScope smts(this); @@ -1545,7 +1552,7 @@ UnsatCore SmtEngine::getUnsatCore() return getUnsatCoreInternal(); } -void SmtEngine::getRelevantInstantiationTermVectors( +void SolverEngine::getRelevantInstantiationTermVectors( std::map& insts, bool getDebugInfo) { Assert(d_state->getMode() == SmtMode::UNSAT); @@ -1558,7 +1565,7 @@ void SmtEngine::getRelevantInstantiationTermVectors( d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo); } -std::string SmtEngine::getProof() +std::string SolverEngine::getProof() { Trace("smt") << "SMT getProof()\n"; SmtScope smts(this); @@ -1587,7 +1594,7 @@ std::string SmtEngine::getProof() return ss.str(); } -void SmtEngine::printInstantiations(std::ostream& out) +void SolverEngine::printInstantiations(std::ostream& out) { SmtScope smts(this); finishInit(); @@ -1680,7 +1687,7 @@ void SmtEngine::printInstantiations(std::ostream& out) } } -void SmtEngine::getInstantiationTermVectors( +void SolverEngine::getInstantiationTermVectors( std::map>>& insts) { SmtScope smts(this); @@ -1691,14 +1698,14 @@ void SmtEngine::getInstantiationTermVectors( qe->getInstantiationTermVectors(insts); } -bool SmtEngine::getSynthSolutions(std::map& solMap) +bool SolverEngine::getSynthSolutions(std::map& solMap) { SmtScope smts(this); finishInit(); return d_sygusSolver->getSynthSolutions(solMap); } -Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) +Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { SmtScope smts(this); finishInit(); @@ -1712,9 +1719,9 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) *d_asserts, q, doFull, d_isInternalSubsolver); } -bool SmtEngine::getInterpol(const Node& conj, - const TypeNode& grammarType, - Node& interpol) +bool SolverEngine::getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol) { SmtScope smts(this); finishInit(); @@ -1727,15 +1734,15 @@ bool SmtEngine::getInterpol(const Node& conj, return success; } -bool SmtEngine::getInterpol(const Node& conj, Node& interpol) +bool SolverEngine::getInterpol(const Node& conj, Node& interpol) { TypeNode grammarType; return getInterpol(conj, grammarType, interpol); } -bool SmtEngine::getAbduct(const Node& conj, - const TypeNode& grammarType, - Node& abd) +bool SolverEngine::getAbduct(const Node& conj, + const TypeNode& grammarType, + Node& abd) { SmtScope smts(this); finishInit(); @@ -1747,13 +1754,13 @@ bool SmtEngine::getAbduct(const Node& conj, return success; } -bool SmtEngine::getAbduct(const Node& conj, Node& abd) +bool SolverEngine::getAbduct(const Node& conj, Node& abd) { TypeNode grammarType; return getAbduct(conj, grammarType, abd); } -void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) +void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) { SmtScope smts(this); QuantifiersEngine* qe = @@ -1761,7 +1768,7 @@ void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) qe->getInstantiatedQuantifiedFormulas(qs); } -void SmtEngine::getInstantiationTermVectors( +void SolverEngine::getInstantiationTermVectors( Node q, std::vector>& tvecs) { SmtScope smts(this); @@ -1770,7 +1777,7 @@ void SmtEngine::getInstantiationTermVectors( qe->getInstantiationTermVectors(q, tvecs); } -std::vector SmtEngine::getAssertions() +std::vector SolverEngine::getAssertions() { SmtScope smts(this); finishInit(); @@ -1790,7 +1797,7 @@ std::vector SmtEngine::getAssertions() return getAssertionsInternal(); } -void SmtEngine::getDifficultyMap(std::map& dmap) +void SolverEngine::getDifficultyMap(std::map& dmap) { Trace("smt") << "SMT getDifficultyMap()\n"; SmtScope smts(this); @@ -1813,7 +1820,7 @@ void SmtEngine::getDifficultyMap(std::map& dmap) d_pfManager->translateDifficultyMap(dmap, *d_asserts); } -void SmtEngine::push() +void SolverEngine::push() { SmtScope smts(this); finishInit(); @@ -1827,7 +1834,7 @@ void SmtEngine::push() d_state->userPush(); } -void SmtEngine::pop() +void SolverEngine::pop() { SmtScope smts(this); finishInit(); @@ -1843,13 +1850,13 @@ void SmtEngine::pop() // clear the learned literals from the preprocessor d_pp->clearLearnedLiterals(); - Trace("userpushpop") << "SmtEngine: popped to level " + Trace("userpushpop") << "SolverEngine: popped to level " << getUserContext()->getLevel() << endl; // should we reset d_status here? // SMT-LIBv2 spec seems to imply no, but it would make sense to.. } -void SmtEngine::resetAssertions() +void SolverEngine::resetAssertions() { SmtScope smts(this); @@ -1879,7 +1886,7 @@ void SmtEngine::resetAssertions() d_smtSolver->resetAssertions(); } -void SmtEngine::interrupt() +void SolverEngine::interrupt() { if (!d_state->isFullyInited()) { @@ -1888,7 +1895,7 @@ void SmtEngine::interrupt() d_smtSolver->interrupt(); } -void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) +void SolverEngine::setResourceLimit(uint64_t units, bool cumulative) { if (cumulative) { @@ -1899,43 +1906,43 @@ void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) d_env->d_options.base.perCallResourceLimit = units; } } -void SmtEngine::setTimeLimit(uint64_t millis) +void SolverEngine::setTimeLimit(uint64_t millis) { d_env->d_options.base.perCallMillisecondLimit = millis; } -unsigned long SmtEngine::getResourceUsage() const +unsigned long SolverEngine::getResourceUsage() const { return getResourceManager()->getResourceUsage(); } -unsigned long SmtEngine::getTimeUsage() const +unsigned long SolverEngine::getTimeUsage() const { return getResourceManager()->getTimeUsage(); } -unsigned long SmtEngine::getResourceRemaining() const +unsigned long SolverEngine::getResourceRemaining() const { return getResourceManager()->getResourceRemaining(); } -NodeManager* SmtEngine::getNodeManager() const +NodeManager* SolverEngine::getNodeManager() const { return d_env->getNodeManager(); } -void SmtEngine::printStatisticsSafe(int fd) const +void SolverEngine::printStatisticsSafe(int fd) const { d_env->getStatisticsRegistry().printSafe(fd); } -void SmtEngine::printStatisticsDiff() const +void SolverEngine::printStatisticsDiff() const { d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err); d_env->getStatisticsRegistry().storeSnapshot(); } -void SmtEngine::setOption(const std::string& key, const std::string& value) +void SolverEngine::setOption(const std::string& key, const std::string& value) { Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; @@ -1973,11 +1980,11 @@ void SmtEngine::setOption(const std::string& key, const std::string& value) options::set(getOptions(), key, optionarg); } -void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } +void SolverEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } -bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } +bool SolverEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } -std::string SmtEngine::getOption(const std::string& key) const +std::string SolverEngine::getOption(const std::string& key) const { NodeManager* nm = d_env->getNodeManager(); @@ -2038,21 +2045,21 @@ std::string SmtEngine::getOption(const std::string& key) const return options::get(getOptions(), key); } -Options& SmtEngine::getOptions() { return d_env->d_options; } +Options& SolverEngine::getOptions() { return d_env->d_options; } -const Options& SmtEngine::getOptions() const { return d_env->getOptions(); } +const Options& SolverEngine::getOptions() const { return d_env->getOptions(); } -ResourceManager* SmtEngine::getResourceManager() const +ResourceManager* SolverEngine::getResourceManager() const { return d_env->getResourceManager(); } -DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); } +DumpManager* SolverEngine::getDumpManager() { return d_env->getDumpManager(); } -const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); } +const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); } -OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } +OutputManager& SolverEngine::getOutputManager() { return d_outMgr; } -theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } +theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); } } // namespace cvc5 diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 92fe30fa1..2a922914e 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * SmtEngine: the main public entry point of libcvc5. + * SolverEngine: the main public entry point of libcvc5. */ #include "cvc5_public.h" -#ifndef CVC5__SMT_ENGINE_H -#define CVC5__SMT_ENGINE_H +#ifndef CVC5__SOLVER_ENGINE_H +#define CVC5__SOLVER_ENGINE_H #include #include @@ -110,7 +110,7 @@ class QuantifiersEngine; /* -------------------------------------------------------------------------- */ -class CVC5_EXPORT SmtEngine +class CVC5_EXPORT SolverEngine { friend class ::cvc5::api::Solver; friend class ::cvc5::smt::SmtEngineState; @@ -121,18 +121,18 @@ class CVC5_EXPORT SmtEngine /* ....................................................................... */ /** - * Construct an SmtEngine with the given expression manager. + * Construct an SolverEngine with the given expression manager. * If provided, optr is a pointer to a set of options that should initialize * the values of the options object owned by this class. */ - SmtEngine(NodeManager* nm, const Options* optr = nullptr); + SolverEngine(NodeManager* nm, const Options* optr = nullptr); /** Destruct the SMT engine. */ - ~SmtEngine(); + ~SolverEngine(); //--------------------------------------------- concerning the state /** - * This is the main initialization procedure of the SmtEngine. + * This is the main initialization procedure of the SolverEngine. * * Should be called whenever the final options and logic for the problem are * set (at least, those options that are not permitted to change after @@ -143,12 +143,12 @@ class CVC5_EXPORT SmtEngine * options being set. * * This post-construction initialization is automatically triggered by the - * use of the SmtEngine; e.g. when the first formula is asserted, a call + * use of the SolverEngine; e.g. when the first formula is asserted, a call * to simplify() is issued, a scope is pushed, etc. */ void finishInit(); /** - * Return true if this SmtEngine is fully initialized (post-construction) + * Return true if this SolverEngine is fully initialized (post-construction) * by the above call. */ bool isFullyInited() const; @@ -216,9 +216,10 @@ class CVC5_EXPORT SmtEngine /** Set is internal subsolver. * - * This function is called on SmtEngine objects that are created internally. - * It is used to mark that this SmtEngine should not perform preprocessing - * passes that rephrase the input, such as --sygus-rr-synth-input or + * This function is called on SolverEngine objects that are created + * internally. It is used to mark that this SolverEngine should not + * perform preprocessing passes that rephrase the input, such as + * --sygus-rr-synth-input or * --sygus-abduct. */ void setIsInternalSubsolver(); @@ -495,8 +496,8 @@ class CVC5_EXPORT SmtEngine /** * Get the assigned value of an expr (only if immediately preceded by a SAT - * or NOT_ENTAILED query). Only permitted if the SmtEngine is set to operate - * interactively and produce-models is on. + * or NOT_ENTAILED query). Only permitted if the SolverEngine is set to + * operate interactively and produce-models is on. * * @throw ModalException, TypeCheckingException, LogicException, * UnsafeInterruptException @@ -577,7 +578,7 @@ class CVC5_EXPORT SmtEngine * elimination is LRA and LIA. * * This function returns a formula ret such that, given - * the current set of formulas A asserted to this SmtEngine : + * the current set of formulas A asserted to this SolverEngine : * * If doFull = true, then * - ( A ^ q ) and ( A ^ ret ) are equivalent @@ -698,7 +699,7 @@ class CVC5_EXPORT SmtEngine /** * Get the current set of assertions. Only permitted if the - * SmtEngine is set to operate interactively. + * SolverEngine is set to operate interactively. */ std::vector getAssertions(); @@ -725,7 +726,7 @@ class CVC5_EXPORT SmtEngine /** * Interrupt a running query. This can be called from another thread - * or from a signal handler. Throws a ModalException if the SmtEngine + * or from a signal handler. Throws a ModalException if the SolverEngine * isn't currently in a query. * * @throw ModalException @@ -733,7 +734,7 @@ class CVC5_EXPORT SmtEngine void interrupt(); /** - * Set a resource limit for SmtEngine operations. This is like a time + * Set a resource limit for SolverEngine operations. This is like a time * limit, but it's deterministic so that reproducible results can be * obtained. Currently, it's based on the number of conflicts. * However, please note that the definition may change between different @@ -746,42 +747,42 @@ class CVC5_EXPORT SmtEngine * cumulative==true replaces any cumulative resource limit currently * in effect; a call with cumulative==false replaces any per-call * resource limit currently in effect. Time limits can be set in - * addition to resource limits; the SmtEngine obeys both. That means - * that up to four independent limits can control the SmtEngine + * addition to resource limits; the SolverEngine obeys both. That means + * that up to four independent limits can control the SolverEngine * at the same time. * - * When an SmtEngine is first created, it has no time or resource + * When an SolverEngine is first created, it has no time or resource * limits. * - * Currently, these limits only cause the SmtEngine to stop what its + * Currently, these limits only cause the SolverEngine to stop what its * doing when the limit expires (or very shortly thereafter); no * heuristics are altered by the limits or the threat of them expiring. * We reserve the right to change this in the future. * * @param units the resource limit, or 0 for no limit * @param cumulative whether this resource limit is to be a cumulative - * resource limit for all remaining calls into the SmtEngine (true), or + * resource limit for all remaining calls into the SolverEngine (true), or * whether it's a per-call resource limit (false); the default is false */ void setResourceLimit(uint64_t units, bool cumulative = false); /** - * Set a per-call time limit for SmtEngine operations. + * Set a per-call time limit for SolverEngine operations. * * A per-call time limit can be set at the same time and replaces * any per-call time limit currently in effect. * Resource limits (either per-call or cumulative) can be set in - * addition to a time limit; the SmtEngine obeys all three of them. + * addition to a time limit; the SolverEngine obeys all three of them. * * Note that the per-call timer only ticks away when one of the - * SmtEngine's workhorse functions (things like assertFormula(), + * SolverEngine's workhorse functions (things like assertFormula(), * checkEntailed(), checkSat(), and simplify()) are running. * Between calls, the timer is still. * - * When an SmtEngine is first created, it has no time or resource + * When an SolverEngine is first created, it has no time or resource * limits. * - * Currently, these limits only cause the SmtEngine to stop what its + * Currently, these limits only cause the SolverEngine to stop what its * doing when the limit expires (or very shortly thereafter); no * heuristics are altered by the limits or the threat of them expiring. * We reserve the right to change this in the future. @@ -791,17 +792,17 @@ class CVC5_EXPORT SmtEngine void setTimeLimit(uint64_t millis); /** - * Get the current resource usage count for this SmtEngine. This + * Get the current resource usage count for this SolverEngine. This * function can be used to ascertain reasonable values to pass as * resource limits to setResourceLimit(). */ unsigned long getResourceUsage() const; - /** Get the current millisecond count for this SmtEngine. */ + /** Get the current millisecond count for this SolverEngine. */ unsigned long getTimeUsage() const; /** - * Get the remaining resources that can be consumed by this SmtEngine + * Get the remaining resources that can be consumed by this SolverEngine * according to the currently-set cumulative resource limit. If there * is not a cumulative resource limit set, this function throws a * ModalException. @@ -815,13 +816,13 @@ class CVC5_EXPORT SmtEngine /** * Print statistics from the statistics registry in the env object owned by - * this SmtEngine. Safe to use in a signal handler. + * this SolverEngine. Safe to use in a signal handler. */ void printStatisticsSafe(int fd) const; /** * Print the changes to the statistics from the statistics registry in the - * env object owned by this SmtEngine since this method was called the last + * env object owned by this SolverEngine since this method was called the last * time. Internally prints the diff and then stores a snapshot for the next * call. */ @@ -831,16 +832,16 @@ class CVC5_EXPORT SmtEngine Options& getOptions(); const Options& getOptions() const; - /** Get a pointer to the UserContext owned by this SmtEngine. */ + /** Get a pointer to the UserContext owned by this SolverEngine. */ context::UserContext* getUserContext(); - /** Get a pointer to the Context owned by this SmtEngine. */ + /** Get a pointer to the Context owned by this SolverEngine. */ context::Context* getContext(); - /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ + /** Get a pointer to the TheoryEngine owned by this SolverEngine. */ TheoryEngine* getTheoryEngine(); - /** Get a pointer to the PropEngine owned by this SmtEngine. */ + /** Get a pointer to the PropEngine owned by this SolverEngine. */ prop::PropEngine* getPropEngine(); /** Get the resource manager of this SMT engine */ @@ -855,7 +856,7 @@ class CVC5_EXPORT SmtEngine /** Get the output manager for this SMT engine */ OutputManager& getOutputManager(); - /** Get a pointer to the Rewriter owned by this SmtEngine. */ + /** Get a pointer to the Rewriter owned by this SolverEngine. */ theory::Rewriter* getRewriter(); /** * Get expanded assertions. @@ -874,16 +875,16 @@ class CVC5_EXPORT SmtEngine /* ....................................................................... */ // disallow copy/assignment - SmtEngine(const SmtEngine&) = delete; - SmtEngine& operator=(const SmtEngine&) = delete; + SolverEngine(const SolverEngine&) = delete; + SolverEngine& operator=(const SolverEngine&) = delete; - /** Set solver instance that owns this SmtEngine. */ + /** Set solver instance that owns this SolverEngine. */ void setSolver(api::Solver* solver) { d_solver = solver; } - /** Get a pointer to the (new) PfManager owned by this SmtEngine. */ + /** Get a pointer to the (new) PfManager owned by this SolverEngine. */ smt::PfManager* getPfManager() { return d_pfManager.get(); }; - /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ + /** Get a pointer to the StatisticsRegistry owned by this SolverEngine. */ StatisticsRegistry& getStatisticsRegistry(); /** @@ -1034,7 +1035,7 @@ class CVC5_EXPORT SmtEngine std::vector getAssertionsInternal(); /* Members -------------------------------------------------------------- */ - /** Solver instance that owns this SmtEngine instance. */ + /** Solver instance that owns this SolverEngine instance. */ api::Solver* d_solver = nullptr; /** @@ -1043,7 +1044,7 @@ class CVC5_EXPORT SmtEngine */ std::unique_ptr d_env; /** - * The state of this SmtEngine, which is responsible for maintaining which + * The state of this SolverEngine, which is responsible for maintaining which * SMT mode we are in, the contexts, the last result, etc. */ std::unique_ptr d_state; @@ -1110,12 +1111,12 @@ class CVC5_EXPORT SmtEngine */ std::unique_ptr d_pp; /** - * The global scope object. Upon creation of this SmtEngine, it becomes the - * SmtEngine in scope. It says the SmtEngine in scope until it is destructed, - * or another SmtEngine is created. + * The global scope object. Upon creation of this SolverEngine, it becomes the + * SolverEngine in scope. It says the SolverEngine in scope until it is + * destructed, or another SolverEngine is created. */ std::unique_ptr d_scope; -}; /* class SmtEngine */ +}; /* class SolverEngine */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index ff701ec48..69ea51dd1 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -335,7 +335,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) for (Node conj : conjs) { // Start new SMT engine to check solutions - std::unique_ptr solChecker; + std::unique_ptr solChecker; initializeSubsolver(solChecker, d_env); solChecker->getOptions().smt.checkSynthSol = false; solChecker->getOptions().quantifiers.sygusRecFun = false; diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index 01025e505..27922acf9 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Implementation of the unsat core manager of SmtEngine. + * Implementation of the unsat core manager of SolverEngine. */ #include "unsat_core_manager.h" diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index eb71c67ca..3b0c00e31 100644 --- a/src/smt/unsat_core_manager.h +++ b/src/smt/unsat_core_manager.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * The unsat core manager of SmtEngine. + * The unsat core manager of SolverEngine. */ #include "cvc5_private.h" @@ -30,7 +30,7 @@ namespace smt { class Assertions; /** - * This class is responsible for managing the proof output of SmtEngine, as + * This class is responsible for managing the proof output of SolverEngine, as * well as setting up the global proof checker and proof node manager. */ class UnsatCoreManager diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 00649a5af..54139c433 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -101,8 +101,8 @@ class AbstractValueTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { // An UnknownTypeException means that this node has no type. For now, // only abstract values are like this---and then, only if they are created - // by the user and don't actually correspond to one that the SmtEngine gave - // them previously. + // by the user and don't actually correspond to one that the SolverEngine + // gave them previously. throw UnknownTypeException(n); } };/* class AbstractValueTypeRule */ diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index 1b4d5cdd6..ce0d89fb7 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -366,7 +366,7 @@ class IntBlaster /** the granularity to use in the translation */ uint64_t d_granularity; - /** an SmtEngine for context */ + /** an SolverEngine for context */ context::Context* d_context; /** true iff the translator should introduce diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index da2a8b3ce..638c2aa26 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -410,7 +410,7 @@ class RewriteRule { // // NOTE: Cannot have static fields like this, or else you can't have // // two SmtEngines in the process (the second-to-be-destroyed will // // have a dangling pointer and segfault). If this statistic is needed, - // // fix the rewriter by making it an instance per-SmtEngine (instead of + // // fix the rewriter by making it an instance per-SolverEngine (instead of // // static). // static RuleStatistics* s_statistics; diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index eb8102856..56dde76a0 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -32,7 +32,7 @@ namespace datatypes { * the conversion from external to internal selectors is done in * expandDefinition. This invariant ensures that the rewritten form of a node * does not mix multiple option settings, which would lead to e.g. shared - * selectors being used in an SmtEngine instance where they are disabled. + * selectors being used in an SolverEngine instance where they are disabled. */ class DatatypesRewriter : public TheoryRewriter { diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index c6aa71ad0..c63a768dd 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -30,17 +30,17 @@ namespace cvc5 { /** * A LogicInfo instance describes a collection of theory modules and some * basic configuration about them. Conceptually, it provides a background - * context for all operations in cvc5. Typically, when cvc5's SmtEngine + * context for all operations in cvc5. Typically, when cvc5's SolverEngine * is created, it is issued a setLogic() command indicating features of the * assertions and queries to follow---for example, whether quantifiers are * used, whether integers or reals (or both) will be used, etc. * * Most places in cvc5 will only ever need to access a const reference to an - * instance of this class. Such an instance is generally set by the SmtEngine - * when setLogic() is called. However, mutating member functions are also - * provided by this class so that it can be used as a more general mechanism - * (e.g., for communicating to the SmtEngine which theories should be used, - * rather than having to provide an SMT-LIB string). + * instance of this class. Such an instance is generally set by the + * SolverEngine when setLogic() is called. However, mutating member functions + * are also provided by this class so that it can be used as a more general + * mechanism (e.g., for communicating to the SolverEngine which theories should + * be used, rather than having to provide an SMT-LIB string). */ class CVC5_EXPORT LogicInfo { diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 27deebe2f..ab1efe728 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -140,9 +140,9 @@ Node CandidateRewriteDatabase::addTerm(Node sol, Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl; // Notice we don't set produce-models. rrChecker takes the same - // options as the SmtEngine we belong to, where we ensure that + // options as the SolverEngine we belong to, where we ensure that // produce-models is set. - std::unique_ptr rrChecker; + std::unique_ptr rrChecker; initializeChecker(rrChecker, crr); Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index c0e783fc1..f81bcfd7b 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -36,7 +36,7 @@ namespace quantifiers { * of this class are to perform the "equivalence checking" and "congruence * and matching filtering" in Figure 1. The equivalence checking is done * through a combination of the sygus sampler object owned by this class - * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite + * and the calls made to copies of the SolverEngine in ::addTerm. The rewrite * rule filtering (based on congruence, matching, variable ordering) is also * managed by the sygus sampler object. */ diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 869ebe036..0d01efba7 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -137,7 +137,7 @@ Node NestedQe::doQe(Env& env, Node q) Trace("cegqi-nested-qe") << " Apply qe to " << q << std::endl; NodeManager* nm = NodeManager::currentNM(); q = nm->mkNode(kind::EXISTS, q[0], q[1].negate()); - std::unique_ptr smt_qe; + std::unique_ptr smt_qe; initializeSubsolver(smt_qe, env); Node qqe = smt_qe->getQuantifierElimination(q, true, false); if (expr::hasBoundVar(qqe)) diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 49b1d56fa..d648a7a29 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -50,7 +50,7 @@ Node ExprMiner::convertToSkolem(Node n) d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end()); } -void ExprMiner::initializeChecker(std::unique_ptr& checker, +void ExprMiner::initializeChecker(std::unique_ptr& checker, Node query) { Assert (!query.isNull()); @@ -88,7 +88,7 @@ Result ExprMiner::doCheck(Node query) return Result(Result::SAT); } } - std::unique_ptr smte; + std::unique_ptr smte; initializeChecker(smte, query); return smte->checkSat(); } diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 56eaccd7c..3933b9635 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -30,7 +30,7 @@ namespace cvc5 { class Env; -class SmtEngine; +class SolverEngine; namespace theory { namespace quantifiers { @@ -85,7 +85,7 @@ class ExprMiner : protected EnvObj * of the argument "query", which is a formula whose free variables (of * kind BOUND_VARIABLE) are a subset of d_vars. */ - void initializeChecker(std::unique_ptr& smte, Node query); + void initializeChecker(std::unique_ptr& smte, Node query); /** * Run the satisfiability check on query and return the result * (sat/unsat/unknown). diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 31d8c3c22..f7c9aa37b 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -157,7 +157,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) { Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl; // make the satisfiability query - std::unique_ptr queryChecker; + std::unique_ptr queryChecker; initializeChecker(queryChecker, qy); Result r = queryChecker->checkSat(); Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d039eb855..ad9da816b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -226,7 +226,7 @@ bool CegSingleInv::solve() siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr); } // solve the single invocation conjecture using a fresh copy of SMT engine - std::unique_ptr siSmt; + std::unique_ptr siSmt; initializeSubsolver(siSmt, d_env); // do not use shared selectors in subsolver, since this leads to solutions // with non-user symbols diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index b9066b079..936310e4e 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -595,7 +595,7 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p, return true; } -void CegisCoreConnective::getModel(SmtEngine& smt, +void CegisCoreConnective::getModel(SolverEngine& smt, std::vector& vals) const { for (const Node& v : d_vars) @@ -607,7 +607,7 @@ void CegisCoreConnective::getModel(SmtEngine& smt, } bool CegisCoreConnective::getUnsatCore( - SmtEngine& smt, + SolverEngine& smt, const std::unordered_set& queryAsserts, std::vector& uasserts) const { @@ -733,7 +733,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { addSuccess = false; // try a new core - std::unique_ptr checkSol; + std::unique_ptr checkSol; initializeSubsolver(checkSol, d_env); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector rasserts = asserts; @@ -773,7 +773,7 @@ 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; + std::unique_ptr checkSc; initializeSubsolver(checkSc, d_env); std::vector scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index ebcd871aa..3ee631dea 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -28,7 +28,7 @@ namespace cvc5 { -class SmtEngine; +class SolverEngine; namespace theory { namespace quantifiers { @@ -339,7 +339,7 @@ class CegisCoreConnective : public Cegis * Assuming smt has just been called to check-sat and returned "SAT", this * method adds the model for d_vars to mvs. */ - void getModel(SmtEngine& smt, std::vector& mvs) const; + void getModel(SolverEngine& smt, std::vector& mvs) const; /** * Assuming smt has just been called to check-sat and returned "UNSAT", this * method get the unsat core and adds it to uasserts. @@ -349,7 +349,7 @@ class CegisCoreConnective : public Cegis * If one of the formulas in queryAsserts was in the unsat core, then this * method returns true. Otherwise, this method returns false. */ - bool getUnsatCore(SmtEngine& smt, + bool getUnsatCore(SolverEngine& smt, const std::unordered_set& queryAsserts, std::vector& uasserts) const; /** diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 7e20f56c3..1a42ec337 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -260,7 +260,9 @@ void SygusInterpol::mkSygusConjecture(Node itp, Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; } -bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp) +bool SygusInterpol::findInterpol(SolverEngine* subSolver, + Node& interpol, + Node itp) { // get the synthesis solution std::map sols; @@ -270,12 +272,12 @@ bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp) if (its == sols.end()) { Trace("sygus-interpol") - << "SmtEngine::getInterpol: could not find solution!" << std::endl; + << "SolverEngine::getInterpol: could not find solution!" << std::endl; throw RecoverableModalException( "Could not find solution for get-interpol."); return false; } - Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is " + Trace("sygus-interpol") << "SolverEngine::getInterpol: solution is " << its->second << std::endl; interpol = its->second; // replace back the created variables to original symbols. @@ -323,7 +325,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name, Node itp = mkPredicate(name); mkSygusConjecture(itp, axioms, conj); - std::unique_ptr subSolver; + std::unique_ptr subSolver; initializeSubsolver(subSolver, d_env); // get the logic LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy(); @@ -337,15 +339,15 @@ bool SygusInterpol::solveInterpolation(const std::string& name, } std::vector vars_empty; subSolver->declareSynthFun(itp, grammarType, false, vars_empty); - Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " + Trace("sygus-interpol") << "SolverEngine::getInterpol: made conjecture : " << d_sygusConj << ", solving for " << d_sygusConj[0][0] << std::endl; subSolver->assertSygusConstraint(d_sygusConj); - Trace("sygus-interpol") << " SmtEngine::getInterpol check sat..." + Trace("sygus-interpol") << " SolverEngine::getInterpol check sat..." << std::endl; Result r = subSolver->checkSynth(); - Trace("sygus-interpol") << " SmtEngine::getInterpol result: " << r + Trace("sygus-interpol") << " SolverEngine::getInterpol result: " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 8f91d921b..924426365 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -27,7 +27,7 @@ namespace cvc5 { class Env; -class SmtEngine; +class SolverEngine; namespace theory { namespace quantifiers { @@ -174,7 +174,7 @@ class SygusInterpol : protected EnvObj * @param interpol the solution to the sygus conjecture. * @param itp the interpolation predicate. */ - bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp); + bool findInterpol(SolverEngine* subsolver, Node& interpol, Node itp); /** * symbols from axioms and conjecture. */ diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 0dfa0141f..2400e0e56 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -51,7 +51,7 @@ Node SygusQePreproc::preprocess(Node q) return Node::null(); } // create new smt engine to do quantifier elimination - std::unique_ptr smt_qe; + std::unique_ptr smt_qe; initializeSubsolver(smt_qe, d_env); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index b7611784d..44269eb6f 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -228,7 +228,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, Trace("sygus-engine") << "Repairing previous solution..." << std::endl; // make the satisfiability query - std::unique_ptr repcChecker; + std::unique_ptr repcChecker; // initialize the subsolver using the standard method initializeSubsolver( repcChecker, diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index e6a1ee514..7797f7fa9 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -44,7 +44,7 @@ class TermDbSygus; * forall x. P( (\x. t[x,c']), x ) [***] * is satisfiable, where notice that the above formula after beta-reduction may * be one in pure first-order logic in a decidable theory (say linear - * arithmetic). To check this, we invoke a separate instance of the SmtEngine + * arithmetic). To check this, we invoke a separate instance of the SolverEngine * within repairSolution(...) below, which if satisfiable gives us the * valuation for c'. */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 30f283dc2..4c23db9bc 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -166,7 +166,7 @@ TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId) Rewriter* Rewriter::getInstance() { - return smt::currentSmtEngine()->getRewriter(); + return smt::currentSolverEngine()->getRewriter(); } Node Rewriter::rewriteTo(theory::TheoryId theoryId, diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 697253e03..be11ff5de 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -110,10 +110,10 @@ class Rewriter { private: /** - * Get the rewriter associated with the SmtEngine in scope. + * Get the rewriter associated with the SolverEngine in scope. * * TODO(#3468): Get rid of this function (it relies on there being an - * singleton with the current SmtEngine in scope) + * singleton with the current SolverEngine in scope) */ static Rewriter* getInstance(); diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 108d59800..fb0a2dbda 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -11,7 +11,7 @@ * **************************************************************************** * * Implementation of utilities for initializing subsolvers (copies of - * SmtEngine) during solving. + * SolverEngine) during solving. */ #include "theory/smt_engine_subsolver.h" @@ -42,14 +42,14 @@ Result quickCheck(Node& query) return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); } -void initializeSubsolver(std::unique_ptr& smte, +void initializeSubsolver(std::unique_ptr& smte, const Options& opts, const LogicInfo& logicInfo, bool needsTimeout, unsigned long timeout) { NodeManager* nm = NodeManager::currentNM(); - smte.reset(new SmtEngine(nm, &opts)); + smte.reset(new SolverEngine(nm, &opts)); smte->setIsInternalSubsolver(); smte->setLogic(logicInfo); // set the options @@ -58,7 +58,7 @@ void initializeSubsolver(std::unique_ptr& smte, smte->setTimeLimit(timeout); } } -void initializeSubsolver(std::unique_ptr& smte, +void initializeSubsolver(std::unique_ptr& smte, const Env& env, bool needsTimeout, unsigned long timeout) @@ -67,7 +67,7 @@ void initializeSubsolver(std::unique_ptr& smte, smte, env.getOptions(), env.getLogicInfo(), needsTimeout, timeout); } -Result checkWithSubsolver(std::unique_ptr& smte, +Result checkWithSubsolver(std::unique_ptr& smte, Node query, const Options& opts, const LogicInfo& logicInfo, @@ -122,7 +122,7 @@ Result checkWithSubsolver(Node query, } return r; } - std::unique_ptr smte; + std::unique_ptr smte; initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout); smte->assertFormula(query); r = smte->checkSat(); diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index f46f29fc1..0e1af29db 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -10,7 +10,8 @@ * directory for licensing information. * **************************************************************************** * - * Utilities for initializing subsolvers (copies of SmtEngine) during solving. + * Utilities for initializing subsolvers (copies of SolverEngine) during + * solving. */ #include "cvc5_private.h" @@ -46,7 +47,7 @@ namespace theory { * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ -void initializeSubsolver(std::unique_ptr& smte, +void initializeSubsolver(std::unique_ptr& smte, const Options& opts, const LogicInfo& logicInfo, bool needsTimeout = false, @@ -55,7 +56,7 @@ void initializeSubsolver(std::unique_ptr& smte, /** * Version that uses the options and logicInfo in an environment. */ -void initializeSubsolver(std::unique_ptr& smte, +void initializeSubsolver(std::unique_ptr& smte, const Env& env, bool needsTimeout = false, unsigned long timeout = 0); @@ -66,7 +67,7 @@ void initializeSubsolver(std::unique_ptr& smte, * If necessary, smte is initialized to the SMT engine that checked its * satisfiability. */ -Result checkWithSubsolver(std::unique_ptr& smte, +Result checkWithSubsolver(std::unique_ptr& smte, Node query, const Options& opts, const LogicInfo& logicInfo, diff --git a/src/theory/theory.h b/src/theory/theory.h index ccda5fa77..67c460615 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -161,7 +161,7 @@ class Theory : protected EnvObj * Construct a Theory. * * The pair is assumed to uniquely identify this Theory - * w.r.t. the SmtEngine. + * w.r.t. the SolverEngine. */ Theory(TheoryId id, Env& env, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b1ab0a001..3807b926d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -205,7 +205,7 @@ class TheoryEngine : protected EnvObj */ bool isRelevant(Node lit) const; /** - * This is called at shutdown time by the SmtEngine, just before + * This is called at shutdown time by the SolverEngine, just before * destruction. It is important because there are destruction * ordering issues between PropEngine and Theory. */ diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 3dd337058..cb5d70a7b 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -162,7 +162,7 @@ class ResourceManager void beginCall(); /** - * Marks the end of a SmtEngine check call, stops the per + * Marks the end of a SolverEngine check call, stops the per * call timer. */ void endCall(); diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp index 4c0b06658..68e22f7dc 100644 --- a/test/api/reset_assertions.cpp +++ b/test/api/reset_assertions.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple test for SmtEngine::resetAssertions() + * A simple test for SolverEngine::resetAssertions() * * This program indirectly also tests some corner cases w.r.t. * context-dependent datastructures: resetAssertions() pops the contexts to diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index df78061a0..5ad7010ed 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -69,10 +69,10 @@ class TestNodeBlackNode : public TestNode Options opts; opts.base.outputLanguage = Language::LANG_AST; opts.base.outputLanguageWasSetByUser = true; - d_smt.reset(new SmtEngine(d_nodeManager, &opts)); + d_slvEngine.reset(new SolverEngine(d_nodeManager, &opts)); } - std::unique_ptr d_smt; + std::unique_ptr d_slvEngine; bool imp(bool a, bool b) const { return (!a) || (b); } bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); } diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index d4e86608d..9f93017f0 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -36,9 +36,9 @@ class TestNodeWhiteTypeNode : public TestNode void SetUp() override { TestNode::SetUp(); - d_smt.reset(new SmtEngine(d_nodeManager)); + d_slvEngine.reset(new SolverEngine(d_nodeManager)); } - std::unique_ptr d_smt; + std::unique_ptr d_slvEngine; }; TEST_F(TestNodeWhiteTypeNode, sub_types) @@ -55,7 +55,7 @@ TEST_F(TestNodeWhiteTypeNode, sub_types) Node lambda = d_nodeManager->mkVar("lambda", funtype); std::vector formals; formals.push_back(x); - d_smt->defineFunction(lambda, formals, xPos); + d_slvEngine->defineFunction(lambda, formals, xPos); ASSERT_FALSE(realType.isComparableTo(booleanType)); ASSERT_TRUE(realType.isComparableTo(integerType)); diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index ad3c1b0d1..aef461173 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -46,7 +46,7 @@ class TestPPWhiteBVGauss : public TestSmt TestSmt::SetUp(); d_preprocContext.reset(new preprocessing::PreprocessingPassContext( - d_smtEngine.get(), d_smtEngine->getEnv(), nullptr)); + d_slvEngine.get(), d_slvEngine->getEnv(), nullptr)); d_bv_gauss.reset(new BVGauss(d_preprocContext.get())); diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index 254c4b5e9..a6af29315 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -31,7 +31,7 @@ class TestPPWhiteForeignTheoryRewrite : public TestSmt TEST_F(TestPPWhiteForeignTheoryRewrite, simplify) { - ForeignTheoryRewriter ftr(d_smtEngine->getEnv()); + ForeignTheoryRewriter ftr(d_slvEngine->getEnv()); std::cout << "len(x) >= 0 is simplified to true" << std::endl; Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType()); Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x); diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index 46bea5e19..354d57a4e 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -107,7 +107,7 @@ class TestPropWhiteCnfStream : public TestSmt void SetUp() override { TestSmt::SetUp(); - d_theoryEngine = d_smtEngine->getTheoryEngine(); + d_theoryEngine = d_slvEngine->getTheoryEngine(); d_satSolver.reset(new FakeSatSolver()); d_cnfContext.reset(new context::Context()); d_cnfRegistrar.reset(new prop::NullRegistrar); @@ -115,8 +115,8 @@ class TestPropWhiteCnfStream : public TestSmt new cvc5::prop::CnfStream(d_satSolver.get(), d_cnfRegistrar.get(), d_cnfContext.get(), - &d_smtEngine->getEnv(), - d_smtEngine->getResourceManager())); + &d_slvEngine->getEnv(), + d_slvEngine->getResourceManager())); } void TearDown() override diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 5dd4137aa..9dda1e588 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Common header for unit tests that need an SmtEngine. + * Common header for unit tests that need an SolverEngine. */ #ifndef CVC5__TEST__UNIT__TEST_SMT_H @@ -47,13 +47,13 @@ class TestSmt : public TestInternal d_nodeManager = NodeManager::currentNM(); d_nodeManager->init(); d_skolemManager = d_nodeManager->getSkolemManager(); - d_smtEngine.reset(new SmtEngine(d_nodeManager)); - d_smtEngine->finishInit(); + d_slvEngine.reset(new SolverEngine(d_nodeManager)); + d_slvEngine->finishInit(); } NodeManager* d_nodeManager; SkolemManager* d_skolemManager; - std::unique_ptr d_smtEngine; + std::unique_ptr d_slvEngine; }; class TestSmtNoFinishInit : public TestInternal @@ -64,12 +64,12 @@ class TestSmtNoFinishInit : public TestInternal d_nodeManager = NodeManager::currentNM(); d_nodeManager->init(); d_skolemManager = d_nodeManager->getSkolemManager(); - d_smtEngine.reset(new SmtEngine(d_nodeManager)); + d_slvEngine.reset(new SolverEngine(d_nodeManager)); } NodeManager* d_nodeManager; SkolemManager* d_skolemManager; - std::unique_ptr d_smtEngine; + std::unique_ptr d_slvEngine; }; /* -------------------------------------------------------------------------- */ diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index c2c6cf77e..438f28c2d 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -59,7 +59,7 @@ TEST_F(TestTheoryWhiteEvaluator, simple) std::vector args = {w, x, y, z}; std::vector vals = {c1, zero, one, c1}; - Rewriter* rr = d_smtEngine->getRewriter(); + Rewriter* rr = d_slvEngine->getRewriter(); Evaluator eval(rr); Node r = eval.eval(t, args, vals); ASSERT_EQ(r, @@ -91,7 +91,7 @@ TEST_F(TestTheoryWhiteEvaluator, loop) std::vector args = {x}; std::vector vals = {c}; - Rewriter* rr = d_smtEngine->getRewriter(); + Rewriter* rr = d_slvEngine->getRewriter(); Evaluator eval(rr); Node r = eval.eval(t, args, vals); ASSERT_EQ(r, @@ -108,7 +108,7 @@ TEST_F(TestTheoryWhiteEvaluator, strIdOf) std::vector args; std::vector vals; - Rewriter* rr = d_smtEngine->getRewriter(); + Rewriter* rr = d_slvEngine->getRewriter(); Evaluator eval(rr); { @@ -143,7 +143,7 @@ TEST_F(TestTheoryWhiteEvaluator, code) std::vector args; std::vector vals; - Rewriter* rr = d_smtEngine->getRewriter(); + Rewriter* rr = d_slvEngine->getRewriter(); Evaluator eval(rr); // (str.code "A") ---> 65 diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 99454a014..32122e619 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -42,7 +42,7 @@ class TestTheoryWhiteSequencesRewriter : public TestSmt { TestSmt::SetUp(); Options opts; - d_rewriter = d_smtEngine->getRewriter(); + d_rewriter = d_slvEngine->getRewriter(); d_seqRewriter.reset(new SequencesRewriter(d_rewriter, nullptr)); } diff --git a/test/unit/theory/theory_arith_pow2_white.cpp b/test/unit/theory/theory_arith_pow2_white.cpp index db601e2ab..697073434 100644 --- a/test/unit/theory/theory_arith_pow2_white.cpp +++ b/test/unit/theory/theory_arith_pow2_white.cpp @@ -34,8 +34,8 @@ class TestTheoryWhiteArithPow2 : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("produce-models", "true"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("produce-models", "true"); + d_slvEngine->finishInit(); d_true = d_nodeManager->mkConst(true); d_one = d_nodeManager->mkConst(Rational(1)); } diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 4132be8df..a41378106 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -42,10 +42,10 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("incremental", "false"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("incremental", "false"); + d_slvEngine->finishInit(); d_arith = static_cast( - d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]); + d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]); d_realType.reset(new TypeNode(d_nodeManager->realType())); d_intType.reset(new TypeNode(d_nodeManager->integerType())); @@ -54,7 +54,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void fakeTheoryEnginePreprocess(TNode input) { Assert(input == Rewriter::rewrite(input)); - d_smtEngine->getTheoryEngine()->preRegister(input); + d_slvEngine->getTheoryEngine()->preRegister(input); } Theory::Effort d_level = Theory::EFFORT_FULL; diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index f76305db6..5fa1e10f2 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -37,8 +37,8 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("produce-models", "true"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("produce-models", "true"); + d_slvEngine->finishInit(); d_true = d_nodeManager->mkConst(true); d_one = d_nodeManager->mkConst(Rational(1)); } @@ -58,7 +58,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) // translating it to integers should yield 7. IntBlaster intBlaster( - d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, false); + d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, false); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); Node seven = d_nodeManager->mkConst(Rational(7)); ASSERT_EQ(seven, result); @@ -80,7 +80,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) // translating it to integers should yield an integer variable. IntBlaster intBlaster( - d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); Node result = intBlaster.translateNoChildren(bv, lemmas, skolems); ASSERT_TRUE(result.isVar() && result.getType().isInteger()); @@ -107,7 +107,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) // translating it to integers should yield an Int x Int -> Bool function IntBlaster intBlaster( - d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); Node result = intBlaster.translateNoChildren(f, lemmas, skolems); TypeNode resultType = result.getType(); std::vector resultDomain = resultType.getArgTypes(); @@ -131,7 +131,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) std::vector lemmas; std::map skolems; IntBlaster intBlaster( - d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); // bit-vector variables TypeNode bvType = d_nodeManager->mkBitVectorType(4); diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 5cd29878e..b03a7345c 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -31,10 +31,10 @@ class TestTheoryWhiteBVOpt : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("produce-assertions", "true"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("produce-assertions", "true"); + d_slvEngine->finishInit(); - d_optslv.reset(new OptimizationSolver(d_smtEngine.get())); + d_optslv.reset(new OptimizationSolver(d_slvEngine.get())); d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u))); d_BV16Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(16u))); } @@ -52,8 +52,8 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) Node b = d_nodeManager->mkConst(BitVector(32u, (unsigned)0xFFFFFFF1)); // (unsigned)0x3FFFFFA1 <= x <= (unsigned)0xFFFFFFF1 - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, (uint32_t)0x3FFFFFA1)); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, signed_min) @@ -73,8 +73,8 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000)); Node b = d_nodeManager->mkConst(BitVector(32u, 2147483647u)); // -2147483648 <= x <= 2147483647 - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true); @@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) // expect the minimum x = -1 ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000)); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, unsigned_max) @@ -100,8 +100,8 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) // If the gap is too large, it will have a performance issue!!! // Need binary search! // (unsigned)1 <= x <= (unsigned)2 - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false); @@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 2u)); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, signed_max) @@ -125,8 +125,8 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) Node b = d_nodeManager->mkConst(BitVector(32u, 10u)); // -2147483648 <= x <= 10 - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true); @@ -137,7 +137,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 10u)); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, min_boundary) @@ -146,11 +146,11 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) Node y = d_nodeManager->mkVar(*d_BV32Type); // x <= 18 - d_smtEngine->assertFormula(d_nodeManager->mkNode( + d_slvEngine->assertFormula(d_nodeManager->mkNode( kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x)); // this perturbs the solver to trigger some boundary bug // that existed previously - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -161,7 +161,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 18u)); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } } // namespace test diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 4cf695609..244cad7ec 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -42,20 +42,20 @@ class TestTheoryWhiteBv : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteBv, bitblaster_core) { - d_smtEngine->setLogic("QF_BV"); + d_slvEngine->setLogic("QF_BV"); - d_smtEngine->setOption("bitblast", "eager"); - d_smtEngine->setOption("bv-solver", "layered"); - d_smtEngine->setOption("incremental", "false"); + d_slvEngine->setOption("bitblast", "eager"); + d_slvEngine->setOption("bv-solver", "layered"); + d_slvEngine->setOption("incremental", "false"); // Notice that this unit test uses the theory engine of a created SMT - // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized + // engine d_slvEngine. We must ensure that d_slvEngine is properly initialized // via the following call, which constructs its underlying theory engine. - d_smtEngine->finishInit(); + d_slvEngine->finishInit(); TheoryBV* tbv = dynamic_cast( - d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]); + d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]); BVSolverLayered* bvsl = dynamic_cast(tbv->d_internal.get()); std::unique_ptr bb( - new EagerBitblaster(bvsl, d_smtEngine->getContext())); + new EagerBitblaster(bvsl, d_slvEngine->getContext())); Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)); Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)); @@ -74,10 +74,10 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) TEST_F(TestTheoryWhiteBv, mkUmulo) { - d_smtEngine->setOption("incremental", "true"); + d_slvEngine->setOption("incremental", "true"); for (uint32_t w = 1; w < 16; ++w) { - d_smtEngine->push(); + d_slvEngine->push(); Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(w)); Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(w)); @@ -88,10 +88,10 @@ 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); - Result res = d_smtEngine->checkSat(); + d_slvEngine->assertFormula(eq); + Result res = d_slvEngine->checkSat(); ASSERT_EQ(res.isSat(), Result::UNSAT); - d_smtEngine->pop(); + d_slvEngine->pop(); } } } // namespace test diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index dd3426973..8185c2354 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -49,10 +49,10 @@ class TestTheoryWhiteEngine : public TestSmt void SetUp() override { TestSmt::SetUp(); - d_context = d_smtEngine->getContext(); - d_user_context = d_smtEngine->getUserContext(); + d_context = d_slvEngine->getContext(); + d_user_context = d_slvEngine->getUserContext(); - d_theoryEngine = d_smtEngine->getTheoryEngine(); + d_theoryEngine = d_slvEngine->getTheoryEngine(); for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { delete d_theoryEngine->d_theoryOut[id]; diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 583f908e7..5f440006b 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -31,10 +31,10 @@ class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("produce-assertions", "true"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("produce-assertions", "true"); + d_slvEngine->finishInit(); - d_optslv.reset(new OptimizationSolver(d_smtEngine.get())); + d_optslv.reset(new OptimizationSolver(d_slvEngine.get())); d_intType.reset(new TypeNode(d_nodeManager->integerType())); } @@ -56,8 +56,8 @@ TEST_F(TestTheoryWhiteIntOpt, max) /* Result of asserts is: 0 < max_cost < 100 */ - d_smtEngine->assertFormula(upb); - d_smtEngine->assertFormula(lowb); + d_slvEngine->assertFormula(upb); + d_slvEngine->assertFormula(lowb); // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); @@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("99")); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, min) @@ -87,8 +87,8 @@ TEST_F(TestTheoryWhiteIntOpt, min) /* Result of asserts is: 0 < max_cost < 100 */ - d_smtEngine->assertFormula(upb); - d_smtEngine->assertFormula(lowb); + d_slvEngine->assertFormula(upb); + d_slvEngine->assertFormula(lowb); // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE); @@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("1")); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, result) @@ -118,8 +118,8 @@ TEST_F(TestTheoryWhiteIntOpt, result) /* Result of asserts is: 0 > max_cost > 100 */ - d_smtEngine->assertFormula(upb); - d_smtEngine->assertFormula(lowb); + d_slvEngine->assertFormula(upb); + d_slvEngine->assertFormula(lowb); // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); @@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteIntOpt, result) // We expect our check to have returned UNSAT ASSERT_EQ(r.isSat(), Result::UNSAT); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, open_interval) @@ -145,10 +145,10 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) 0 < cost1 < 100 110 < cost2 */ - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1)); - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1)); - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2)); /* Optimization objective: cost1 + cost2 @@ -164,7 +164,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("112")); - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); } } // namespace test diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 9a091fb3b..91a058efd 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -31,8 +31,8 @@ class TestTheoryWhiteOptMultigoal : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("produce-assertions", "true"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("produce-assertions", "true"); + d_slvEngine->finishInit(); d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u))); } @@ -42,19 +42,19 @@ class TestTheoryWhiteOptMultigoal : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteOptMultigoal, box) { - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); Node x = d_nodeManager->mkVar(*d_BV32Type); Node y = d_nodeManager->mkVar(*d_BV32Type); Node z = d_nodeManager->mkVar(*d_BV32Type); // 18 <= x - d_smtEngine->assertFormula(d_nodeManager->mkNode( + d_slvEngine->assertFormula(d_nodeManager->mkNode( kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x)); // y <= x - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - OptimizationSolver optSolver(d_smtEngine.get()); + OptimizationSolver optSolver(d_slvEngine.get()); // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -84,19 +84,19 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) TEST_F(TestTheoryWhiteOptMultigoal, lex) { - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); Node x = d_nodeManager->mkVar(*d_BV32Type); Node y = d_nodeManager->mkVar(*d_BV32Type); Node z = d_nodeManager->mkVar(*d_BV32Type); // 18 <= x - d_smtEngine->assertFormula(d_nodeManager->mkNode( + d_slvEngine->assertFormula(d_nodeManager->mkNode( kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x)); // y <= x - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - OptimizationSolver optSolver(d_smtEngine.get()); + OptimizationSolver optSolver(d_slvEngine.get()); // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -124,7 +124,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) TEST_F(TestTheoryWhiteOptMultigoal, pareto) { - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); TypeNode bv4ty(d_nodeManager->mkBitVectorType(4u)); Node a = d_nodeManager->mkVar(bv4ty); Node b = d_nodeManager->mkVar(bv4ty); @@ -169,13 +169,13 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) (and (= a 1) (= b 3)) )) */ - d_smtEngine->assertFormula(d_nodeManager->mkOr(stmts)); + d_slvEngine->assertFormula(d_nodeManager->mkOr(stmts)); /* (maximize a) (maximize b) */ - OptimizationSolver optSolver(d_smtEngine.get()); + OptimizationSolver optSolver(d_slvEngine.get()); optSolver.addObjective(a, OptimizationObjective::MAXIMIZE); optSolver.addObjective(b, OptimizationObjective::MAXIMIZE); @@ -237,25 +237,25 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) TEST_F(TestTheoryWhiteOptMultigoal, pushpop) { - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); Node x = d_nodeManager->mkVar(*d_BV32Type); Node y = d_nodeManager->mkVar(*d_BV32Type); Node z = d_nodeManager->mkVar(*d_BV32Type); // 18 <= x - d_smtEngine->assertFormula(d_nodeManager->mkNode( + d_slvEngine->assertFormula(d_nodeManager->mkNode( kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x)); // y <= x - d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); + d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - OptimizationSolver optSolver(d_smtEngine.get()); + OptimizationSolver optSolver(d_slvEngine.get()); // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // push - d_smtEngine->push(); + d_slvEngine->push(); // maximize y with `signed` comparison over bit-vectors. optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true); @@ -280,7 +280,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) BitVector(32u, (unsigned)0xFFFFFFFF)); // pop - d_smtEngine->pop(); + d_slvEngine->pop(); // now we only have one objective: (minimize x) r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); @@ -290,7 +290,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) ASSERT_EQ(results[0].getValue().getConst(), BitVector(32u, 18u)); // resetting the assertions also resets the optimization objectives - d_smtEngine->resetAssertions(); + d_slvEngine->resetAssertions(); r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index e5ba92995..cfdced65d 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -34,9 +34,9 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("cegqi-full", "true"); - d_smtEngine->setOption("produce-models", "true"); - d_smtEngine->finishInit(); + d_slvEngine->setOption("cegqi-full", "true"); + d_slvEngine->setOption("produce-models", "true"); + d_slvEngine->finishInit(); d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4)); d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4)); @@ -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); Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); - Result res = d_smtEngine->checkSat(a); + Result res = d_slvEngine->checkSat(a); ASSERT_EQ(res.d_sat, Result::UNSAT); } @@ -117,13 +117,13 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode()); Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); - Result res = d_smtEngine->checkSat(a); + Result res = d_slvEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << 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; + std::cout << "s " << d_slvEngine->getValue(d_s) << std::endl; + std::cout << "t " << d_slvEngine->getValue(d_t) << std::endl; + std::cout << "x " << d_slvEngine->getValue(d_x) << std::endl; } ASSERT_EQ(res.d_sat, Result::UNSAT); } @@ -173,16 +173,16 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node scr = d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode()); Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); - Result res = d_smtEngine->checkSat(a); + Result res = d_slvEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; if (!s1.isNull()) - std::cout << "s1 " << d_smtEngine->getValue(s1) << std::endl; + std::cout << "s1 " << d_slvEngine->getValue(s1) << std::endl; if (!s2.isNull()) - 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; + std::cout << "s2 " << d_slvEngine->getValue(s2) << std::endl; + std::cout << "t " << d_slvEngine->getValue(t) << std::endl; + std::cout << "x " << d_slvEngine->getValue(x) << std::endl; } ASSERT_TRUE(res.d_sat == Result::UNSAT); } @@ -213,12 +213,12 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node scr = d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode()); Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); - Result res = d_smtEngine->checkSat(a); + Result res = d_slvEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; - std::cout << "t " << d_smtEngine->getValue(t) << std::endl; - std::cout << "x " << d_smtEngine->getValue(x) << std::endl; + std::cout << "t " << d_slvEngine->getValue(t) << std::endl; + std::cout << "x " << d_slvEngine->getValue(x) << std::endl; } ASSERT_TRUE(res.d_sat == Result::UNSAT); } diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index eb80723fd..e50670eb3 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -37,14 +37,14 @@ class TestTheoryWhite : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->finishInit(); - delete d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; - delete d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; - d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr; - d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr; + d_slvEngine->finishInit(); + delete d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; + delete d_slvEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; + d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr; + d_slvEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr; d_dummy_theory.reset(new DummyTheory( - d_smtEngine->getEnv(), d_outputChannel, Valuation(nullptr))); + d_slvEngine->getEnv(), d_outputChannel, Valuation(nullptr))); d_outputChannel.clear(); d_atom0 = d_nodeManager->mkConst(true); d_atom1 = d_nodeManager->mkConst(false); -- 2.30.2