From 56cd2e8f584ed36fd76144a622355511a4b09935 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 30 Sep 2021 14:14:59 -0700 Subject: [PATCH] Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279) This is in preparation for renaming SmtEngine to SolverEngine. --- src/CMakeLists.txt | 4 +- src/api/cpp/cvc5.cpp | 2 +- src/main/command_executor.cpp | 2 +- src/main/driver_unified.cpp | 2 +- src/omt/bitvector_optimizer.cpp | 2 +- src/omt/integer_optimizer.cpp | 2 +- src/preprocessing/passes/sygus_inference.cpp | 2 +- .../preprocessing_pass_context.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 2 +- src/printer/tptp/tptp_printer.cpp | 2 +- src/smt/abduction_solver.cpp | 2 +- src/smt/assertions.cpp | 2 +- src/smt/expand_definitions.cpp | 2 +- src/smt/interpolation_solver.cpp | 2 +- src/smt/listeners.cpp | 2 +- src/smt/optimization_solver.cpp | 2 +- src/smt/output_manager.cpp | 2 +- src/smt/preprocessor.cpp | 2 +- src/smt/process_assertions.cpp | 2 +- src/smt/proof_post_processor.cpp | 2 +- src/smt/smt_engine_scope.cpp | 2 +- src/smt/smt_engine_state.cpp | 2 +- src/smt/smt_solver.cpp | 2 +- src/smt/{smt_engine.cpp => solver_engine.cpp} | 136 +++++++++++------- src/smt/{smt_engine.h => solver_engine.h} | 17 +-- src/theory/bv/abstraction.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 2 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 2 +- src/theory/bv/bv_subtheory_algebraic.cpp | 2 +- src/theory/bv/theory_bv_rewrite_rules.h | 2 +- .../candidate_rewrite_database.cpp | 2 +- .../ematching/candidate_generator.cpp | 2 +- src/theory/rewriter.cpp | 2 +- src/theory/smt_engine_subsolver.cpp | 2 +- src/theory/smt_engine_subsolver.h | 2 +- src/theory/theory_model.cpp | 2 +- test/api/smt2_compliance.cpp | 2 +- test/unit/node/attribute_white.cpp | 2 +- test/unit/node/node_black.cpp | 2 +- test/unit/node/type_node_white.cpp | 2 +- .../preprocessing/pass_bv_gauss_white.cpp | 2 +- .../pass_foreign_theory_rewrite_white.cpp | 2 +- test/unit/printer/smt2_printer_black.cpp | 2 +- test/unit/test_env.h | 2 +- test/unit/test_node.h | 2 +- test/unit/test_smt.h | 2 +- 46 files changed, 136 insertions(+), 107 deletions(-) rename src/smt/{smt_engine.cpp => solver_engine.cpp} (95%) rename src/smt/{smt_engine.h => solver_engine.h} (99%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 18312f7c0..fe9267bed 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -343,8 +343,8 @@ libcvc5_add_sources( smt/proof_post_processor.h smt/set_defaults.cpp smt/set_defaults.h - smt/smt_engine.cpp - smt/smt_engine.h + smt/solver_engine.cpp + smt/solver_engine.h smt/smt_engine_scope.cpp smt/smt_engine_scope.h smt/smt_engine_state.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 42690586a..a8b60a94d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -64,8 +64,8 @@ #include "proof/unsat_core.h" #include "smt/env.h" #include "smt/model.h" -#include "smt/smt_engine.h" #include "smt/smt_mode.h" +#include "smt/solver_engine.h" #include "theory/datatypes/tuple_project_op.h" #include "theory/logic_info.h" #include "theory/theory_model.h" diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 2c5741491..6a6ae4658 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -27,7 +27,7 @@ #include "main/main.h" #include "smt/command.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" namespace cvc5 { namespace main { diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index de7566b1f..ee610757b 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -36,7 +36,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "util/result.h" using namespace std; diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index 01cb6da42..72219d995 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -16,7 +16,7 @@ #include "omt/bitvector_optimizer.h" #include "options/smt_options.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "util/bitvector.h" using namespace cvc5::smt; diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index 379b0cd43..b3047b390 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -16,7 +16,7 @@ #include "omt/integer_optimizer.h" #include "options/smt_options.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" using namespace cvc5::smt; namespace cvc5::omt { diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 8abd77a27..9a35c2909 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -17,9 +17,9 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index a0894351d..9d7c80812 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -17,7 +17,7 @@ #include "expr/node_algorithm.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0c107573f..507937b2d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -41,7 +41,7 @@ #include "proof/unsat_core.h" #include "smt/command.h" #include "smt/node_command.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "smt_util/boolean_simplification.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/datatypes/sygus_datatype_utils.h" diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 6c8746706..e5f2ea55d 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -25,7 +25,7 @@ #include "proof/unsat_core.h" #include "smt/command.h" #include "smt/node_command.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" using namespace std; diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 3bdf13efb..0c6ff5a68 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -20,7 +20,7 @@ #include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index b78659d39..02ae86317 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -25,7 +25,7 @@ #include "options/smt_options.h" #include "smt/abstract_values.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/trust_substitutions.h" using namespace cvc5::theory; diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 293c46906..3ee08848d 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -22,8 +22,8 @@ #include "preprocessing/assertion_pipeline.h" #include "proof/conv_proof_generator.h" #include "smt/env.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" +#include "smt/solver_engine.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "util/resource_manager.h" diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index ff8e14e9b..923f14272 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -20,7 +20,7 @@ #include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_interpol.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index a0a3962ac..816a49a85 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -23,8 +23,8 @@ #include "smt/dump.h" #include "smt/dump_manager.h" #include "smt/node_command.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" namespace cvc5 { namespace smt { diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 67de9728c..a62a315c1 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -23,7 +23,7 @@ #include "options/smt_options.h" #include "smt/assertions.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/smt_engine_subsolver.h" using namespace cvc5::theory; diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index aa91bb184..03995fdc5 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -16,7 +16,7 @@ #include "smt/output_manager.h" #include "options/base_options.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" namespace cvc5 { diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index c36ff1bce..e63877c22 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -25,7 +25,7 @@ #include "smt/dump.h" #include "smt/env.h" #include "smt/preprocess_proof_generator.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/rewriter.h" using namespace std; diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index a9426d5bd..1fd47352e 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -33,8 +33,8 @@ #include "smt/assertions.h" #include "smt/dump.h" #include "smt/expand_definitions.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" +#include "smt/solver_engine.h" #include "theory/logic_info.h" #include "theory/theory_engine.h" diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index f5db349e1..d6a5f7652 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -19,7 +19,7 @@ #include "options/proof_options.h" #include "preprocessing/assertion_pipeline.h" #include "proof/proof_node_manager.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/arith/arith_utilities.h" #include "theory/builtin/proof_checker.h" #include "theory/bv/bitblast/bitblast_proof_generator.h" diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index ebaa73b03..2dcb4fa23 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -21,7 +21,7 @@ #include "base/check.h" #include "base/configuration_private.h" #include "base/output.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" namespace cvc5 { namespace smt { diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 2206b29cd..6fb997c95 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -21,7 +21,7 @@ #include "options/option_exception.h" #include "options/smt_options.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" namespace cvc5 { namespace smt { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e509eafcf..48db0c45f 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -21,9 +21,9 @@ #include "smt/assertions.h" #include "smt/env.h" #include "smt/preprocessor.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" +#include "smt/solver_engine.h" #include "theory/logic_info.h" #include "theory/theory_engine.h" #include "theory/theory_traits.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/solver_engine.cpp similarity index 95% rename from src/smt/smt_engine.cpp rename to src/smt/solver_engine.cpp index 99410593c..1a03aea0a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -13,7 +13,7 @@ * The main entry point into the cvc5 library's SMT interface. */ -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "base/check.h" #include "base/exception.h" @@ -233,16 +233,16 @@ void SmtEngine::finishInit() // dumping the command twice. if (Dump.isOn("benchmark")) { - LogicInfo everything; - everything.lock(); - getPrinter().toStreamCmdSetInfo( - d_env->getDumpOut(), - "notes", - "cvc5 always dumps the most general, all-supported logic (below), as " - "some internals might require the use of a logic more general than " - "the input."); - getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(), - everything.getLogicString()); + LogicInfo everything; + everything.lock(); + getPrinter().toStreamCmdSetInfo( + d_env->getDumpOut(), + "notes", + "cvc5 always dumps the most general, all-supported logic (below), as " + "some internals might require the use of a logic more general than " + "the input."); + getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(), + everything.getLogicString()); } // initialize the dump manager @@ -272,7 +272,8 @@ void SmtEngine::finishInit() Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; } -void SmtEngine::shutdown() { +void SmtEngine::shutdown() +{ d_state->shutdown(); d_smtSolver->shutdown(); @@ -284,14 +285,15 @@ SmtEngine::~SmtEngine() { SmtScope smts(this); - try { + try + { shutdown(); // global push/pop around everything, to ensure proper destruction // of context-dependent data structures d_state->cleanup(); - //destroy all passes before destroying things that they refer to + // destroy all passes before destroying things that they refer to d_pp->cleanup(); d_pfManager.reset(nullptr); @@ -315,7 +317,9 @@ SmtEngine::~SmtEngine() d_state.reset(nullptr); // destroy the environment d_env.reset(nullptr); - } catch(Exception& e) { + } + catch (Exception& e) + { Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl; } } @@ -325,8 +329,9 @@ void SmtEngine::setLogic(const LogicInfo& logic) SmtScope smts(this); if (d_state->isFullyInited()) { - throw ModalException("Cannot set logic in SmtEngine after the engine has " - "finished initializing."); + throw ModalException( + "Cannot set logic in SmtEngine after the engine has " + "finished initializing."); } d_env->d_logic = logic; d_userLogic = logic; @@ -389,7 +394,8 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) d_env->getStatisticsRegistry().registerValue( "driver::filename", value); } - else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) + else if (key == "smt-lib-version" + && !getOptions().base.inputLanguageWasSetByUser) { Language ilang = Language::LANG_SMTLIB_V2_6; @@ -436,7 +442,8 @@ std::string SmtEngine::getInfo(const std::string& key) const Trace("smt") << "SMT getInfo(" << key << ")" << endl; if (key == "all-statistics") { - return toSExpr(d_env->getStatisticsRegistry().begin(), d_env->getStatisticsRegistry().end()); + return toSExpr(d_env->getStatisticsRegistry().begin(), + d_env->getStatisticsRegistry().end()); } if (key == "error-behavior") { @@ -500,9 +507,10 @@ std::string SmtEngine::getInfo(const std::string& key) const Assert(key == "all-options"); // get the options, like all-statistics std::vector> res; - for (const auto& opt: options::getNames()) + for (const auto& opt : options::getNames()) { - res.emplace_back(std::vector{opt, options::get(getOptions(), opt)}); + res.emplace_back( + std::vector{opt, options::get(getOptions(), opt)}); } return toSExpr(res); } @@ -513,9 +521,11 @@ void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) i != formals.end(); ++i) { - if((*i).getKind() != kind::BOUND_VARIABLE) { + if ((*i).getKind() != kind::BOUND_VARIABLE) + { stringstream ss; - ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n" + ss << "All formal arguments to defined functions must be " + "BOUND_VARIABLEs, but in the\n" << "definition of function " << func << ", formal\n" << " " << *i << "\n" << "has kind " << (*i).getKind(); @@ -528,17 +538,18 @@ void SmtEngine::debugCheckFunctionBody(Node formula, const std::vector& formals, Node func) { - TypeNode formulaType = - formula.getType(d_env->getOptions().expr.typeChecking); + 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 // doesn't match the SMT-LIBv2 standard... - if(formals.size() > 0) { + if (formals.size() > 0) + { TypeNode rangeType = funcType.getRangeType(); - if(! formulaType.isComparableTo(rangeType)) { + if (!formulaType.isComparableTo(rangeType)) + { stringstream ss; ss << "Type of defined function does not match its declaration\n" << "The function : " << func << "\n" @@ -547,8 +558,11 @@ void SmtEngine::debugCheckFunctionBody(Node formula, << "Body type : " << formulaType; throw TypeCheckingExceptionPrivate(func, ss.str()); } - } else { - if(! formulaType.isComparableTo(funcType)) { + } + else + { + if (!formulaType.isComparableTo(funcType)) + { stringstream ss; ss << "Declared type of defined constant does not match its definition\n" << "The constant : " << func << "\n" @@ -573,7 +587,7 @@ void SmtEngine::defineFunction(Node func, stringstream ss; ss << language::SetLanguage( - language::SetLanguage::getLanguage(Dump.getStream())) + language::SetLanguage::getLanguage(Dump.getStream())) << func; DefineFunctionNodeCommand nc(ss.str(), func, formals, formula); @@ -679,7 +693,8 @@ void SmtEngine::defineFunctionRec(Node func, defineFunctionsRec(funcs, formals_multi, formulas, global); } -Result SmtEngine::quickCheck() { +Result SmtEngine::quickCheck() +{ Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; const std::string& filename = d_env->getOptions().driver.filename; @@ -900,7 +915,8 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, { printStatisticsDiff(); } - return Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename); + return Result( + Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename); } } @@ -951,7 +967,7 @@ Result SmtEngine::assertFormula(const Node& formula) d_asserts->assertFormula(n); return quickCheck().asEntailmentResult(); -}/* SmtEngine::assertFormula() */ +} /* SmtEngine::assertFormula() */ /* -------------------------------------------------------------------------- @@ -1063,8 +1079,9 @@ Node SmtEngine::getValue(const Node& ex) const // two are different, but they need to be unified. This ugly hack here // is to fix bug 554 until we can revamp boolean-terms and models [MGD] - //AJR : necessary? - if(!n.getType().isFunction()) { + // AJR : necessary? + if (!n.getType().isFunction()) + { n = Rewriter::rewrite(n); } @@ -1088,8 +1105,7 @@ Node SmtEngine::getValue(const Node& ex) const Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); - if (d_env->getOptions().smt.abstractValues - && resultNode.getType().isArray()) + if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray()) { resultNode = d_absValues->mkAbstractValue(resultNode); Trace("smt") << "--- abstract value >> " << resultNode << endl; @@ -1200,8 +1216,7 @@ Result SmtEngine::blockModel() TheoryModel* m = getAvailableModel("block model"); - if (d_env->getOptions().smt.blockModelsMode - == options::BlockModelsMode::NONE) + if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) { std::stringstream ss; ss << "Cannot block model when block-models is set to none."; @@ -1435,7 +1450,8 @@ std::vector SmtEngine::reduceUnsatCore(const std::vector& core) } } -void SmtEngine::checkUnsatCore() { +void SmtEngine::checkUnsatCore() +{ Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; @@ -1460,20 +1476,25 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions" << std::endl; theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); - for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { + for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i) + { Node assertionAfterExpansion = tls.apply(*i, false); Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << ", expanded to " << assertionAfterExpansion << "\n"; coreChecker->assertFormula(assertionAfterExpansion); } Result r; - try { + try + { r = coreChecker->checkSat(); - } catch(...) { + } + catch (...) + { throw; } Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; - if(r.asSatisfiabilityResult().isUnknown()) { + if (r.asSatisfiabilityResult().isUnknown()) + { Warning() << "SmtEngine::checkUnsatCore(): could not check core result unknown." << std::endl; @@ -1485,7 +1506,8 @@ void SmtEngine::checkUnsatCore() { } } -void SmtEngine::checkModel(bool hardFailure) { +void SmtEngine::checkModel(bool hardFailure) +{ context::CDList* al = d_asserts->getAssertionList(); // --check-model implies --produce-assertions, which enables the // assertion list, so we should be ok. @@ -1511,7 +1533,8 @@ void SmtEngine::checkModel(bool hardFailure) { d_checkModels->checkModel(m, al, hardFailure); } -UnsatCore SmtEngine::getUnsatCore() { +UnsatCore SmtEngine::getUnsatCore() +{ Trace("smt") << "SMT getUnsatCore()" << std::endl; SmtScope smts(this); finishInit(); @@ -1564,7 +1587,8 @@ std::string SmtEngine::getProof() return ss.str(); } -void SmtEngine::printInstantiations( std::ostream& out ) { +void SmtEngine::printInstantiations(std::ostream& out) +{ SmtScope smts(this); finishInit(); QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); @@ -1633,7 +1657,8 @@ void SmtEngine::printInstantiations( std::ostream& out ) { continue; } // must have a name - if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM) + if (d_env->getOptions().printer.printInstMode + == options::PrintInstMode::NUM) { out << "(num-instantiations " << name << " " << i.second.d_inst.size() << ")" << std::endl; @@ -1758,7 +1783,8 @@ std::vector SmtEngine::getAssertions() if (!d_env->getOptions().smt.produceAssertions) { const char* msg = - "Cannot query the current assertion list when not in produce-assertions mode."; + "Cannot query the current assertion list when not in " + "produce-assertions mode."; throw ModalException(msg); } return getAssertionsInternal(); @@ -1794,13 +1820,15 @@ void SmtEngine::push() d_state->doPendingPops(); Trace("smt") << "SMT push()" << endl; d_smtSolver->processAssertions(*d_asserts); - if(Dump.isOn("benchmark")) { + if (Dump.isOn("benchmark")) + { getPrinter().toStreamCmdPush(d_env->getDumpOut()); } d_state->userPush(); } -void SmtEngine::pop() { +void SmtEngine::pop() +{ SmtScope smts(this); finishInit(); Trace("smt") << "SMT pop()" << endl; @@ -1835,7 +1863,6 @@ void SmtEngine::resetAssertions() return; } - Trace("smt") << "SMT resetAssertions()" << endl; if (Dump.isOn("benchmark")) { @@ -1958,7 +1985,8 @@ std::string SmtEngine::getOption(const std::string& key) const if (key.find("command-verbosity:") == 0) { - auto it = d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); + auto it = + d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); if (it != d_commandVerbosity.end()) { return std::to_string(it->second); @@ -1980,7 +2008,7 @@ std::string SmtEngine::getOption(const std::string& key) const { vector result; Node defaultVerbosity; - for (const auto& verb: d_commandVerbosity) + for (const auto& verb : d_commandVerbosity) { // treat the command name as a variable name as opposed to a string // constant to avoid printing double quotes around the name diff --git a/src/smt/smt_engine.h b/src/smt/solver_engine.h similarity index 99% rename from src/smt/smt_engine.h rename to src/smt/solver_engine.h index a06b2fd61..92fe30fa1 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/solver_engine.h @@ -33,7 +33,8 @@ namespace cvc5 { -template class NodeTemplate; +template +class NodeTemplate; typedef NodeTemplate Node; typedef NodeTemplate TNode; class TypeNode; @@ -56,9 +57,9 @@ class Solver; /* -------------------------------------------------------------------------- */ namespace context { - class Context; - class UserContext; - } // namespace context +class Context; +class UserContext; +} // namespace context /* -------------------------------------------------------------------------- */ @@ -69,8 +70,8 @@ class PreprocessingPassContext; /* -------------------------------------------------------------------------- */ namespace prop { - class PropEngine; - } // namespace prop +class PropEngine; +} // namespace prop /* -------------------------------------------------------------------------- */ @@ -121,8 +122,8 @@ class CVC5_EXPORT SmtEngine /** * Construct an SmtEngine 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. + * 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); /** Destruct the SMT engine. */ diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 37758ad4a..1c4633b5a 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -19,9 +19,9 @@ #include "options/bv_options.h" #include "printer/printer.h" #include "smt/dump.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index dd3a3e9ce..9e3efa3bf 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -21,8 +21,8 @@ #include "options/smt_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" -#include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 3eb2eebe7..a61c7a9ab 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -20,8 +20,8 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" -#include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "theory/bv/abstraction.h" #include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv.h" diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index d6e60d1f4..27afdbbaa 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -20,9 +20,9 @@ #include "options/bv_options.h" #include "printer/printer.h" #include "smt/dump.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "smt_util/boolean_simplification.h" #include "theory/bv/bv_quick_check.h" #include "theory/bv/bv_solver_layered.h" diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 7553bcbb6..da2a8b3ce 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -25,8 +25,8 @@ #include "context/context.h" #include "printer/printer.h" #include "smt/dump.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" #include "util/statistics_stats.h" diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 475df0b43..27deebe2f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -17,9 +17,9 @@ #include "options/base_options.h" #include "printer/printer.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 0fd5c21d5..f891b0e99 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -18,8 +18,8 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_state.h" diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 4e571a66b..30f283dc2 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,9 +17,9 @@ #include "options/theory_options.h" #include "proof/conv_proof_generator.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine.h" #include "theory/builtin/proof_checker.h" #include "theory/evaluator.h" #include "theory/quantifiers/extended_rewrite.h" diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index dda065d7b..108d59800 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -17,8 +17,8 @@ #include "theory/smt_engine_subsolver.h" #include "smt/env.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 028c35cd8..f46f29fc1 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -22,7 +22,7 @@ #include #include "expr/node.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" namespace cvc5 { namespace theory { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 528e093aa..8c1a17fe1 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -20,7 +20,7 @@ #include "options/theory_options.h" #include "options/uf_options.h" #include "smt/env.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "theory/trust_substitutions.h" #include "util/rational.h" diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 83c3833d1..2a39b1d0b 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -22,7 +22,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" using namespace cvc5; using namespace cvc5::parser; diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index 4b0f1892f..fef1184a2 100644 --- a/test/unit/node/attribute_white.cpp +++ b/test/unit/node/attribute_white.cpp @@ -22,8 +22,8 @@ #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" #include "expr/node_value.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "test_node.h" #include "theory/theory.h" #include "theory/theory_engine.h" diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index d083c9fb0..df78061a0 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -30,7 +30,7 @@ #include "options/base_options.h" #include "options/language.h" #include "options/options_public.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "test_node.h" #include "theory/rewriter.h" #include "util/bitvector.h" diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index d3d05040f..d4e86608d 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -19,7 +19,7 @@ #include "expr/node_manager.h" #include "expr/type_node.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "test_node.h" #include "util/rational.h" diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 329c565ea..ad3c1b0d1 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -22,8 +22,8 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/preprocessing_pass_context.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "test_smt.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index c10d8f363..254c4b5e9 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -15,7 +15,7 @@ #include "expr/node_manager.h" #include "preprocessing/passes/foreign_theory_rewrite.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "test_smt.h" #include "util/rational.h" diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index 3d9c3ca2c..66304ec01 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -19,7 +19,7 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "options/language.h" -#include "smt/smt_engine.h" +#include "smt/solver_engine.h" #include "test_smt.h" #include "util/regexp.h" #include "util/string.h" diff --git a/test/unit/test_env.h b/test/unit/test_env.h index b3f60a98a..4b4fb72e9 100644 --- a/test/unit/test_env.h +++ b/test/unit/test_env.h @@ -20,8 +20,8 @@ #include "expr/skolem_manager.h" #include "options/options.h" #include "smt/env.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "test.h" namespace cvc5 { diff --git a/test/unit/test_node.h b/test/unit/test_node.h index a6a85b1b1..08fa8eb30 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -18,8 +18,8 @@ #include "expr/node_manager.h" #include "expr/skolem_manager.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "test.h" namespace cvc5 { diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 92701d60c..5dd4137aa 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -21,8 +21,8 @@ #include "expr/node_manager.h" #include "expr/skolem_manager.h" #include "proof/proof_checker.h" -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/solver_engine.h" #include "test.h" #include "theory/output_channel.h" #include "theory/rewriter.h" -- 2.30.2