From: Aina Niemetz Date: Thu, 30 Sep 2021 21:14:59 +0000 (-0700) Subject: Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279) X-Git-Tag: cvc5-1.0.0~1144 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56cd2e8f584ed36fd76144a622355511a4b09935;p=cvc5.git Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279) This is in preparation for renaming SmtEngine to SolverEngine. --- 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.cpp b/src/smt/smt_engine.cpp deleted file mode 100644 index 99410593c..000000000 --- a/src/smt/smt_engine.cpp +++ /dev/null @@ -1,2030 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The main entry point into the cvc5 library's SMT interface. - */ - -#include "smt/smt_engine.h" - -#include "base/check.h" -#include "base/exception.h" -#include "base/modal_exception.h" -#include "base/output.h" -#include "decision/decision_engine.h" -#include "expr/bound_var_manager.h" -#include "expr/node.h" -#include "options/base_options.h" -#include "options/expr_options.h" -#include "options/language.h" -#include "options/main_options.h" -#include "options/option_exception.h" -#include "options/options_public.h" -#include "options/parser_options.h" -#include "options/printer_options.h" -#include "options/proof_options.h" -#include "options/smt_options.h" -#include "options/theory_options.h" -#include "printer/printer.h" -#include "proof/unsat_core.h" -#include "prop/prop_engine.h" -#include "smt/abduction_solver.h" -#include "smt/abstract_values.h" -#include "smt/assertions.h" -#include "smt/check_models.h" -#include "smt/dump.h" -#include "smt/dump_manager.h" -#include "smt/env.h" -#include "smt/interpolation_solver.h" -#include "smt/listeners.h" -#include "smt/logic_exception.h" -#include "smt/model_blocker.h" -#include "smt/model_core_builder.h" -#include "smt/node_command.h" -#include "smt/preprocessor.h" -#include "smt/proof_manager.h" -#include "smt/quant_elim_solver.h" -#include "smt/set_defaults.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_engine_state.h" -#include "smt/smt_engine_stats.h" -#include "smt/smt_solver.h" -#include "smt/sygus_solver.h" -#include "smt/unsat_core_manager.h" -#include "theory/quantifiers/instantiation_list.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers_engine.h" -#include "theory/rewriter.h" -#include "theory/smt_engine_subsolver.h" -#include "theory/theory_engine.h" -#include "util/random.h" -#include "util/rational.h" -#include "util/resource_manager.h" -#include "util/sexpr.h" -#include "util/statistics_registry.h" - -// required for hacks related to old proofs for unsat cores -#include "base/configuration.h" -#include "base/configuration_private.h" - -using namespace std; -using namespace cvc5::smt; -using namespace cvc5::preprocessing; -using namespace cvc5::prop; -using namespace cvc5::context; -using namespace cvc5::theory; - -namespace cvc5 { - -SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) - : d_env(new Env(nm, optr)), - d_state(new SmtEngineState(*d_env.get(), *this)), - d_absValues(new AbstractValues(getNodeManager())), - d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), - d_routListener(new ResourceOutListener(*this)), - d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), - d_smtSolver(nullptr), - d_checkModels(nullptr), - d_pfManager(nullptr), - d_ucManager(nullptr), - d_sygusSolver(nullptr), - d_abductSolver(nullptr), - d_interpolSolver(nullptr), - d_quantElimSolver(nullptr), - d_isInternalSubsolver(false), - d_stats(nullptr), - d_outMgr(this), - 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. - d_scope.reset(new SmtScope(this)); - // listen to node manager events - getNodeManager()->subscribeEvents(d_snmListener.get()); - // listen to resource out - getResourceManager()->registerListener(d_routListener.get()); - // make statistics - d_stats.reset(new SmtEngineStatistics()); - // reset the preprocessor - d_pp.reset( - new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); - // make the SMT solver - d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats)); - // make the SyGuS solver - d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp)); - // make the quantifier elimination solver - 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 -{ - return d_state->getNumUserLevels(); -} -SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); } -bool SmtEngine::isSmtModeSat() const -{ - SmtMode mode = getSmtMode(); - return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN; -} -Result SmtEngine::getStatusOfLastCommand() const -{ - return d_state->getStatus(); -} -context::UserContext* SmtEngine::getUserContext() -{ - return d_env->getUserContext(); -} -context::Context* SmtEngine::getContext() { return d_env->getContext(); } - -TheoryEngine* SmtEngine::getTheoryEngine() -{ - return d_smtSolver->getTheoryEngine(); -} - -prop::PropEngine* SmtEngine::getPropEngine() -{ - return d_smtSolver->getPropEngine(); -} - -void SmtEngine::finishInit() -{ - if (d_state->isFullyInited()) - { - // already initialized, return - return; - } - - // Notice that finishInitInternal is called when options are finalized. If we - // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52 - // of SMT-LIB 2.6 standard. - - // set the logic - const LogicInfo& logic = getLogicInfo(); - if (!logic.isLocked()) - { - setLogicInternal(); - } - - // set the random seed - Random::getRandom().setSeed(d_env->getOptions().driver.seed); - - // Call finish init on the set defaults module. This inializes the logic - // and the best default options based on our heuristics. - SetDefaults sdefaults(d_isInternalSubsolver); - sdefaults.setDefaults(d_env->d_logic, getOptions()); - - if (d_env->getOptions().smt.produceProofs) - { - // ensure bound variable uses canonical bound variables - getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); - // make the proof manager - d_pfManager.reset(new PfManager(*d_env.get())); - PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); - // start the unsat core manager - d_ucManager.reset(new UnsatCoreManager()); - // enable it in the assertions pipeline - d_asserts->setProofGenerator(pppg); - // enabled proofs in the preprocessor - d_pp->setProofGenerator(pppg); - } - - Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; - d_smtSolver->finishInit(logic); - - // now can construct the SMT-level model object - TheoryEngine* te = d_smtSolver->getTheoryEngine(); - Assert(te != nullptr); - TheoryModel* tm = te->getModel(); - if (tm != nullptr) - { - // make the check models utility - d_checkModels.reset(new CheckModels(*d_env.get())); - } - - // global push/pop around everything, to ensure proper destruction - // of context-dependent data structures - d_state->setup(); - - Trace("smt-debug") << "Set up assertions..." << std::endl; - d_asserts->finishInit(); - - // dump out a set-logic command only when raw-benchmark is disabled to avoid - // 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()); - } - - // initialize the dump manager - getDumpManager()->finishInit(); - - // subsolvers - if (d_env->getOptions().smt.produceAbducts) - { - d_abductSolver.reset(new AbductionSolver(*d_env.get())); - } - if (d_env->getOptions().smt.produceInterpols - != options::ProduceInterpols::NONE) - { - d_interpolSolver.reset(new InterpolationSolver(*d_env.get())); - } - - d_pp->finishInit(); - - AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) - << "The PropEngine has pushed but the SmtEngine " - "hasn't finished initializing!"; - - Assert(getLogicInfo().isLocked()); - - // store that we are finished initializing - d_state->finishInit(); - Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; -} - -void SmtEngine::shutdown() { - d_state->shutdown(); - - d_smtSolver->shutdown(); - - d_env->shutdown(); -} - -SmtEngine::~SmtEngine() -{ - SmtScope smts(this); - - 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 - d_pp->cleanup(); - - d_pfManager.reset(nullptr); - d_ucManager.reset(nullptr); - - d_absValues.reset(nullptr); - d_asserts.reset(nullptr); - - d_abductSolver.reset(nullptr); - d_interpolSolver.reset(nullptr); - d_quantElimSolver.reset(nullptr); - d_sygusSolver.reset(nullptr); - d_smtSolver.reset(nullptr); - - d_stats.reset(nullptr); - getNodeManager()->unsubscribeEvents(d_snmListener.get()); - d_snmListener.reset(nullptr); - d_routListener.reset(nullptr); - d_pp.reset(nullptr); - // destroy the state - d_state.reset(nullptr); - // destroy the environment - d_env.reset(nullptr); - } catch(Exception& e) { - Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl; - } -} - -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."); - } - d_env->d_logic = logic; - d_userLogic = logic; - setLogicInternal(); -} - -void SmtEngine::setLogic(const std::string& s) -{ - SmtScope smts(this); - try - { - setLogic(LogicInfo(s)); - } - catch (IllegalArgumentException& e) - { - throw LogicException(e.what()); - } -} - -void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } - -const LogicInfo& SmtEngine::getLogicInfo() const -{ - return d_env->getLogicInfo(); -} - -LogicInfo SmtEngine::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. - LogicInfo res = d_userLogic; - res.lock(); - return res; -} - -void SmtEngine::setLogicInternal() -{ - Assert(!d_state->isFullyInited()) - << "setting logic in SmtEngine 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) -{ - SmtScope smts(this); - - Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; - - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value); - } - - if (key == "filename") - { - d_env->d_options.driver.filename = value; - d_env->d_originalOptions->driver.filename = value; - d_env->getStatisticsRegistry().registerValue( - "driver::filename", value); - } - else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) - { - Language ilang = Language::LANG_SMTLIB_V2_6; - - if (value != "2" && value != "2.6") - { - Warning() << "SMT-LIB version " << value - << " unsupported, defaulting to language (and semantics of) " - "SMT-LIB 2.6\n"; - } - getOptions().base.inputLanguage = ilang; - // also update the output language - if (!getOptions().base.outputLanguageWasSetByUser) - { - Language olang = ilang; - if (d_env->getOptions().base.outputLanguage != olang) - { - getOptions().base.outputLanguage = olang; - *d_env->getOptions().base.out << language::SetLanguage(olang); - } - } - } - else if (key == "status") - { - d_state->notifyExpectedStatus(value); - } -} - -bool SmtEngine::isValidGetInfoFlag(const std::string& key) const -{ - if (key == "all-statistics" || key == "error-behavior" || key == "name" - || key == "version" || key == "authors" || key == "status" - || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options" || key == "time") - { - return true; - } - return false; -} - -std::string SmtEngine::getInfo(const std::string& key) const -{ - SmtScope smts(this); - - Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if (key == "all-statistics") - { - return toSExpr(d_env->getStatisticsRegistry().begin(), d_env->getStatisticsRegistry().end()); - } - if (key == "error-behavior") - { - return "immediate-exit"; - } - if (key == "filename") - { - return d_env->getOptions().driver.filename; - } - if (key == "name") - { - return toSExpr(Configuration::getName()); - } - if (key == "version") - { - return toSExpr(Configuration::getVersionString()); - } - if (key == "authors") - { - return toSExpr(Configuration::about()); - } - if (key == "status") - { - // sat | unsat | unknown - Result status = d_state->getStatus(); - switch (status.asSatisfiabilityResult().isSat()) - { - case Result::SAT: return "sat"; - case Result::UNSAT: return "unsat"; - default: return "unknown"; - } - } - if (key == "time") - { - return toSExpr(std::clock()); - } - if (key == "reason-unknown") - { - Result status = d_state->getStatus(); - if (!status.isNull() && status.isUnknown()) - { - std::stringstream ss; - ss << status.whyUnknown(); - std::string s = ss.str(); - transform(s.begin(), s.end(), s.begin(), ::tolower); - return s; - } - else - { - throw RecoverableModalException( - "Can't get-info :reason-unknown when the " - "last result wasn't unknown!"); - } - } - if (key == "assertion-stack-levels") - { - size_t ulevel = d_state->getNumUserLevels(); - AlwaysAssert(ulevel <= std::numeric_limits::max()); - return toSExpr(ulevel); - } - Assert(key == "all-options"); - // get the options, like all-statistics - std::vector> res; - for (const auto& opt: options::getNames()) - { - res.emplace_back(std::vector{opt, options::get(getOptions(), opt)}); - } - return toSExpr(res); -} - -void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) -{ - for (std::vector::const_iterator i = formals.begin(); - i != formals.end(); - ++i) - { - if((*i).getKind() != kind::BOUND_VARIABLE) { - stringstream ss; - 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(); - throw TypeCheckingExceptionPrivate(func, ss.str()); - } - } -} - -void SmtEngine::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 - // doesn't match the SMT-LIBv2 standard... - if(formals.size() > 0) { - TypeNode rangeType = funcType.getRangeType(); - if(! formulaType.isComparableTo(rangeType)) { - stringstream ss; - ss << "Type of defined function does not match its declaration\n" - << "The function : " << func << "\n" - << "Declared type : " << rangeType << "\n" - << "The body : " << formula << "\n" - << "Body type : " << formulaType; - throw TypeCheckingExceptionPrivate(func, ss.str()); - } - } else { - if(! formulaType.isComparableTo(funcType)) { - stringstream ss; - ss << "Declared type of defined constant does not match its definition\n" - << "The constant : " << func << "\n" - << "Declared type : " << funcType << "\n" - << "The definition : " << formula << "\n" - << "Definition type: " << formulaType; - throw TypeCheckingExceptionPrivate(func, ss.str()); - } - } -} - -void SmtEngine::defineFunction(Node func, - const std::vector& formals, - Node formula, - bool global) -{ - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - Trace("smt") << "SMT defineFunction(" << func << ")" << endl; - debugCheckFormals(formals, func); - - stringstream ss; - ss << language::SetLanguage( - language::SetLanguage::getLanguage(Dump.getStream())) - << func; - - DefineFunctionNodeCommand nc(ss.str(), func, formals, formula); - getDumpManager()->addToDump(nc, "declarations"); - - // type check body - debugCheckFunctionBody(formula, formals, func); - - // Substitute out any abstract values in formula - Node def = d_absValues->substituteAbstractValues(formula); - if (!formals.empty()) - { - NodeManager* nm = NodeManager::currentNM(); - def = nm->mkNode( - kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def); - } - // A define-fun is treated as a (higher-order) assertion. It is provided - // to the assertions object. It will be added as a top-level substitution - // within this class, possibly multiple times if global is true. - Node feq = func.eqNode(def); - d_asserts->addDefineFunDefinition(feq, global); -} - -void SmtEngine::defineFunctionsRec( - const std::vector& funcs, - const std::vector>& formals, - const std::vector& formulas, - bool global) -{ - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - Trace("smt") << "SMT defineFunctionsRec(...)" << endl; - - if (funcs.size() != formals.size() && funcs.size() != formulas.size()) - { - stringstream ss; - ss << "Number of functions, formals, and function bodies passed to " - "defineFunctionsRec do not match:" - << "\n" - << " #functions : " << funcs.size() << "\n" - << " #arg lists : " << formals.size() << "\n" - << " #function bodies : " << formulas.size() << "\n"; - throw ModalException(ss.str()); - } - for (unsigned i = 0, size = funcs.size(); i < size; i++) - { - // check formal argument list - debugCheckFormals(formals[i], funcs[i]); - // type check body - debugCheckFunctionBody(formulas[i], formals[i], funcs[i]); - } - - NodeManager* nm = getNodeManager(); - for (unsigned i = 0, size = funcs.size(); i < size; i++) - { - // we assert a quantified formula - Node func_app; - // make the function application - if (formals[i].empty()) - { - // it has no arguments - func_app = funcs[i]; - } - else - { - std::vector children; - children.push_back(funcs[i]); - children.insert(children.end(), formals[i].begin(), formals[i].end()); - func_app = nm->mkNode(kind::APPLY_UF, children); - } - Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]); - if (!formals[i].empty()) - { - // set the attribute to denote this is a function definition - Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app); - aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr); - FunDefAttribute fda; - func_app.setAttribute(fda, true); - // make the quantified formula - Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]); - lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr); - } - // 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. - // 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) -{ - std::vector funcs; - funcs.push_back(func); - std::vector> formals_multi; - formals_multi.push_back(formals); - std::vector formulas; - formulas.push_back(formula); - defineFunctionsRec(funcs, formals_multi, formulas, global); -} - -Result SmtEngine::quickCheck() { - Assert(d_state->isFullyInited()); - Trace("smt") << "SMT quickCheck()" << endl; - const std::string& filename = d_env->getOptions().driver.filename; - return Result( - Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); -} - -TheoryModel* SmtEngine::getAvailableModel(const char* c) const -{ - if (!d_env->getOptions().theory.assignFunctionValues) - { - std::stringstream ss; - ss << "Cannot " << c << " when --assign-function-values is false."; - throw RecoverableModalException(ss.str().c_str()); - } - - if (d_state->getMode() != SmtMode::SAT - && d_state->getMode() != SmtMode::SAT_UNKNOWN) - { - std::stringstream ss; - ss << "Cannot " << c - << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN " - "response."; - throw RecoverableModalException(ss.str().c_str()); - } - - if (!d_env->getOptions().smt.produceModels) - { - std::stringstream ss; - ss << "Cannot " << c << " when produce-models options is off."; - throw ModalException(ss.str().c_str()); - } - - TheoryEngine* te = d_smtSolver->getTheoryEngine(); - Assert(te != nullptr); - TheoryModel* m = te->getBuiltModel(); - - if (m == nullptr) - { - std::stringstream ss; - ss << "Cannot " << c - << " since model is not available. Perhaps the most recent call to " - "check-sat was interrupted?"; - throw RecoverableModalException(ss.str().c_str()); - } - - return m; -} - -QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const -{ - QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine(); - if (qe == nullptr) - { - std::stringstream ss; - ss << "Cannot " << c << " when quantifiers are not present."; - throw ModalException(ss.str().c_str()); - } - return qe; -} - -void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } - -void SmtEngine::notifyPushPost() -{ - TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - Assert(getPropEngine() != nullptr); - getPropEngine()->push(); -} - -void SmtEngine::notifyPopPre() -{ - TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - PropEngine* pe = getPropEngine(); - Assert(pe != nullptr); - pe->pop(); -} - -void SmtEngine::notifyPostSolvePre() -{ - PropEngine* pe = getPropEngine(); - Assert(pe != nullptr); - pe->resetTrail(); -} - -void SmtEngine::notifyPostSolvePost() -{ - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->postsolve(); -} - -Result SmtEngine::checkSat() -{ - Node nullNode; - return checkSat(nullNode); -} - -Result SmtEngine::checkSat(const Node& assumption) -{ - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), {assumption}); - } - std::vector assump; - if (!assumption.isNull()) - { - assump.push_back(assumption); - } - return checkSatInternal(assump, false); -} - -Result SmtEngine::checkSat(const std::vector& assumptions) -{ - if (Dump.isOn("benchmark")) - { - if (assumptions.empty()) - { - getPrinter().toStreamCmdCheckSat(d_env->getDumpOut()); - } - else - { - getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), - assumptions); - } - } - return checkSatInternal(assumptions, false); -} - -Result SmtEngine::checkEntailed(const Node& node) -{ - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdQuery(d_env->getDumpOut(), node); - } - return checkSatInternal( - node.isNull() ? std::vector() : std::vector{node}, - true) - .asEntailmentResult(); -} - -Result SmtEngine::checkEntailed(const std::vector& nodes) -{ - return checkSatInternal(nodes, true).asEntailmentResult(); -} - -Result SmtEngine::checkSatInternal(const std::vector& assumptions, - bool isEntailmentCheck) -{ - try - { - SmtScope smts(this); - finishInit(); - - Trace("smt") << "SmtEngine::" - << (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; - - // Check that SAT results generate a model correctly. - if (d_env->getOptions().smt.checkModels) - { - if (r.asSatisfiabilityResult().isSat() == Result::SAT) - { - checkModel(); - } - } - // Check that UNSAT results generate a proof correctly. - if (d_env->getOptions().smt.checkProofs - || d_env->getOptions().proof.proofCheck - == options::ProofCheckMode::EAGER) - { - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - if ((d_env->getOptions().smt.checkProofs - || d_env->getOptions().proof.proofCheck - == options::ProofCheckMode::EAGER) - && !d_env->getOptions().smt.produceProofs) - { - throw ModalException( - "Cannot check-proofs because proofs were disabled."); - } - checkProof(); - } - } - // Check that UNSAT results generate an unsat core correctly. - if (d_env->getOptions().smt.checkUnsatCores) - { - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); - checkUnsatCore(); - } - } - if (d_env->getOptions().base.statisticsEveryQuery) - { - printStatisticsDiff(); - } - return r; - } - catch (UnsafeInterruptException& e) - { - AlwaysAssert(getResourceManager()->out()); - // Notice that we do not notify the state of this result. If we wanted to - // make the solver resume a working state after an interupt, then we would - // implement a different callback and use it here, e.g. - // d_state.notifyCheckSatInterupt. - Result::UnknownExplanation why = getResourceManager()->outOfResources() - ? Result::RESOURCEOUT - : Result::TIMEOUT; - - if (d_env->getOptions().base.statisticsEveryQuery) - { - printStatisticsDiff(); - } - return Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename); - } -} - -std::vector SmtEngine::getUnsatAssumptions(void) -{ - Trace("smt") << "SMT getUnsatAssumptions()" << endl; - SmtScope smts(this); - if (!d_env->getOptions().smt.unsatAssumptions) - { - throw ModalException( - "Cannot get unsat assumptions when produce-unsat-assumptions option " - "is off."); - } - if (d_state->getMode() != SmtMode::UNSAT) - { - throw RecoverableModalException( - "Cannot get unsat assumptions unless immediately preceded by " - "UNSAT/ENTAILED."); - } - finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut()); - } - UnsatCore core = getUnsatCoreInternal(); - std::vector res; - std::vector& assumps = d_asserts->getAssumptions(); - for (const Node& e : assumps) - { - if (std::find(core.begin(), core.end(), e) != core.end()) - { - res.push_back(e); - } - } - return res; -} - -Result SmtEngine::assertFormula(const Node& formula) -{ - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - - Trace("smt") << "SmtEngine::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() */ - -/* - -------------------------------------------------------------------------- - Handling SyGuS commands - -------------------------------------------------------------------------- -*/ - -void SmtEngine::declareSygusVar(Node var) -{ - SmtScope smts(this); - d_sygusSolver->declareSygusVar(var); -} - -void SmtEngine::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) -{ - // use a null sygus type - TypeNode sygusType; - declareSynthFun(func, sygusType, isInv, vars); -} - -void SmtEngine::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) -{ - SmtScope smts(this); - finishInit(); - d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); -} - -Result SmtEngine::checkSynth() -{ - SmtScope smts(this); - finishInit(); - return d_sygusSolver->checkSynth(*d_asserts); -} - -/* - -------------------------------------------------------------------------- - End of Handling SyGuS commands - -------------------------------------------------------------------------- -*/ - -void SmtEngine::declarePool(const Node& p, const std::vector& initValue) -{ - Assert(p.isVar() && p.getType().isSet()); - finishInit(); - QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool"); - qe->declarePool(p, initValue); -} - -Node SmtEngine::simplify(const Node& ex) -{ - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - // ensure we've processed assertions - d_smtSolver->processAssertions(*d_asserts); - return d_pp->simplify(ex); -} - -Node SmtEngine::expandDefinitions(const Node& ex) -{ - getResourceManager()->spendResource(Resource::PreprocessStep); - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - return d_pp->expandDefinitions(ex); -} - -// TODO(#1108): Simplify the error reporting of this method. -Node SmtEngine::getValue(const Node& ex) const -{ - SmtScope smts(this); - - Trace("smt") << "SMT getValue(" << ex << ")" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex}); - } - TypeNode expectedType = ex.getType(); - - // Substitute out any abstract values in ex and expand - Node n = d_pp->expandDefinitions(ex); - - Trace("smt") << "--- getting value of " << n << endl; - // There are two ways model values for terms are computed (for historical - // reasons). One way is that used in check-model; the other is that - // used by the Model classes. It's not clear to me exactly how these - // 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()) { - n = Rewriter::rewrite(n); - } - - Trace("smt") << "--- getting value of " << n << endl; - TheoryModel* m = getAvailableModel("get-value"); - Assert(m != nullptr); - Node resultNode = m->getValue(n); - Trace("smt") << "--- got value " << n << " = " << resultNode << endl; - Trace("smt") << "--- type " << resultNode.getType() << endl; - Trace("smt") << "--- expected type " << expectedType << endl; - - // type-check the result we got - // Notice that lambdas have function type, which does not respect the subtype - // relation, so we ignore them here. - Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA - || resultNode.getType().isSubtypeOf(expectedType)) - << "Run with -t smt for details."; - - // Ensure it's a constant, or a lambda (for uninterpreted functions). This - // assertion only holds for models that do not have approximate values. - Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA - || resultNode.isConst()); - - if (d_env->getOptions().smt.abstractValues - && resultNode.getType().isArray()) - { - resultNode = d_absValues->mkAbstractValue(resultNode); - Trace("smt") << "--- abstract value >> " << resultNode << endl; - } - - return resultNode; -} - -std::vector SmtEngine::getValues(const std::vector& exprs) const -{ - std::vector result; - for (const Node& e : exprs) - { - result.push_back(getValue(e)); - } - return result; -} - -std::vector SmtEngine::getModelDomainElements(TypeNode tn) const -{ - Assert(tn.isSort()); - TheoryModel* m = getAvailableModel("getModelDomainElements"); - return m->getDomainElements(tn); -} - -bool SmtEngine::isModelCoreSymbol(Node n) -{ - SmtScope smts(this); - Assert(n.isVar()); - const Options& opts = d_env->getOptions(); - if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE) - { - // if the model core mode is none, we are always a model core symbol - return true; - } - TheoryModel* tm = getAvailableModel("isModelCoreSymbol"); - // compute the model core if not done so already - if (!tm->isUsingModelCore()) - { - // If we enabled model cores, we compute a model core for m based on our - // (expanded) assertions using the model core builder utility. Notice that - // we get the assertions using the getAssertionsInternal, which does not - // impact whether we are in "sat" mode - std::vector asserts = getAssertionsInternal(); - d_pp->expandDefinitions(asserts); - ModelCoreBuilder mcb(*d_env.get()); - mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode); - } - return tm->isModelCoreSymbol(n); -} - -std::string SmtEngine::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 - // level. This is to ensure that the information associated with a model is - // completely accessible by the user. This is currently not rigorously - // enforced. An alternative design would be to have this method implemented - // at the API level, but this makes exceptions in the text interface less - // intuitive. - TheoryModel* tm = getAvailableModel("get model"); - // use the smt::Model model utility for printing - const Options& opts = d_env->getOptions(); - bool isKnownSat = (d_state->getMode() == SmtMode::SAT); - Model m(isKnownSat, opts.driver.filename); - // set the model declarations, which determines what is printed in the model - for (const TypeNode& tn : declaredSorts) - { - m.addDeclarationSort(tn, getModelDomainElements(tn)); - } - bool usingModelCores = - (opts.smt.modelCoresMode != options::ModelCoresMode::NONE); - for (const Node& n : declaredFuns) - { - if (usingModelCores && !tm->isModelCoreSymbol(n)) - { - // skip if not in model core - continue; - } - Node value = tm->getValue(n); - m.addDeclarationTerm(n, value); - } - // for separation logic - TypeNode locT, dataT; - if (getSepHeapTypes(locT, dataT)) - { - std::pair sh = getSepHeapAndNilExpr(); - m.setHeapModel(sh.first, sh.second); - } - // print the model - std::stringstream ssm; - ssm << m; - return ssm.str(); -} - -Result SmtEngine::blockModel() -{ - Trace("smt") << "SMT blockModel()" << endl; - SmtScope smts(this); - - finishInit(); - - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdBlockModel(d_env->getDumpOut()); - } - - TheoryModel* m = getAvailableModel("block model"); - - if (d_env->getOptions().smt.blockModelsMode - == options::BlockModelsMode::NONE) - { - std::stringstream ss; - ss << "Cannot block model when block-models is set to none."; - throw RecoverableModalException(ss.str().c_str()); - } - - // get expanded assertions - std::vector eassertsProc = getExpandedAssertions(); - Node eblocker = ModelBlocker::getModelBlocker( - eassertsProc, m, d_env->getOptions().smt.blockModelsMode); - Trace("smt") << "Block formula: " << eblocker << std::endl; - return assertFormula(eblocker); -} - -Result SmtEngine::blockModelValues(const std::vector& exprs) -{ - Trace("smt") << "SMT blockModelValues()" << endl; - SmtScope smts(this); - - finishInit(); - - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs); - } - - TheoryModel* m = getAvailableModel("block model values"); - - // get expanded assertions - std::vector eassertsProc = getExpandedAssertions(); - // we always do block model values mode here - Node eblocker = ModelBlocker::getModelBlocker( - eassertsProc, m, options::BlockModelsMode::VALUES, exprs); - return assertFormula(eblocker); -} - -std::pair SmtEngine::getSepHeapAndNilExpr(void) -{ - if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) - { - const char* msg = - "Cannot obtain separation logic expressions if not using the " - "separation logic theory."; - throw RecoverableModalException(msg); - } - Node heap; - Node nil; - TheoryModel* tm = getAvailableModel("get separation logic heap and nil"); - if (!tm->getHeapModel(heap, nil)) - { - const char* msg = - "Failed to obtain heap/nil " - "expressions from theory model."; - throw RecoverableModalException(msg); - } - return std::make_pair(heap, nil); -} - -std::vector SmtEngine::getAssertionsInternal() -{ - Assert(d_state->isFullyInited()); - context::CDList* al = d_asserts->getAssertionList(); - Assert(al != nullptr); - std::vector res; - for (const Node& n : *al) - { - res.emplace_back(n); - } - return res; -} - -std::vector SmtEngine::getExpandedAssertions() -{ - std::vector easserts = getAssertions(); - // must expand definitions - d_pp->expandDefinitions(easserts); - return easserts; -} -Env& SmtEngine::getEnv() { return *d_env.get(); } - -void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) -{ - if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) - { - const char* msg = - "Cannot declare heap if not using the separation logic theory."; - throw RecoverableModalException(msg); - } - SmtScope smts(this); - finishInit(); - TheoryEngine* te = getTheoryEngine(); - te->declareSepHeap(locT, dataT); -} - -bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) -{ - SmtScope smts(this); - finishInit(); - TheoryEngine* te = getTheoryEngine(); - return te->getSepHeapTypes(locT, dataT); -} - -Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } - -Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } - -void SmtEngine::checkProof() -{ - Assert(d_env->getOptions().smt.produceProofs); - // internal check the proof - PropEngine* pe = getPropEngine(); - Assert(pe != nullptr); - if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER) - { - pe->checkProof(d_asserts->getAssertionList()); - } - Assert(pe->getProof() != nullptr); - std::shared_ptr pePfn = pe->getProof(); - if (d_env->getOptions().smt.checkProofs) - { - d_pfManager->checkProof(pePfn, *d_asserts); - } -} - -StatisticsRegistry& SmtEngine::getStatisticsRegistry() -{ - return d_env->getStatisticsRegistry(); -} - -UnsatCore SmtEngine::getUnsatCoreInternal() -{ - if (!d_env->getOptions().smt.unsatCores) - { - throw ModalException( - "Cannot get an unsat core when produce-unsat-cores or produce-proofs " - "option is off."); - } - if (d_state->getMode() != SmtMode::UNSAT) - { - throw RecoverableModalException( - "Cannot get an unsat core unless immediately preceded by " - "UNSAT/ENTAILED response."); - } - // generate with new proofs - PropEngine* pe = getPropEngine(); - Assert(pe != nullptr); - - std::shared_ptr pepf; - if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) - { - pepf = pe->getRefutation(); - } - else - { - pepf = pe->getProof(); - } - Assert(pepf != nullptr); - std::shared_ptr pfn = d_pfManager->getFinalProof(pepf, *d_asserts); - std::vector core; - d_ucManager->getUnsatCore(pfn, *d_asserts, core); - if (options::minimalUnsatCores()) - { - core = reduceUnsatCore(core); - } - return UnsatCore(core); -} - -std::vector SmtEngine::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; - std::unordered_set removed; - for (const Node& skip : core) - { - std::unique_ptr coreChecker; - initializeSubsolver(coreChecker, *d_env.get()); - coreChecker->setLogic(getLogicInfo()); - coreChecker->getOptions().smt.checkUnsatCores = false; - // disable all proof options - coreChecker->getOptions().smt.produceProofs = false; - coreChecker->getOptions().smt.checkProofs = false; - - for (const Node& ucAssertion : core) - { - if (ucAssertion != skip && removed.find(ucAssertion) == removed.end()) - { - Node assertionAfterExpansion = expandDefinitions(ucAssertion); - coreChecker->assertFormula(assertionAfterExpansion); - } - } - Result r; - try - { - r = coreChecker->checkSat(); - } - catch (...) - { - throw; - } - - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - removed.insert(skip); - } - else if (r.asSatisfiabilityResult().isUnknown()) - { - Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core " - "due to " - "unknown result."; - } - } - - if (removed.empty()) - { - return core; - } - else - { - std::vector newUcAssertions; - for (const Node& n : core) - { - if (removed.find(n) == removed.end()) - { - newUcAssertions.push_back(n); - } - } - - return newUcAssertions; - } -} - -void SmtEngine::checkUnsatCore() { - Assert(d_env->getOptions().smt.unsatCores) - << "cannot check unsat core if unsat cores are turned off"; - - Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; - UnsatCore core = getUnsatCore(); - - // initialize the core checker - std::unique_ptr coreChecker; - initializeSubsolver(coreChecker, *d_env.get()); - coreChecker->getOptions().smt.checkUnsatCores = false; - // disable all proof options - coreChecker->getOptions().smt.produceProofs = false; - coreChecker->getOptions().smt.checkProofs = false; - - // set up separation logic heap if necessary - TypeNode sepLocType, sepDataType; - if (getSepHeapTypes(sepLocType, sepDataType)) - { - coreChecker->declareSepHeap(sepLocType, sepDataType); - } - - Notice() << "SmtEngine::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 - << ", expanded to " << assertionAfterExpansion << "\n"; - coreChecker->assertFormula(assertionAfterExpansion); - } - Result r; - try { - r = coreChecker->checkSat(); - } catch(...) { - throw; - } - Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; - if(r.asSatisfiabilityResult().isUnknown()) { - Warning() - << "SmtEngine::checkUnsatCore(): could not check core result unknown." - << std::endl; - } - else if (r.asSatisfiabilityResult().isSat()) - { - InternalError() - << "SmtEngine::checkUnsatCore(): produced core was satisfiable."; - } -} - -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. - Assert(al != nullptr) - << "don't have an assertion list to check in SmtEngine::checkModel()"; - - TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); - - Notice() << "SmtEngine::checkModel(): generating model" << endl; - TheoryModel* m = getAvailableModel("check model"); - Assert(m != nullptr); - - // check the model with the theory engine for debugging - if (options::debugCheckModels()) - { - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->checkTheoryAssertionsWithModel(hardFailure); - } - - // check the model with the check models utility - Assert(d_checkModels != nullptr); - d_checkModels->checkModel(m, al, hardFailure); -} - -UnsatCore SmtEngine::getUnsatCore() { - Trace("smt") << "SMT getUnsatCore()" << std::endl; - SmtScope smts(this); - finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetUnsatCore(d_env->getDumpOut()); - } - return getUnsatCoreInternal(); -} - -void SmtEngine::getRelevantInstantiationTermVectors( - std::map& insts, bool getDebugInfo) -{ - Assert(d_state->getMode() == SmtMode::UNSAT); - // generate with new proofs - PropEngine* pe = getPropEngine(); - Assert(pe != nullptr); - Assert(pe->getProof() != nullptr); - std::shared_ptr pfn = - d_pfManager->getFinalProof(pe->getProof(), *d_asserts); - d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo); -} - -std::string SmtEngine::getProof() -{ - Trace("smt") << "SMT getProof()\n"; - SmtScope smts(this); - finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetProof(d_env->getDumpOut()); - } - if (!d_env->getOptions().smt.produceProofs) - { - throw ModalException("Cannot get a proof when proof option is off."); - } - if (d_state->getMode() != SmtMode::UNSAT) - { - throw RecoverableModalException( - "Cannot get a proof unless immediately preceded by " - "UNSAT/ENTAILED response."); - } - // the prop engine has the proof of false - PropEngine* pe = getPropEngine(); - Assert(pe != nullptr); - Assert(pe->getProof() != nullptr); - Assert(d_pfManager); - std::ostringstream ss; - d_pfManager->printProof(ss, pe->getProof(), *d_asserts); - return ss.str(); -} - -void SmtEngine::printInstantiations( std::ostream& out ) { - SmtScope smts(this); - finishInit(); - QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); - - // First, extract and print the skolemizations - bool printed = false; - bool reqNames = !d_env->getOptions().printer.printInstFull; - // only print when in list mode - if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST) - { - std::map> sks; - qe->getSkolemTermVectors(sks); - for (const std::pair>& s : sks) - { - Node name; - if (!qe->getNameForQuant(s.first, name, reqNames)) - { - // did not have a name and we are only printing formulas with names - continue; - } - SkolemList slist(name, s.second); - out << slist; - printed = true; - } - } - - // Second, extract and print the instantiations - std::map rinsts; - if (d_env->getOptions().smt.produceProofs - && (!d_env->getOptions().smt.unsatCores - || d_env->getOptions().smt.unsatCoresMode - == options::UnsatCoresMode::FULL_PROOF) - && getSmtMode() == SmtMode::UNSAT) - { - // minimize instantiations based on proof manager - getRelevantInstantiationTermVectors(rinsts, - options::dumpInstantiationsDebug()); - } - else - { - std::map>> insts; - getInstantiationTermVectors(insts); - for (const std::pair>>& i : insts) - { - // convert to instantiation list - Node q = i.first; - InstantiationList& ilq = rinsts[q]; - ilq.initialize(q); - for (const std::vector& ii : i.second) - { - ilq.d_inst.push_back(InstantiationVec(ii)); - } - } - } - for (std::pair& i : rinsts) - { - if (i.second.d_inst.empty()) - { - // no instantiations, skip - continue; - } - Node name; - if (!qe->getNameForQuant(i.first, name, reqNames)) - { - // did not have a name and we are only printing formulas with names - continue; - } - // must have a name - if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM) - { - out << "(num-instantiations " << name << " " << i.second.d_inst.size() - << ")" << std::endl; - } - else - { - // take the name - i.second.d_quant = name; - Assert(d_env->getOptions().printer.printInstMode - == options::PrintInstMode::LIST); - out << i.second; - } - printed = true; - } - // if we did not print anything, we indicate this - if (!printed) - { - out << "none" << std::endl; - } -} - -void SmtEngine::getInstantiationTermVectors( - std::map>>& insts) -{ - SmtScope smts(this); - finishInit(); - QuantifiersEngine* qe = - getAvailableQuantifiersEngine("getInstantiationTermVectors"); - // get the list of all instantiations - qe->getInstantiationTermVectors(insts); -} - -bool SmtEngine::getSynthSolutions(std::map& solMap) -{ - SmtScope smts(this); - finishInit(); - return d_sygusSolver->getSynthSolutions(solMap); -} - -Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) -{ - SmtScope smts(this); - finishInit(); - const LogicInfo& logic = getLogicInfo(); - if (!logic.isPure(THEORY_ARITH) && strict) - { - Warning() << "Unexpected logic for quantifier elimination " << logic - << endl; - } - return d_quantElimSolver->getQuantifierElimination( - *d_asserts, q, doFull, d_isInternalSubsolver); -} - -bool SmtEngine::getInterpol(const Node& conj, - const TypeNode& grammarType, - Node& interpol) -{ - SmtScope smts(this); - finishInit(); - std::vector axioms = getExpandedAssertions(); - bool success = - d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol); - // notify the state of whether the get-interpol call was successfuly, which - // impacts the SMT mode. - d_state->notifyGetInterpol(success); - return success; -} - -bool SmtEngine::getInterpol(const Node& conj, Node& interpol) -{ - TypeNode grammarType; - return getInterpol(conj, grammarType, interpol); -} - -bool SmtEngine::getAbduct(const Node& conj, - const TypeNode& grammarType, - Node& abd) -{ - SmtScope smts(this); - finishInit(); - std::vector axioms = getExpandedAssertions(); - bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd); - // notify the state of whether the get-abduct call was successfuly, which - // impacts the SMT mode. - d_state->notifyGetAbduct(success); - return success; -} - -bool SmtEngine::getAbduct(const Node& conj, Node& abd) -{ - TypeNode grammarType; - return getAbduct(conj, grammarType, abd); -} - -void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) -{ - SmtScope smts(this); - QuantifiersEngine* qe = - getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas"); - qe->getInstantiatedQuantifiedFormulas(qs); -} - -void SmtEngine::getInstantiationTermVectors( - Node q, std::vector>& tvecs) -{ - SmtScope smts(this); - QuantifiersEngine* qe = - getAvailableQuantifiersEngine("getInstantiationTermVectors"); - qe->getInstantiationTermVectors(q, tvecs); -} - -std::vector SmtEngine::getAssertions() -{ - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetAssertions(d_env->getDumpOut()); - } - Trace("smt") << "SMT getAssertions()" << endl; - if (!d_env->getOptions().smt.produceAssertions) - { - const char* msg = - "Cannot query the current assertion list when not in produce-assertions mode."; - throw ModalException(msg); - } - return getAssertionsInternal(); -} - -void SmtEngine::getDifficultyMap(std::map& dmap) -{ - Trace("smt") << "SMT getDifficultyMap()\n"; - SmtScope smts(this); - finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetDifficulty(d_env->getDumpOut()); - } - if (!d_env->getOptions().smt.produceDifficulty) - { - throw ModalException( - "Cannot get difficulty when difficulty option is off."); - } - // the prop engine has the proof of false - Assert(d_pfManager); - // get difficulty map from theory engine first - TheoryEngine* te = getTheoryEngine(); - te->getDifficultyMap(dmap); - // then ask proof manager to translate dmap in terms of the input - d_pfManager->translateDifficultyMap(dmap, *d_asserts); -} - -void SmtEngine::push() -{ - SmtScope smts(this); - finishInit(); - d_state->doPendingPops(); - Trace("smt") << "SMT push()" << endl; - d_smtSolver->processAssertions(*d_asserts); - if(Dump.isOn("benchmark")) { - getPrinter().toStreamCmdPush(d_env->getDumpOut()); - } - d_state->userPush(); -} - -void SmtEngine::pop() { - SmtScope smts(this); - finishInit(); - Trace("smt") << "SMT pop()" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdPop(d_env->getDumpOut()); - } - d_state->userPop(); - - // Clear out assertion queues etc., in case anything is still in there - d_asserts->clearCurrent(); - // clear the learned literals from the preprocessor - d_pp->clearLearnedLiterals(); - - Trace("userpushpop") << "SmtEngine: 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() -{ - SmtScope smts(this); - - if (!d_state->isFullyInited()) - { - // We're still in Start Mode, nothing asserted yet, do nothing. - // (see solver execution modes in the SMT-LIB standard) - Assert(getContext()->getLevel() == 0); - Assert(getUserContext()->getLevel() == 0); - getDumpManager()->resetAssertions(); - return; - } - - - Trace("smt") << "SMT resetAssertions()" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdResetAssertions(d_env->getDumpOut()); - } - - d_asserts->clearCurrent(); - d_state->notifyResetAssertions(); - getDumpManager()->resetAssertions(); - // push the state to maintain global context around everything - d_state->setup(); - - // reset SmtSolver, which will construct a new prop engine - d_smtSolver->resetAssertions(); -} - -void SmtEngine::interrupt() -{ - if (!d_state->isFullyInited()) - { - return; - } - d_smtSolver->interrupt(); -} - -void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) -{ - if (cumulative) - { - d_env->d_options.base.cumulativeResourceLimit = units; - } - else - { - d_env->d_options.base.perCallResourceLimit = units; - } -} -void SmtEngine::setTimeLimit(uint64_t millis) -{ - d_env->d_options.base.perCallMillisecondLimit = millis; -} - -unsigned long SmtEngine::getResourceUsage() const -{ - return getResourceManager()->getResourceUsage(); -} - -unsigned long SmtEngine::getTimeUsage() const -{ - return getResourceManager()->getTimeUsage(); -} - -unsigned long SmtEngine::getResourceRemaining() const -{ - return getResourceManager()->getResourceRemaining(); -} - -NodeManager* SmtEngine::getNodeManager() const -{ - return d_env->getNodeManager(); -} - -void SmtEngine::printStatisticsSafe(int fd) const -{ - d_env->getStatisticsRegistry().printSafe(fd); -} - -void SmtEngine::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) -{ - Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; - - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdSetOption(d_env->getDumpOut(), key, value); - } - - if (key == "command-verbosity") - { - size_t fstIndex = value.find(" "); - size_t sndIndex = value.find(" ", fstIndex + 1); - if (sndIndex == std::string::npos) - { - string c = value.substr(1, fstIndex - 1); - int v = - std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1)); - if (v < 0 || v > 2) - { - throw OptionException("command-verbosity must be 0, 1, or 2"); - } - d_commandVerbosity[c] = v; - return; - } - throw OptionException( - "command-verbosity value must be a tuple (command-name integer)"); - } - - if (value.find(" ") != std::string::npos) - { - throw OptionException("bad value for :" + key); - } - - std::string optionarg = value; - options::set(getOptions(), key, optionarg); -} - -void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } - -bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } - -std::string SmtEngine::getOption(const std::string& key) const -{ - NodeManager* nm = d_env->getNodeManager(); - - Trace("smt") << "SMT getOption(" << key << ")" << endl; - - if (key.find("command-verbosity:") == 0) - { - auto it = d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); - if (it != d_commandVerbosity.end()) - { - return std::to_string(it->second); - } - it = d_commandVerbosity.find("*"); - if (it != d_commandVerbosity.end()) - { - return std::to_string(it->second); - } - return "2"; - } - - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key); - } - - if (key == "command-verbosity") - { - vector result; - Node defaultVerbosity; - 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 - Node name = nm->mkBoundVar(verb.first, nm->integerType()); - Node value = nm->mkConst(Rational(verb.second)); - if (verb.first == "*") - { - // put the default at the end of the SExpr - defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value); - } - else - { - result.push_back(nm->mkNode(Kind::SEXPR, name, value)); - } - } - // ensure the default is always listed - if (defaultVerbosity.isNull()) - { - defaultVerbosity = nm->mkNode(Kind::SEXPR, - nm->mkBoundVar("*", nm->integerType()), - nm->mkConst(Rational(2))); - } - result.push_back(defaultVerbosity); - return nm->mkNode(Kind::SEXPR, result).toString(); - } - - return options::get(getOptions(), key); -} - -Options& SmtEngine::getOptions() { return d_env->d_options; } - -const Options& SmtEngine::getOptions() const { return d_env->getOptions(); } - -ResourceManager* SmtEngine::getResourceManager() const -{ - return d_env->getResourceManager(); -} - -DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); } - -const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); } - -OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } - -theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } - -} // namespace cvc5 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h deleted file mode 100644 index a06b2fd61..000000000 --- a/src/smt/smt_engine.h +++ /dev/null @@ -1,1123 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * SmtEngine: the main public entry point of libcvc5. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__SMT_ENGINE_H -#define CVC5__SMT_ENGINE_H - -#include -#include -#include -#include - -#include "context/cdhashmap_forward.h" -#include "cvc5_export.h" -#include "options/options.h" -#include "smt/output_manager.h" -#include "smt/smt_mode.h" -#include "theory/logic_info.h" -#include "util/result.h" - -namespace cvc5 { - -template class NodeTemplate; -typedef NodeTemplate Node; -typedef NodeTemplate TNode; -class TypeNode; - -class Env; -class NodeManager; -class TheoryEngine; -class UnsatCore; -class StatisticsRegistry; -class Printer; -class ResourceManager; -struct InstantiationList; - -/* -------------------------------------------------------------------------- */ - -namespace api { -class Solver; -} // namespace api - -/* -------------------------------------------------------------------------- */ - -namespace context { - class Context; - class UserContext; - } // namespace context - -/* -------------------------------------------------------------------------- */ - -namespace preprocessing { -class PreprocessingPassContext; -} - -/* -------------------------------------------------------------------------- */ - -namespace prop { - class PropEngine; - } // namespace prop - -/* -------------------------------------------------------------------------- */ - -namespace smt { -/** Utilities */ -class SmtEngineState; -class AbstractValues; -class Assertions; -class DumpManager; -class ResourceOutListener; -class SmtNodeManagerListener; -class OptionsManager; -class Preprocessor; -class CheckModels; -/** Subsolvers */ -class SmtSolver; -class SygusSolver; -class AbductionSolver; -class InterpolationSolver; -class QuantElimSolver; - -struct SmtEngineStatistics; -class SmtScope; -class PfManager; -class UnsatCoreManager; - -} // namespace smt - -/* -------------------------------------------------------------------------- */ - -namespace theory { -class TheoryModel; -class Rewriter; -class QuantifiersEngine; -} // namespace theory - -/* -------------------------------------------------------------------------- */ - -class CVC5_EXPORT SmtEngine -{ - friend class ::cvc5::api::Solver; - friend class ::cvc5::smt::SmtEngineState; - friend class ::cvc5::smt::SmtScope; - - /* ....................................................................... */ - public: - /* ....................................................................... */ - - /** - * 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. - */ - SmtEngine(NodeManager* nm, const Options* optr = nullptr); - /** Destruct the SMT engine. */ - ~SmtEngine(); - - //--------------------------------------------- concerning the state - - /** - * This is the main initialization procedure of the SmtEngine. - * - * 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 - * assertions and queries are made). - * - * Internally, this creates the theory engine, prop engine, decision engine, - * and other utilities whose initialization depends on the final set of - * 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 - * to simplify() is issued, a scope is pushed, etc. - */ - void finishInit(); - /** - * Return true if this SmtEngine is fully initialized (post-construction) - * by the above call. - */ - bool isFullyInited() const; - /** - * Return true if a checkEntailed() or checkSatisfiability() has been made. - */ - bool isQueryMade() const; - /** Return the user context level. */ - size_t getNumUserLevels() const; - /** Return the current mode of the solver. */ - SmtMode getSmtMode() const; - /** - * Whether the SmtMode allows for get-value, get-model, get-assignment, etc. - * This is equivalent to: - * getSmtMode()==SmtMode::SAT || getSmtMode()==SmtMode::SAT_UNKNOWN - */ - bool isSmtModeSat() const; - /** - * Returns the most recent result of checkSat/checkEntailed or - * (set-info :status). - */ - Result getStatusOfLastCommand() const; - //--------------------------------------------- end concerning the state - - /** - * Set the logic of the script. - * @throw ModalException, LogicException - */ - void setLogic(const std::string& logic); - - /** - * Set the logic of the script. - * @throw ModalException, LogicException - */ - void setLogic(const char* logic); - - /** - * Set the logic of the script. - * @throw ModalException - */ - void setLogic(const LogicInfo& logic); - - /** Get the logic information currently set. */ - const LogicInfo& getLogicInfo() const; - - /** Get the logic information set by the user. */ - LogicInfo getUserLogicInfo() const; - - /** - * Set information about the script executing. - */ - void setInfo(const std::string& key, const std::string& value); - - /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */ - bool isValidGetInfoFlag(const std::string& key) const; - - /** Query information about the SMT environment. */ - std::string getInfo(const std::string& key) const; - - /** - * Set an aspect of the current SMT execution environment. - * @throw OptionException, ModalException - */ - void setOption(const std::string& key, const std::string& value); - - /** 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 - * --sygus-abduct. - */ - void setIsInternalSubsolver(); - /** Is this an internal subsolver? */ - bool isInternalSubsolver() const; - - /** - * Block the current model. Can be called only if immediately preceded by - * a SAT or INVALID query. Only permitted if produce-models is on, and the - * block-models option is set to a mode other than "none". - * - * This adds an assertion to the assertion stack that blocks the current - * model based on the current options configured by cvc5. - * - * The return value has the same meaning as that of assertFormula. - */ - Result blockModel(); - - /** - * Block the current model values of (at least) the values in exprs. - * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query. - * Only permitted if produce-models is on, and the block-models option is set - * to a mode other than "none". - * - * This adds an assertion to the assertion stack of the form: - * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn))) - * where M0 ... Mn are the current model values of exprs[0] ... exprs[n]. - * - * The return value has the same meaning as that of assertFormula. - */ - Result blockModelValues(const std::vector& exprs); - - /** - * Declare heap. For smt2 inputs, this is called when the command - * (declare-heap (locT datat)) is invoked by the user. This sets locT as the - * location type and dataT is the data type for the heap. This command should - * be executed only once, and must be invoked before solving separation logic - * inputs. - */ - void declareSepHeap(TypeNode locT, TypeNode dataT); - - /** - * Get the separation heap types, which extracts which types were passed to - * the method above. - * - * @return true if the separation logic heap types have been declared. - */ - bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT); - - /** When using separation logic, obtain the expression for the heap. */ - Node getSepHeapExpr(); - - /** When using separation logic, obtain the expression for nil. */ - Node getSepNilExpr(); - - /** - * Get an aspect of the current SMT execution environment. - * @throw OptionException - */ - std::string getOption(const std::string& key) const; - - /** - * Define function func in the current context to be: - * (lambda (formals) formula) - * This adds func to the list of defined functions, which indicates that - * all occurrences of func should be expanded during expandDefinitions. - * - * @param func a variable of function type that expects the arguments in - * formal - * @param formals a list of BOUND_VARIABLE expressions - * @param formula The body of the function, must not contain func - * @param global True if this definition is global (i.e. should persist when - * popping the user context) - */ - void defineFunction(Node func, - const std::vector& formals, - Node formula, - bool global = false); - - /** - * Define functions recursive - * - * For each i, this constrains funcs[i] in the current context to be: - * (lambda (formals[i]) formulas[i]) - * where formulas[i] may contain variables from funcs. Unlike defineFunction - * above, we do not add funcs[i] to the set of defined functions. Instead, - * we consider funcs[i] to be a free uninterpreted function, and add: - * forall formals[i]. f(formals[i]) = formulas[i] - * to the set of assertions in the current context. - * This method expects input such that for each i: - * - func[i] : a variable of function type that expects the arguments in - * formals[i], and - * - formals[i] : a list of BOUND_VARIABLE expressions. - * - * @param global True if this definition is global (i.e. should persist when - * popping the user context) - */ - void defineFunctionsRec(const std::vector& funcs, - const std::vector>& formals, - const std::vector& formulas, - bool global = false); - /** - * Define function recursive - * Same as above, but for a single function. - */ - void defineFunctionRec(Node func, - const std::vector& formals, - Node formula, - bool global = false); - /** - * Add a formula to the current context: preprocess, do per-theory - * setup, use processAssertionList(), asserting to T-solver for - * literals and conjunction of literals. Returns false if - * immediately determined to be inconsistent. Note this formula will - * be included in the unsat core when applicable. - * - * @throw TypeCheckingException, LogicException, UnsafeInterruptException - */ - Result assertFormula(const Node& formula); - - /** - * Reduce an unsatisfiable core to make it minimal. - */ - std::vector reduceUnsatCore(const std::vector& core); - - /** - * Check if a given (set of) expression(s) is entailed with respect to the - * current set of assertions. We check this by asserting the negation of - * the (big AND over the) given (set of) expression(s). - * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result. - * - * @throw Exception - */ - Result checkEntailed(const Node& assumption); - Result checkEntailed(const std::vector& assumptions); - - /** - * Assert a formula (if provided) to the current context and call - * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result. - * - * @throw Exception - */ - Result checkSat(); - Result checkSat(const Node& assumption); - Result checkSat(const std::vector& assumptions); - - /** - * Returns a set of so-called "failed" assumptions. - * - * The returned set is a subset of the set of assumptions of a previous - * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability - * with this set of failed assumptions still produces an unsat answer. - * - * Note that the returned set of failed assumptions is not necessarily - * minimal. - */ - std::vector getUnsatAssumptions(void); - - /*---------------------------- sygus commands ---------------------------*/ - - /** - * Add sygus variable declaration. - * - * Declared SyGuS variables may be used in SyGuS constraints, in which they - * are assumed to be universally quantified. - * - * In SyGuS semantics, declared functions are treated in the same manner as - * declared variables, i.e. as universally quantified (function) variables - * which can occur in the SyGuS constraints that compose the conjecture to - * which a function is being synthesized. Thus declared functions should use - * this method as well. - */ - void declareSygusVar(Node var); - - /** - * Add a function-to-synthesize declaration. - * - * The given sygusType may not correspond to the actual function type of func - * but to a datatype encoding the syntax restrictions for the - * function-to-synthesize. In this case this information is stored to be used - * during solving. - * - * vars contains the arguments of the function-to-synthesize. These variables - * are also stored to be used during solving. - * - * isInv determines whether the function-to-synthesize is actually an - * invariant. This information is necessary if we are dumping a command - * corresponding to this declaration, so that it can be properly printed. - */ - void declareSynthFun(Node func, - TypeNode sygusType, - bool isInv, - const std::vector& vars); - /** - * Same as above, without a sygus type. - */ - void declareSynthFun(Node func, bool isInv, const std::vector& vars); - - /** - * Add a regular sygus constraint or assumption. - * @param n The formula - * @param isAssume True if n is an assumption. - */ - void assertSygusConstraint(Node n, bool isAssume = false); - - /** - * Add an invariant constraint. - * - * Invariant constraints are not explicitly declared: they are given in terms - * of the invariant-to-synthesize, the pre condition, transition relation and - * post condition. The actual constraint is built based on the inputs of these - * place holder predicates : - * - * PRE(x) -> INV(x) - * INV() ^ TRANS(x, x') -> INV(x') - * INV(x) -> POST(x) - * - * The regular and primed variables are retrieved from the declaration of the - * invariant-to-synthesize. - */ - void assertSygusInvConstraint(Node inv, Node pre, Node trans, Node post); - /** - * Assert a synthesis conjecture to the current context and call - * check(). Returns sat, unsat, or unknown result. - * - * The actual synthesis conjecture is built based on the previously - * communicated information to this module (universal variables, defined - * functions, functions-to-synthesize, and which constraints compose it). The - * built conjecture is a higher-order formula of the form - * - * exists f1...fn . forall v1...vm . F - * - * in which f1...fn are the functions-to-synthesize, v1...vm are the declared - * universal variables and F is the set of declared constraints. - * - * @throw Exception - */ - Result checkSynth(); - - /*------------------------- end of sygus commands ------------------------*/ - - /** - * Declare pool whose initial value is the terms in initValue. A pool is - * a variable of type (Set T) that is used in quantifier annotations and does - * not occur in constraints. - * - * @param p The pool to declare, which should be a variable of type (Set T) - * for some type T. - * @param initValue The initial value of p, which should be a vector of terms - * of type T. - */ - void declarePool(const Node& p, const std::vector& initValue); - /** - * Simplify a formula without doing "much" work. Does not involve - * the SAT Engine in the simplification, but uses the current - * definitions, assertions, and the current partial model, if one - * has been constructed. It also involves theory normalization. - * - * @throw TypeCheckingException, LogicException, UnsafeInterruptException - * - * @todo (design) is this meant to give an equivalent or an - * equisatisfiable formula? - */ - Node simplify(const Node& e); - - /** - * Expand the definitions in a term or formula. - * - * @param n The node to expand - * - * @throw TypeCheckingException, LogicException, UnsafeInterruptException - */ - Node expandDefinitions(const Node& n); - - /** - * 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. - * - * @throw ModalException, TypeCheckingException, LogicException, - * UnsafeInterruptException - */ - Node getValue(const Node& e) const; - - /** - * Same as getValue but for a vector of expressions - */ - std::vector getValues(const std::vector& exprs) const; - - /** - * @return the domain elements for uninterpreted sort tn. - */ - std::vector getModelDomainElements(TypeNode tn) const; - - /** - * @return true if v is a model core symbol - */ - bool isModelCoreSymbol(Node v); - - /** - * Get a model (only if immediately preceded by an SAT or unknown query). - * Only permitted if the model option is on. - * - * @param declaredSorts The sorts to print in the model - * @param declaredFuns The free constants to print in the model. A subset - * of these may be printed based on isModelCoreSymbol. - * @return the string corresponding to the model. If the output language is - * smt2, then this corresponds to a response to the get-model command. - */ - std::string getModel(const std::vector& declaredSorts, - const std::vector& declaredFuns); - - /** print instantiations - * - * Print all instantiations for all quantified formulas on out, - * returns true if at least one instantiation was printed. The type of output - * (list, num, etc.) is determined by printInstMode. - */ - void printInstantiations(std::ostream& out); - /** - * Print the current proof. This method should be called after an UNSAT - * response. It gets the proof of false from the PropEngine and passes - * it to the ProofManager, which post-processes the proof and prints it - * in the proper format. - */ - void printProof(); - - /** - * Get synth solution. - * - * This method returns true if we are in a state immediately preceded by - * a successful call to checkSynth. - * - * This method adds entries to solMap that map functions-to-synthesize with - * their solutions, for all active conjectures. This should be called - * immediately after the solver answers unsat for sygus input. - * - * Specifically, given a sygus conjecture of the form - * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn ) - * where x1...xn are second order bound variables, we map each xi to - * lambda term in solMap such that - * forall y1...yn. P( solMap[x1]...solMap[xn], y1...yn ) - * is a valid formula. - */ - bool getSynthSolutions(std::map& solMap); - - /** - * Do quantifier elimination. - * - * This function takes as input a quantified formula q - * of the form: - * Q x1...xn. P( x1...xn, y1...yn ) - * where P( x1...xn, y1...yn ) is a quantifier-free - * formula in a logic that supports quantifier elimination. - * Currently, the only logics supported by quantifier - * elimination is LRA and LIA. - * - * This function returns a formula ret such that, given - * the current set of formulas A asserted to this SmtEngine : - * - * If doFull = true, then - * - ( A ^ q ) and ( A ^ ret ) are equivalent - * - ret is quantifier-free formula containing - * only free variables in y1...yn. - * - * If doFull = false, then - * - (A ^ q) => (A ^ ret) if Q is forall or - * (A ^ ret) => (A ^ q) if Q is exists, - * - ret is quantifier-free formula containing - * only free variables in y1...yn, - * - If Q is exists, let A^Q_n be the formula - * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n - * where for each i=1,...n, formula ret^Q_i - * is the result of calling doQuantifierElimination - * for q with the set of assertions A^Q_{i-1}. - * Similarly, if Q is forall, then let A^Q_n be - * A ^ ret^Q_1 ^ ... ^ ret^Q_n - * where ret^Q_i is the same as above. - * In either case, we have that ret^Q_j will - * eventually be true or false, for some finite j. - * - * The former feature is quantifier elimination, and - * is run on invocations of the smt2 extended command get-qe. - * The latter feature is referred to as partial quantifier - * elimination, and is run on invocations of the smt2 - * extended command get-qe-disjunct, which can be used - * for incrementally computing the result of a - * quantifier elimination. - * - * The argument strict is whether to output - * warnings, such as when an unexpected logic is used. - * - * throw@ Exception - */ - Node getQuantifierElimination(Node q, bool doFull, bool strict = true); - - /** - * This method asks this SMT engine to find an interpolant with respect to - * the current assertion stack (call it A) and the conjecture (call it B). If - * this method returns true, then interpolant is set to a formula I such that - * A ^ ~I and I ^ ~B are both unsatisfiable. - * - * The argument grammarType is a sygus datatype type that encodes the syntax - * restrictions on the shapes of possible solutions. - * - * This method invokes a separate copy of the SMT engine for solving the - * corresponding sygus problem for generating such a solution. - */ - bool getInterpol(const Node& conj, - const TypeNode& grammarType, - Node& interpol); - - /** Same as above, but without user-provided grammar restrictions */ - bool getInterpol(const Node& conj, Node& interpol); - - /** - * This method asks this SMT engine to find an abduct with respect to the - * current assertion stack (call it A) and the conjecture (call it B). - * If this method returns true, then abd is set to a formula C such that - * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable. - * - * The argument grammarType is a sygus datatype type that encodes the syntax - * restrictions on the shape of possible solutions. - * - * This method invokes a separate copy of the SMT engine for solving the - * corresponding sygus problem for generating such a solution. - */ - bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd); - - /** Same as above, but without user-provided grammar restrictions */ - bool getAbduct(const Node& conj, Node& abd); - - /** - * Get list of quantified formulas that were instantiated on the last call - * to check-sat. - */ - void getInstantiatedQuantifiedFormulas(std::vector& qs); - - /** - * Get instantiation term vectors for quantified formula q. - * - * This method is similar to above, but in the example above, we return the - * (vectors of) terms t1, ..., tn instead. - * - * Notice that these are not guaranteed to come in the same order as the - * instantiation lemmas above. - */ - void getInstantiationTermVectors(Node q, - std::vector>& tvecs); - /** - * As above but only the instantiations that were relevant for the - * refutation. - */ - void getRelevantInstantiationTermVectors( - std::map& insts, bool getDebugInfo = false); - /** - * Get instantiation term vectors, which maps each instantiated quantified - * formula to the list of instantiations for that quantified formula. This - * list is minimized if proofs are enabled, and this call is immediately - * preceded by an UNSAT or ENTAILED query - */ - void getInstantiationTermVectors( - std::map>>& insts); - - /** - * Get an unsatisfiable core (only if immediately preceded by an UNSAT or - * ENTAILED query). Only permitted if cvc5 was built with unsat-core support - * and produce-unsat-cores is on. - */ - UnsatCore getUnsatCore(); - - /** - * Get a refutation proof (only if immediately preceded by an UNSAT or - * ENTAILED query). Only permitted if cvc5 was built with proof support and - * the proof option is on. */ - std::string getProof(); - - /** - * Get the current set of assertions. Only permitted if the - * SmtEngine is set to operate interactively. - */ - std::vector getAssertions(); - - /** - * Get difficulty map, which populates dmap, mapping input assertions - * to a value that estimates their difficulty for solving the current problem. - */ - void getDifficultyMap(std::map& dmap); - - /** - * Push a user-level context. - * throw@ ModalException, LogicException, UnsafeInterruptException - */ - void push(); - - /** - * Pop a user-level context. Throws an exception if nothing to pop. - * @throw ModalException - */ - void pop(); - - /** Reset all assertions, global declarations, etc. */ - void resetAssertions(); - - /** - * Interrupt a running query. This can be called from another thread - * or from a signal handler. Throws a ModalException if the SmtEngine - * isn't currently in a query. - * - * @throw ModalException - */ - void interrupt(); - - /** - * Set a resource limit for SmtEngine 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 - * versions of cvc5 (as may the number of conflicts required, anyway), - * and it might even be different between instances of the same version - * of cvc5 on different platforms. - * - * A cumulative and non-cumulative (per-call) resource limit can be - * set at the same time. A call to setResourceLimit() with - * 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 - * at the same time. - * - * When an SmtEngine is first created, it has no time or resource - * limits. - * - * Currently, these limits only cause the SmtEngine 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 - * 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. - * - * 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. - * - * Note that the per-call timer only ticks away when one of the - * SmtEngine'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 - * limits. - * - * Currently, these limits only cause the SmtEngine 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 millis the time limit in milliseconds, or 0 for no limit - */ - void setTimeLimit(uint64_t millis); - - /** - * Get the current resource usage count for this SmtEngine. 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. */ - unsigned long getTimeUsage() const; - - /** - * Get the remaining resources that can be consumed by this SmtEngine - * according to the currently-set cumulative resource limit. If there - * is not a cumulative resource limit set, this function throws a - * ModalException. - * - * @throw ModalException - */ - unsigned long getResourceRemaining() const; - - /** Permit access to the underlying NodeManager. */ - NodeManager* getNodeManager() const; - - /** - * Print statistics from the statistics registry in the env object owned by - * this SmtEngine. 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 - * time. Internally prints the diff and then stores a snapshot for the next - * call. - */ - void printStatisticsDiff() const; - - /** Get the options object (const and non-const versions) */ - Options& getOptions(); - const Options& getOptions() const; - - /** Get a pointer to the UserContext owned by this SmtEngine. */ - context::UserContext* getUserContext(); - - /** Get a pointer to the Context owned by this SmtEngine. */ - context::Context* getContext(); - - /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ - TheoryEngine* getTheoryEngine(); - - /** Get a pointer to the PropEngine owned by this SmtEngine. */ - prop::PropEngine* getPropEngine(); - - /** Get the resource manager of this SMT engine */ - ResourceManager* getResourceManager() const; - - /** Permit access to the underlying dump manager. */ - smt::DumpManager* getDumpManager(); - - /** Get the printer used by this SMT engine */ - const Printer& getPrinter() const; - - /** Get the output manager for this SMT engine */ - OutputManager& getOutputManager(); - - /** Get a pointer to the Rewriter owned by this SmtEngine. */ - theory::Rewriter* getRewriter(); - /** - * Get expanded assertions. - * - * Return the set of assertions, after expanding definitions. - */ - std::vector getExpandedAssertions(); - - /** - * !!!!! temporary, until the environment is passsed to all classes that - * require it. - */ - Env& getEnv(); - /* ....................................................................... */ - private: - /* ....................................................................... */ - - // disallow copy/assignment - SmtEngine(const SmtEngine&) = delete; - SmtEngine& operator=(const SmtEngine&) = delete; - - /** Set solver instance that owns this SmtEngine. */ - void setSolver(api::Solver* solver) { d_solver = solver; } - - /** Get a pointer to the (new) PfManager owned by this SmtEngine. */ - smt::PfManager* getPfManager() { return d_pfManager.get(); }; - - /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ - StatisticsRegistry& getStatisticsRegistry(); - - /** - * Internal method to get an unsatisfiable core (only if immediately preceded - * by an UNSAT or ENTAILED query). Only permitted if cvc5 was built with - * unsat-core support and produce-unsat-cores is on. Does not dump the - * command. - */ - UnsatCore getUnsatCoreInternal(); - - /** - * Check that a generated proof checks. This method is the same as printProof, - * but does not print the proof. Like that method, it should be called - * after an UNSAT response. It ensures that a well-formed proof of false - * can be constructed by the combination of the PropEngine and ProofManager. - */ - void checkProof(); - - /** - * Check that an unsatisfiable core is indeed unsatisfiable. - */ - void checkUnsatCore(); - - /** - * Check that a generated Model (via getModel()) actually satisfies - * all user assertions. - */ - void checkModel(bool hardFailure = true); - - /** - * Check that a solution to an interpolation problem is indeed a solution. - * - * The check is made by determining that the assertions imply the solution of - * the interpolation problem (interpol), and the solution implies the goal - * (conj). If these criteria are not met, an internal error is thrown. - */ - void checkInterpol(Node interpol, - const std::vector& easserts, - const Node& conj); - - /** - * This is called by the destructor, 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(); - - /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). - */ - Result quickCheck(); - - /** - * Get the (SMT-level) model pointer, if we are in SAT mode. Otherwise, - * return nullptr. - * - * This ensures that the underlying theory model of the SmtSolver maintained - * by this class is currently available, which means that cvc5 is producing - * models, and is in "SAT mode", otherwise a recoverable exception is thrown. - * - * @param c used for giving an error message to indicate the context - * this method was called. - */ - theory::TheoryModel* getAvailableModel(const char* c) const; - /** - * Get available quantifiers engine, which throws a modal exception if it - * does not exist. This can happen if a quantifiers-specific call (e.g. - * getInstantiatedQuantifiedFormulas) is called in a non-quantified logic. - * - * @param c used for giving an error message to indicate the context - * this method was called. - */ - theory::QuantifiersEngine* getAvailableQuantifiersEngine(const char* c) const; - - // --------------------------------------- callbacks from the state - /** - * Notify push pre, which is called just before the user context of the state - * pushes. This processes all pending assertions. - */ - void notifyPushPre(); - /** - * Notify push post, which is called just after the user context of the state - * pushes. This performs a push on the underlying prop engine. - */ - void notifyPushPost(); - /** - * Notify pop pre, which is called just before the user context of the state - * pops. This performs a pop on the underlying prop engine. - */ - void notifyPopPre(); - /** - * Notify post solve pre, which is called once per check-sat query. It - * is triggered when the first d_state.doPendingPops() is issued after the - * check-sat. This method is called before the contexts pop in the method - * doPendingPops. - */ - void notifyPostSolvePre(); - /** - * Same as above, but after contexts are popped. This calls the postsolve - * method of the underlying TheoryEngine. - */ - void notifyPostSolvePost(); - // --------------------------------------- end callbacks from the state - - /** - * Internally handle the setting of a logic. This function should always - * be called when d_logic is updated. - */ - void setLogicInternal(); - - /* - * Check satisfiability (used to check satisfiability and entailment). - */ - Result checkSatInternal(const std::vector& assumptions, - bool isEntailmentCheck); - - /** - * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is - * the function that the formal argument list is for. This method is used - * as a helper function when defining (recursive) functions. - */ - void debugCheckFormals(const std::vector& formals, Node func); - - /** - * Checks whether formula is a valid function body for func whose formal - * argument list is stored in formals. This method is - * used as a helper function when defining (recursive) functions. - */ - void debugCheckFunctionBody(Node formula, - const std::vector& formals, - Node func); - - /** - * Helper method to obtain both the heap and nil from the solver. Returns a - * std::pair where the first element is the heap expression and the second - * element is the nil expression. - */ - std::pair getSepHeapAndNilExpr(); - /** - * Get assertions internal, which is only called after initialization. This - * should be used internally to get the assertions instead of getAssertions - * or getExpandedAssertions, which may trigger initialization and SMT state - * changes. - */ - std::vector getAssertionsInternal(); - /* Members -------------------------------------------------------------- */ - - /** Solver instance that owns this SmtEngine instance. */ - api::Solver* d_solver = nullptr; - - /** - * The environment object, which contains all utilities that are globally - * available to internal code. - */ - std::unique_ptr d_env; - /** - * The state of this SmtEngine, which is responsible for maintaining which - * SMT mode we are in, the contexts, the last result, etc. - */ - std::unique_ptr d_state; - - /** Abstract values */ - std::unique_ptr d_absValues; - /** Assertions manager */ - std::unique_ptr d_asserts; - /** Resource out listener */ - std::unique_ptr d_routListener; - /** Node manager listener */ - std::unique_ptr d_snmListener; - - /** The SMT solver */ - std::unique_ptr d_smtSolver; - - /** - * The utility used for checking models - */ - std::unique_ptr d_checkModels; - - /** - * The proof manager, which manages all things related to checking, - * processing, and printing proofs. - */ - std::unique_ptr d_pfManager; - - /** - * The unsat core manager, which produces unsat cores and related information - * from refutations. */ - std::unique_ptr d_ucManager; - - /** The solver for sygus queries */ - std::unique_ptr d_sygusSolver; - - /** The solver for abduction queries */ - std::unique_ptr d_abductSolver; - /** The solver for interpolation queries */ - std::unique_ptr d_interpolSolver; - /** The solver for quantifier elimination queries */ - std::unique_ptr d_quantElimSolver; - - /** - * The logic set by the user. The actual logic, which may extend the user's - * logic, lives in the Env class. - */ - LogicInfo d_userLogic; - - /** Whether this is an internal subsolver. */ - bool d_isInternalSubsolver; - - /** - * Verbosity of various commands. - */ - std::map d_commandVerbosity; - - /** The statistics class */ - std::unique_ptr d_stats; - - /** the output manager for commands */ - mutable OutputManager d_outMgr; - /** - * The preprocessor. - */ - 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. - */ - std::unique_ptr d_scope; -}; /* class SmtEngine */ - -/* -------------------------------------------------------------------------- */ - -} // namespace cvc5 - -#endif /* CVC5__SMT_ENGINE_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/solver_engine.cpp b/src/smt/solver_engine.cpp new file mode 100644 index 000000000..1a03aea0a --- /dev/null +++ b/src/smt/solver_engine.cpp @@ -0,0 +1,2058 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The main entry point into the cvc5 library's SMT interface. + */ + +#include "smt/solver_engine.h" + +#include "base/check.h" +#include "base/exception.h" +#include "base/modal_exception.h" +#include "base/output.h" +#include "decision/decision_engine.h" +#include "expr/bound_var_manager.h" +#include "expr/node.h" +#include "options/base_options.h" +#include "options/expr_options.h" +#include "options/language.h" +#include "options/main_options.h" +#include "options/option_exception.h" +#include "options/options_public.h" +#include "options/parser_options.h" +#include "options/printer_options.h" +#include "options/proof_options.h" +#include "options/smt_options.h" +#include "options/theory_options.h" +#include "printer/printer.h" +#include "proof/unsat_core.h" +#include "prop/prop_engine.h" +#include "smt/abduction_solver.h" +#include "smt/abstract_values.h" +#include "smt/assertions.h" +#include "smt/check_models.h" +#include "smt/dump.h" +#include "smt/dump_manager.h" +#include "smt/env.h" +#include "smt/interpolation_solver.h" +#include "smt/listeners.h" +#include "smt/logic_exception.h" +#include "smt/model_blocker.h" +#include "smt/model_core_builder.h" +#include "smt/node_command.h" +#include "smt/preprocessor.h" +#include "smt/proof_manager.h" +#include "smt/quant_elim_solver.h" +#include "smt/set_defaults.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_engine_state.h" +#include "smt/smt_engine_stats.h" +#include "smt/smt_solver.h" +#include "smt/sygus_solver.h" +#include "smt/unsat_core_manager.h" +#include "theory/quantifiers/instantiation_list.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/smt_engine_subsolver.h" +#include "theory/theory_engine.h" +#include "util/random.h" +#include "util/rational.h" +#include "util/resource_manager.h" +#include "util/sexpr.h" +#include "util/statistics_registry.h" + +// required for hacks related to old proofs for unsat cores +#include "base/configuration.h" +#include "base/configuration_private.h" + +using namespace std; +using namespace cvc5::smt; +using namespace cvc5::preprocessing; +using namespace cvc5::prop; +using namespace cvc5::context; +using namespace cvc5::theory; + +namespace cvc5 { + +SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) + : d_env(new Env(nm, optr)), + d_state(new SmtEngineState(*d_env.get(), *this)), + d_absValues(new AbstractValues(getNodeManager())), + d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), + d_routListener(new ResourceOutListener(*this)), + d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), + d_smtSolver(nullptr), + d_checkModels(nullptr), + d_pfManager(nullptr), + d_ucManager(nullptr), + d_sygusSolver(nullptr), + d_abductSolver(nullptr), + d_interpolSolver(nullptr), + d_quantElimSolver(nullptr), + d_isInternalSubsolver(false), + d_stats(nullptr), + d_outMgr(this), + 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. + d_scope.reset(new SmtScope(this)); + // listen to node manager events + getNodeManager()->subscribeEvents(d_snmListener.get()); + // listen to resource out + getResourceManager()->registerListener(d_routListener.get()); + // make statistics + d_stats.reset(new SmtEngineStatistics()); + // reset the preprocessor + d_pp.reset( + new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); + // make the SMT solver + d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats)); + // make the SyGuS solver + d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp)); + // make the quantifier elimination solver + 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 +{ + return d_state->getNumUserLevels(); +} +SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); } +bool SmtEngine::isSmtModeSat() const +{ + SmtMode mode = getSmtMode(); + return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN; +} +Result SmtEngine::getStatusOfLastCommand() const +{ + return d_state->getStatus(); +} +context::UserContext* SmtEngine::getUserContext() +{ + return d_env->getUserContext(); +} +context::Context* SmtEngine::getContext() { return d_env->getContext(); } + +TheoryEngine* SmtEngine::getTheoryEngine() +{ + return d_smtSolver->getTheoryEngine(); +} + +prop::PropEngine* SmtEngine::getPropEngine() +{ + return d_smtSolver->getPropEngine(); +} + +void SmtEngine::finishInit() +{ + if (d_state->isFullyInited()) + { + // already initialized, return + return; + } + + // Notice that finishInitInternal is called when options are finalized. If we + // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52 + // of SMT-LIB 2.6 standard. + + // set the logic + const LogicInfo& logic = getLogicInfo(); + if (!logic.isLocked()) + { + setLogicInternal(); + } + + // set the random seed + Random::getRandom().setSeed(d_env->getOptions().driver.seed); + + // Call finish init on the set defaults module. This inializes the logic + // and the best default options based on our heuristics. + SetDefaults sdefaults(d_isInternalSubsolver); + sdefaults.setDefaults(d_env->d_logic, getOptions()); + + if (d_env->getOptions().smt.produceProofs) + { + // ensure bound variable uses canonical bound variables + getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); + // make the proof manager + d_pfManager.reset(new PfManager(*d_env.get())); + PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); + // start the unsat core manager + d_ucManager.reset(new UnsatCoreManager()); + // enable it in the assertions pipeline + d_asserts->setProofGenerator(pppg); + // enabled proofs in the preprocessor + d_pp->setProofGenerator(pppg); + } + + Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; + d_smtSolver->finishInit(logic); + + // now can construct the SMT-level model object + TheoryEngine* te = d_smtSolver->getTheoryEngine(); + Assert(te != nullptr); + TheoryModel* tm = te->getModel(); + if (tm != nullptr) + { + // make the check models utility + d_checkModels.reset(new CheckModels(*d_env.get())); + } + + // global push/pop around everything, to ensure proper destruction + // of context-dependent data structures + d_state->setup(); + + Trace("smt-debug") << "Set up assertions..." << std::endl; + d_asserts->finishInit(); + + // dump out a set-logic command only when raw-benchmark is disabled to avoid + // 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()); + } + + // initialize the dump manager + getDumpManager()->finishInit(); + + // subsolvers + if (d_env->getOptions().smt.produceAbducts) + { + d_abductSolver.reset(new AbductionSolver(*d_env.get())); + } + if (d_env->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + { + d_interpolSolver.reset(new InterpolationSolver(*d_env.get())); + } + + d_pp->finishInit(); + + AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) + << "The PropEngine has pushed but the SmtEngine " + "hasn't finished initializing!"; + + Assert(getLogicInfo().isLocked()); + + // store that we are finished initializing + d_state->finishInit(); + Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; +} + +void SmtEngine::shutdown() +{ + d_state->shutdown(); + + d_smtSolver->shutdown(); + + d_env->shutdown(); +} + +SmtEngine::~SmtEngine() +{ + SmtScope smts(this); + + 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 + d_pp->cleanup(); + + d_pfManager.reset(nullptr); + d_ucManager.reset(nullptr); + + d_absValues.reset(nullptr); + d_asserts.reset(nullptr); + + d_abductSolver.reset(nullptr); + d_interpolSolver.reset(nullptr); + d_quantElimSolver.reset(nullptr); + d_sygusSolver.reset(nullptr); + d_smtSolver.reset(nullptr); + + d_stats.reset(nullptr); + getNodeManager()->unsubscribeEvents(d_snmListener.get()); + d_snmListener.reset(nullptr); + d_routListener.reset(nullptr); + d_pp.reset(nullptr); + // destroy the state + d_state.reset(nullptr); + // destroy the environment + d_env.reset(nullptr); + } + catch (Exception& e) + { + Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl; + } +} + +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."); + } + d_env->d_logic = logic; + d_userLogic = logic; + setLogicInternal(); +} + +void SmtEngine::setLogic(const std::string& s) +{ + SmtScope smts(this); + try + { + setLogic(LogicInfo(s)); + } + catch (IllegalArgumentException& e) + { + throw LogicException(e.what()); + } +} + +void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } + +const LogicInfo& SmtEngine::getLogicInfo() const +{ + return d_env->getLogicInfo(); +} + +LogicInfo SmtEngine::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. + LogicInfo res = d_userLogic; + res.lock(); + return res; +} + +void SmtEngine::setLogicInternal() +{ + Assert(!d_state->isFullyInited()) + << "setting logic in SmtEngine 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) +{ + SmtScope smts(this); + + Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; + + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value); + } + + if (key == "filename") + { + d_env->d_options.driver.filename = value; + d_env->d_originalOptions->driver.filename = value; + d_env->getStatisticsRegistry().registerValue( + "driver::filename", value); + } + else if (key == "smt-lib-version" + && !getOptions().base.inputLanguageWasSetByUser) + { + Language ilang = Language::LANG_SMTLIB_V2_6; + + if (value != "2" && value != "2.6") + { + Warning() << "SMT-LIB version " << value + << " unsupported, defaulting to language (and semantics of) " + "SMT-LIB 2.6\n"; + } + getOptions().base.inputLanguage = ilang; + // also update the output language + if (!getOptions().base.outputLanguageWasSetByUser) + { + Language olang = ilang; + if (d_env->getOptions().base.outputLanguage != olang) + { + getOptions().base.outputLanguage = olang; + *d_env->getOptions().base.out << language::SetLanguage(olang); + } + } + } + else if (key == "status") + { + d_state->notifyExpectedStatus(value); + } +} + +bool SmtEngine::isValidGetInfoFlag(const std::string& key) const +{ + if (key == "all-statistics" || key == "error-behavior" || key == "name" + || key == "version" || key == "authors" || key == "status" + || key == "reason-unknown" || key == "assertion-stack-levels" + || key == "all-options" || key == "time") + { + return true; + } + return false; +} + +std::string SmtEngine::getInfo(const std::string& key) const +{ + SmtScope smts(this); + + Trace("smt") << "SMT getInfo(" << key << ")" << endl; + if (key == "all-statistics") + { + return toSExpr(d_env->getStatisticsRegistry().begin(), + d_env->getStatisticsRegistry().end()); + } + if (key == "error-behavior") + { + return "immediate-exit"; + } + if (key == "filename") + { + return d_env->getOptions().driver.filename; + } + if (key == "name") + { + return toSExpr(Configuration::getName()); + } + if (key == "version") + { + return toSExpr(Configuration::getVersionString()); + } + if (key == "authors") + { + return toSExpr(Configuration::about()); + } + if (key == "status") + { + // sat | unsat | unknown + Result status = d_state->getStatus(); + switch (status.asSatisfiabilityResult().isSat()) + { + case Result::SAT: return "sat"; + case Result::UNSAT: return "unsat"; + default: return "unknown"; + } + } + if (key == "time") + { + return toSExpr(std::clock()); + } + if (key == "reason-unknown") + { + Result status = d_state->getStatus(); + if (!status.isNull() && status.isUnknown()) + { + std::stringstream ss; + ss << status.whyUnknown(); + std::string s = ss.str(); + transform(s.begin(), s.end(), s.begin(), ::tolower); + return s; + } + else + { + throw RecoverableModalException( + "Can't get-info :reason-unknown when the " + "last result wasn't unknown!"); + } + } + if (key == "assertion-stack-levels") + { + size_t ulevel = d_state->getNumUserLevels(); + AlwaysAssert(ulevel <= std::numeric_limits::max()); + return toSExpr(ulevel); + } + Assert(key == "all-options"); + // get the options, like all-statistics + std::vector> res; + for (const auto& opt : options::getNames()) + { + res.emplace_back( + std::vector{opt, options::get(getOptions(), opt)}); + } + return toSExpr(res); +} + +void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) +{ + for (std::vector::const_iterator i = formals.begin(); + i != formals.end(); + ++i) + { + if ((*i).getKind() != kind::BOUND_VARIABLE) + { + stringstream ss; + 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(); + throw TypeCheckingExceptionPrivate(func, ss.str()); + } + } +} + +void SmtEngine::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 + // doesn't match the SMT-LIBv2 standard... + if (formals.size() > 0) + { + TypeNode rangeType = funcType.getRangeType(); + if (!formulaType.isComparableTo(rangeType)) + { + stringstream ss; + ss << "Type of defined function does not match its declaration\n" + << "The function : " << func << "\n" + << "Declared type : " << rangeType << "\n" + << "The body : " << formula << "\n" + << "Body type : " << formulaType; + throw TypeCheckingExceptionPrivate(func, ss.str()); + } + } + else + { + if (!formulaType.isComparableTo(funcType)) + { + stringstream ss; + ss << "Declared type of defined constant does not match its definition\n" + << "The constant : " << func << "\n" + << "Declared type : " << funcType << "\n" + << "The definition : " << formula << "\n" + << "Definition type: " << formulaType; + throw TypeCheckingExceptionPrivate(func, ss.str()); + } + } +} + +void SmtEngine::defineFunction(Node func, + const std::vector& formals, + Node formula, + bool global) +{ + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + Trace("smt") << "SMT defineFunction(" << func << ")" << endl; + debugCheckFormals(formals, func); + + stringstream ss; + ss << language::SetLanguage( + language::SetLanguage::getLanguage(Dump.getStream())) + << func; + + DefineFunctionNodeCommand nc(ss.str(), func, formals, formula); + getDumpManager()->addToDump(nc, "declarations"); + + // type check body + debugCheckFunctionBody(formula, formals, func); + + // Substitute out any abstract values in formula + Node def = d_absValues->substituteAbstractValues(formula); + if (!formals.empty()) + { + NodeManager* nm = NodeManager::currentNM(); + def = nm->mkNode( + kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def); + } + // A define-fun is treated as a (higher-order) assertion. It is provided + // to the assertions object. It will be added as a top-level substitution + // within this class, possibly multiple times if global is true. + Node feq = func.eqNode(def); + d_asserts->addDefineFunDefinition(feq, global); +} + +void SmtEngine::defineFunctionsRec( + const std::vector& funcs, + const std::vector>& formals, + const std::vector& formulas, + bool global) +{ + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + Trace("smt") << "SMT defineFunctionsRec(...)" << endl; + + if (funcs.size() != formals.size() && funcs.size() != formulas.size()) + { + stringstream ss; + ss << "Number of functions, formals, and function bodies passed to " + "defineFunctionsRec do not match:" + << "\n" + << " #functions : " << funcs.size() << "\n" + << " #arg lists : " << formals.size() << "\n" + << " #function bodies : " << formulas.size() << "\n"; + throw ModalException(ss.str()); + } + for (unsigned i = 0, size = funcs.size(); i < size; i++) + { + // check formal argument list + debugCheckFormals(formals[i], funcs[i]); + // type check body + debugCheckFunctionBody(formulas[i], formals[i], funcs[i]); + } + + NodeManager* nm = getNodeManager(); + for (unsigned i = 0, size = funcs.size(); i < size; i++) + { + // we assert a quantified formula + Node func_app; + // make the function application + if (formals[i].empty()) + { + // it has no arguments + func_app = funcs[i]; + } + else + { + std::vector children; + children.push_back(funcs[i]); + children.insert(children.end(), formals[i].begin(), formals[i].end()); + func_app = nm->mkNode(kind::APPLY_UF, children); + } + Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]); + if (!formals[i].empty()) + { + // set the attribute to denote this is a function definition + Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app); + aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr); + FunDefAttribute fda; + func_app.setAttribute(fda, true); + // make the quantified formula + Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]); + lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr); + } + // 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. + // 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) +{ + std::vector funcs; + funcs.push_back(func); + std::vector> formals_multi; + formals_multi.push_back(formals); + std::vector formulas; + formulas.push_back(formula); + defineFunctionsRec(funcs, formals_multi, formulas, global); +} + +Result SmtEngine::quickCheck() +{ + Assert(d_state->isFullyInited()); + Trace("smt") << "SMT quickCheck()" << endl; + const std::string& filename = d_env->getOptions().driver.filename; + return Result( + Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); +} + +TheoryModel* SmtEngine::getAvailableModel(const char* c) const +{ + if (!d_env->getOptions().theory.assignFunctionValues) + { + std::stringstream ss; + ss << "Cannot " << c << " when --assign-function-values is false."; + throw RecoverableModalException(ss.str().c_str()); + } + + if (d_state->getMode() != SmtMode::SAT + && d_state->getMode() != SmtMode::SAT_UNKNOWN) + { + std::stringstream ss; + ss << "Cannot " << c + << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN " + "response."; + throw RecoverableModalException(ss.str().c_str()); + } + + if (!d_env->getOptions().smt.produceModels) + { + std::stringstream ss; + ss << "Cannot " << c << " when produce-models options is off."; + throw ModalException(ss.str().c_str()); + } + + TheoryEngine* te = d_smtSolver->getTheoryEngine(); + Assert(te != nullptr); + TheoryModel* m = te->getBuiltModel(); + + if (m == nullptr) + { + std::stringstream ss; + ss << "Cannot " << c + << " since model is not available. Perhaps the most recent call to " + "check-sat was interrupted?"; + throw RecoverableModalException(ss.str().c_str()); + } + + return m; +} + +QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const +{ + QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine(); + if (qe == nullptr) + { + std::stringstream ss; + ss << "Cannot " << c << " when quantifiers are not present."; + throw ModalException(ss.str().c_str()); + } + return qe; +} + +void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } + +void SmtEngine::notifyPushPost() +{ + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); + Assert(getPropEngine() != nullptr); + getPropEngine()->push(); +} + +void SmtEngine::notifyPopPre() +{ + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + pe->pop(); +} + +void SmtEngine::notifyPostSolvePre() +{ + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + pe->resetTrail(); +} + +void SmtEngine::notifyPostSolvePost() +{ + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->postsolve(); +} + +Result SmtEngine::checkSat() +{ + Node nullNode; + return checkSat(nullNode); +} + +Result SmtEngine::checkSat(const Node& assumption) +{ + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), {assumption}); + } + std::vector assump; + if (!assumption.isNull()) + { + assump.push_back(assumption); + } + return checkSatInternal(assump, false); +} + +Result SmtEngine::checkSat(const std::vector& assumptions) +{ + if (Dump.isOn("benchmark")) + { + if (assumptions.empty()) + { + getPrinter().toStreamCmdCheckSat(d_env->getDumpOut()); + } + else + { + getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), + assumptions); + } + } + return checkSatInternal(assumptions, false); +} + +Result SmtEngine::checkEntailed(const Node& node) +{ + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdQuery(d_env->getDumpOut(), node); + } + return checkSatInternal( + node.isNull() ? std::vector() : std::vector{node}, + true) + .asEntailmentResult(); +} + +Result SmtEngine::checkEntailed(const std::vector& nodes) +{ + return checkSatInternal(nodes, true).asEntailmentResult(); +} + +Result SmtEngine::checkSatInternal(const std::vector& assumptions, + bool isEntailmentCheck) +{ + try + { + SmtScope smts(this); + finishInit(); + + Trace("smt") << "SmtEngine::" + << (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; + + // Check that SAT results generate a model correctly. + if (d_env->getOptions().smt.checkModels) + { + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + checkModel(); + } + } + // Check that UNSAT results generate a proof correctly. + if (d_env->getOptions().smt.checkProofs + || d_env->getOptions().proof.proofCheck + == options::ProofCheckMode::EAGER) + { + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + if ((d_env->getOptions().smt.checkProofs + || d_env->getOptions().proof.proofCheck + == options::ProofCheckMode::EAGER) + && !d_env->getOptions().smt.produceProofs) + { + throw ModalException( + "Cannot check-proofs because proofs were disabled."); + } + checkProof(); + } + } + // Check that UNSAT results generate an unsat core correctly. + if (d_env->getOptions().smt.checkUnsatCores) + { + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); + checkUnsatCore(); + } + } + if (d_env->getOptions().base.statisticsEveryQuery) + { + printStatisticsDiff(); + } + return r; + } + catch (UnsafeInterruptException& e) + { + AlwaysAssert(getResourceManager()->out()); + // Notice that we do not notify the state of this result. If we wanted to + // make the solver resume a working state after an interupt, then we would + // implement a different callback and use it here, e.g. + // d_state.notifyCheckSatInterupt. + Result::UnknownExplanation why = getResourceManager()->outOfResources() + ? Result::RESOURCEOUT + : Result::TIMEOUT; + + if (d_env->getOptions().base.statisticsEveryQuery) + { + printStatisticsDiff(); + } + return Result( + Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename); + } +} + +std::vector SmtEngine::getUnsatAssumptions(void) +{ + Trace("smt") << "SMT getUnsatAssumptions()" << endl; + SmtScope smts(this); + if (!d_env->getOptions().smt.unsatAssumptions) + { + throw ModalException( + "Cannot get unsat assumptions when produce-unsat-assumptions option " + "is off."); + } + if (d_state->getMode() != SmtMode::UNSAT) + { + throw RecoverableModalException( + "Cannot get unsat assumptions unless immediately preceded by " + "UNSAT/ENTAILED."); + } + finishInit(); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut()); + } + UnsatCore core = getUnsatCoreInternal(); + std::vector res; + std::vector& assumps = d_asserts->getAssumptions(); + for (const Node& e : assumps) + { + if (std::find(core.begin(), core.end(), e) != core.end()) + { + res.push_back(e); + } + } + return res; +} + +Result SmtEngine::assertFormula(const Node& formula) +{ + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + + Trace("smt") << "SmtEngine::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() */ + +/* + -------------------------------------------------------------------------- + Handling SyGuS commands + -------------------------------------------------------------------------- +*/ + +void SmtEngine::declareSygusVar(Node var) +{ + SmtScope smts(this); + d_sygusSolver->declareSygusVar(var); +} + +void SmtEngine::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) +{ + // use a null sygus type + TypeNode sygusType; + declareSynthFun(func, sygusType, isInv, vars); +} + +void SmtEngine::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) +{ + SmtScope smts(this); + finishInit(); + d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); +} + +Result SmtEngine::checkSynth() +{ + SmtScope smts(this); + finishInit(); + return d_sygusSolver->checkSynth(*d_asserts); +} + +/* + -------------------------------------------------------------------------- + End of Handling SyGuS commands + -------------------------------------------------------------------------- +*/ + +void SmtEngine::declarePool(const Node& p, const std::vector& initValue) +{ + Assert(p.isVar() && p.getType().isSet()); + finishInit(); + QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool"); + qe->declarePool(p, initValue); +} + +Node SmtEngine::simplify(const Node& ex) +{ + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + // ensure we've processed assertions + d_smtSolver->processAssertions(*d_asserts); + return d_pp->simplify(ex); +} + +Node SmtEngine::expandDefinitions(const Node& ex) +{ + getResourceManager()->spendResource(Resource::PreprocessStep); + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + return d_pp->expandDefinitions(ex); +} + +// TODO(#1108): Simplify the error reporting of this method. +Node SmtEngine::getValue(const Node& ex) const +{ + SmtScope smts(this); + + Trace("smt") << "SMT getValue(" << ex << ")" << endl; + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex}); + } + TypeNode expectedType = ex.getType(); + + // Substitute out any abstract values in ex and expand + Node n = d_pp->expandDefinitions(ex); + + Trace("smt") << "--- getting value of " << n << endl; + // There are two ways model values for terms are computed (for historical + // reasons). One way is that used in check-model; the other is that + // used by the Model classes. It's not clear to me exactly how these + // 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()) + { + n = Rewriter::rewrite(n); + } + + Trace("smt") << "--- getting value of " << n << endl; + TheoryModel* m = getAvailableModel("get-value"); + Assert(m != nullptr); + Node resultNode = m->getValue(n); + Trace("smt") << "--- got value " << n << " = " << resultNode << endl; + Trace("smt") << "--- type " << resultNode.getType() << endl; + Trace("smt") << "--- expected type " << expectedType << endl; + + // type-check the result we got + // Notice that lambdas have function type, which does not respect the subtype + // relation, so we ignore them here. + Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA + || resultNode.getType().isSubtypeOf(expectedType)) + << "Run with -t smt for details."; + + // Ensure it's a constant, or a lambda (for uninterpreted functions). This + // assertion only holds for models that do not have approximate values. + Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA + || resultNode.isConst()); + + if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray()) + { + resultNode = d_absValues->mkAbstractValue(resultNode); + Trace("smt") << "--- abstract value >> " << resultNode << endl; + } + + return resultNode; +} + +std::vector SmtEngine::getValues(const std::vector& exprs) const +{ + std::vector result; + for (const Node& e : exprs) + { + result.push_back(getValue(e)); + } + return result; +} + +std::vector SmtEngine::getModelDomainElements(TypeNode tn) const +{ + Assert(tn.isSort()); + TheoryModel* m = getAvailableModel("getModelDomainElements"); + return m->getDomainElements(tn); +} + +bool SmtEngine::isModelCoreSymbol(Node n) +{ + SmtScope smts(this); + Assert(n.isVar()); + const Options& opts = d_env->getOptions(); + if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE) + { + // if the model core mode is none, we are always a model core symbol + return true; + } + TheoryModel* tm = getAvailableModel("isModelCoreSymbol"); + // compute the model core if not done so already + if (!tm->isUsingModelCore()) + { + // If we enabled model cores, we compute a model core for m based on our + // (expanded) assertions using the model core builder utility. Notice that + // we get the assertions using the getAssertionsInternal, which does not + // impact whether we are in "sat" mode + std::vector asserts = getAssertionsInternal(); + d_pp->expandDefinitions(asserts); + ModelCoreBuilder mcb(*d_env.get()); + mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode); + } + return tm->isModelCoreSymbol(n); +} + +std::string SmtEngine::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 + // level. This is to ensure that the information associated with a model is + // completely accessible by the user. This is currently not rigorously + // enforced. An alternative design would be to have this method implemented + // at the API level, but this makes exceptions in the text interface less + // intuitive. + TheoryModel* tm = getAvailableModel("get model"); + // use the smt::Model model utility for printing + const Options& opts = d_env->getOptions(); + bool isKnownSat = (d_state->getMode() == SmtMode::SAT); + Model m(isKnownSat, opts.driver.filename); + // set the model declarations, which determines what is printed in the model + for (const TypeNode& tn : declaredSorts) + { + m.addDeclarationSort(tn, getModelDomainElements(tn)); + } + bool usingModelCores = + (opts.smt.modelCoresMode != options::ModelCoresMode::NONE); + for (const Node& n : declaredFuns) + { + if (usingModelCores && !tm->isModelCoreSymbol(n)) + { + // skip if not in model core + continue; + } + Node value = tm->getValue(n); + m.addDeclarationTerm(n, value); + } + // for separation logic + TypeNode locT, dataT; + if (getSepHeapTypes(locT, dataT)) + { + std::pair sh = getSepHeapAndNilExpr(); + m.setHeapModel(sh.first, sh.second); + } + // print the model + std::stringstream ssm; + ssm << m; + return ssm.str(); +} + +Result SmtEngine::blockModel() +{ + Trace("smt") << "SMT blockModel()" << endl; + SmtScope smts(this); + + finishInit(); + + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdBlockModel(d_env->getDumpOut()); + } + + TheoryModel* m = getAvailableModel("block model"); + + if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) + { + std::stringstream ss; + ss << "Cannot block model when block-models is set to none."; + throw RecoverableModalException(ss.str().c_str()); + } + + // get expanded assertions + std::vector eassertsProc = getExpandedAssertions(); + Node eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m, d_env->getOptions().smt.blockModelsMode); + Trace("smt") << "Block formula: " << eblocker << std::endl; + return assertFormula(eblocker); +} + +Result SmtEngine::blockModelValues(const std::vector& exprs) +{ + Trace("smt") << "SMT blockModelValues()" << endl; + SmtScope smts(this); + + finishInit(); + + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs); + } + + TheoryModel* m = getAvailableModel("block model values"); + + // get expanded assertions + std::vector eassertsProc = getExpandedAssertions(); + // we always do block model values mode here + Node eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m, options::BlockModelsMode::VALUES, exprs); + return assertFormula(eblocker); +} + +std::pair SmtEngine::getSepHeapAndNilExpr(void) +{ + if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) + { + const char* msg = + "Cannot obtain separation logic expressions if not using the " + "separation logic theory."; + throw RecoverableModalException(msg); + } + Node heap; + Node nil; + TheoryModel* tm = getAvailableModel("get separation logic heap and nil"); + if (!tm->getHeapModel(heap, nil)) + { + const char* msg = + "Failed to obtain heap/nil " + "expressions from theory model."; + throw RecoverableModalException(msg); + } + return std::make_pair(heap, nil); +} + +std::vector SmtEngine::getAssertionsInternal() +{ + Assert(d_state->isFullyInited()); + context::CDList* al = d_asserts->getAssertionList(); + Assert(al != nullptr); + std::vector res; + for (const Node& n : *al) + { + res.emplace_back(n); + } + return res; +} + +std::vector SmtEngine::getExpandedAssertions() +{ + std::vector easserts = getAssertions(); + // must expand definitions + d_pp->expandDefinitions(easserts); + return easserts; +} +Env& SmtEngine::getEnv() { return *d_env.get(); } + +void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) +{ + if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) + { + const char* msg = + "Cannot declare heap if not using the separation logic theory."; + throw RecoverableModalException(msg); + } + SmtScope smts(this); + finishInit(); + TheoryEngine* te = getTheoryEngine(); + te->declareSepHeap(locT, dataT); +} + +bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) +{ + SmtScope smts(this); + finishInit(); + TheoryEngine* te = getTheoryEngine(); + return te->getSepHeapTypes(locT, dataT); +} + +Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } + +Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } + +void SmtEngine::checkProof() +{ + Assert(d_env->getOptions().smt.produceProofs); + // internal check the proof + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER) + { + pe->checkProof(d_asserts->getAssertionList()); + } + Assert(pe->getProof() != nullptr); + std::shared_ptr pePfn = pe->getProof(); + if (d_env->getOptions().smt.checkProofs) + { + d_pfManager->checkProof(pePfn, *d_asserts); + } +} + +StatisticsRegistry& SmtEngine::getStatisticsRegistry() +{ + return d_env->getStatisticsRegistry(); +} + +UnsatCore SmtEngine::getUnsatCoreInternal() +{ + if (!d_env->getOptions().smt.unsatCores) + { + throw ModalException( + "Cannot get an unsat core when produce-unsat-cores or produce-proofs " + "option is off."); + } + if (d_state->getMode() != SmtMode::UNSAT) + { + throw RecoverableModalException( + "Cannot get an unsat core unless immediately preceded by " + "UNSAT/ENTAILED response."); + } + // generate with new proofs + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + + std::shared_ptr pepf; + if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) + { + pepf = pe->getRefutation(); + } + else + { + pepf = pe->getProof(); + } + Assert(pepf != nullptr); + std::shared_ptr pfn = d_pfManager->getFinalProof(pepf, *d_asserts); + std::vector core; + d_ucManager->getUnsatCore(pfn, *d_asserts, core); + if (options::minimalUnsatCores()) + { + core = reduceUnsatCore(core); + } + return UnsatCore(core); +} + +std::vector SmtEngine::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; + std::unordered_set removed; + for (const Node& skip : core) + { + std::unique_ptr coreChecker; + initializeSubsolver(coreChecker, *d_env.get()); + coreChecker->setLogic(getLogicInfo()); + coreChecker->getOptions().smt.checkUnsatCores = false; + // disable all proof options + coreChecker->getOptions().smt.produceProofs = false; + coreChecker->getOptions().smt.checkProofs = false; + + for (const Node& ucAssertion : core) + { + if (ucAssertion != skip && removed.find(ucAssertion) == removed.end()) + { + Node assertionAfterExpansion = expandDefinitions(ucAssertion); + coreChecker->assertFormula(assertionAfterExpansion); + } + } + Result r; + try + { + r = coreChecker->checkSat(); + } + catch (...) + { + throw; + } + + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + removed.insert(skip); + } + else if (r.asSatisfiabilityResult().isUnknown()) + { + Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core " + "due to " + "unknown result."; + } + } + + if (removed.empty()) + { + return core; + } + else + { + std::vector newUcAssertions; + for (const Node& n : core) + { + if (removed.find(n) == removed.end()) + { + newUcAssertions.push_back(n); + } + } + + return newUcAssertions; + } +} + +void SmtEngine::checkUnsatCore() +{ + Assert(d_env->getOptions().smt.unsatCores) + << "cannot check unsat core if unsat cores are turned off"; + + Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; + UnsatCore core = getUnsatCore(); + + // initialize the core checker + std::unique_ptr coreChecker; + initializeSubsolver(coreChecker, *d_env.get()); + coreChecker->getOptions().smt.checkUnsatCores = false; + // disable all proof options + coreChecker->getOptions().smt.produceProofs = false; + coreChecker->getOptions().smt.checkProofs = false; + + // set up separation logic heap if necessary + TypeNode sepLocType, sepDataType; + if (getSepHeapTypes(sepLocType, sepDataType)) + { + coreChecker->declareSepHeap(sepLocType, sepDataType); + } + + Notice() << "SmtEngine::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 + << ", expanded to " << assertionAfterExpansion << "\n"; + coreChecker->assertFormula(assertionAfterExpansion); + } + Result r; + try + { + r = coreChecker->checkSat(); + } + catch (...) + { + throw; + } + Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; + if (r.asSatisfiabilityResult().isUnknown()) + { + Warning() + << "SmtEngine::checkUnsatCore(): could not check core result unknown." + << std::endl; + } + else if (r.asSatisfiabilityResult().isSat()) + { + InternalError() + << "SmtEngine::checkUnsatCore(): produced core was satisfiable."; + } +} + +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. + Assert(al != nullptr) + << "don't have an assertion list to check in SmtEngine::checkModel()"; + + TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); + + Notice() << "SmtEngine::checkModel(): generating model" << endl; + TheoryModel* m = getAvailableModel("check model"); + Assert(m != nullptr); + + // check the model with the theory engine for debugging + if (options::debugCheckModels()) + { + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->checkTheoryAssertionsWithModel(hardFailure); + } + + // check the model with the check models utility + Assert(d_checkModels != nullptr); + d_checkModels->checkModel(m, al, hardFailure); +} + +UnsatCore SmtEngine::getUnsatCore() +{ + Trace("smt") << "SMT getUnsatCore()" << std::endl; + SmtScope smts(this); + finishInit(); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetUnsatCore(d_env->getDumpOut()); + } + return getUnsatCoreInternal(); +} + +void SmtEngine::getRelevantInstantiationTermVectors( + std::map& insts, bool getDebugInfo) +{ + Assert(d_state->getMode() == SmtMode::UNSAT); + // generate with new proofs + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + Assert(pe->getProof() != nullptr); + std::shared_ptr pfn = + d_pfManager->getFinalProof(pe->getProof(), *d_asserts); + d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo); +} + +std::string SmtEngine::getProof() +{ + Trace("smt") << "SMT getProof()\n"; + SmtScope smts(this); + finishInit(); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetProof(d_env->getDumpOut()); + } + if (!d_env->getOptions().smt.produceProofs) + { + throw ModalException("Cannot get a proof when proof option is off."); + } + if (d_state->getMode() != SmtMode::UNSAT) + { + throw RecoverableModalException( + "Cannot get a proof unless immediately preceded by " + "UNSAT/ENTAILED response."); + } + // the prop engine has the proof of false + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + Assert(pe->getProof() != nullptr); + Assert(d_pfManager); + std::ostringstream ss; + d_pfManager->printProof(ss, pe->getProof(), *d_asserts); + return ss.str(); +} + +void SmtEngine::printInstantiations(std::ostream& out) +{ + SmtScope smts(this); + finishInit(); + QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); + + // First, extract and print the skolemizations + bool printed = false; + bool reqNames = !d_env->getOptions().printer.printInstFull; + // only print when in list mode + if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST) + { + std::map> sks; + qe->getSkolemTermVectors(sks); + for (const std::pair>& s : sks) + { + Node name; + if (!qe->getNameForQuant(s.first, name, reqNames)) + { + // did not have a name and we are only printing formulas with names + continue; + } + SkolemList slist(name, s.second); + out << slist; + printed = true; + } + } + + // Second, extract and print the instantiations + std::map rinsts; + if (d_env->getOptions().smt.produceProofs + && (!d_env->getOptions().smt.unsatCores + || d_env->getOptions().smt.unsatCoresMode + == options::UnsatCoresMode::FULL_PROOF) + && getSmtMode() == SmtMode::UNSAT) + { + // minimize instantiations based on proof manager + getRelevantInstantiationTermVectors(rinsts, + options::dumpInstantiationsDebug()); + } + else + { + std::map>> insts; + getInstantiationTermVectors(insts); + for (const std::pair>>& i : insts) + { + // convert to instantiation list + Node q = i.first; + InstantiationList& ilq = rinsts[q]; + ilq.initialize(q); + for (const std::vector& ii : i.second) + { + ilq.d_inst.push_back(InstantiationVec(ii)); + } + } + } + for (std::pair& i : rinsts) + { + if (i.second.d_inst.empty()) + { + // no instantiations, skip + continue; + } + Node name; + if (!qe->getNameForQuant(i.first, name, reqNames)) + { + // did not have a name and we are only printing formulas with names + continue; + } + // must have a name + if (d_env->getOptions().printer.printInstMode + == options::PrintInstMode::NUM) + { + out << "(num-instantiations " << name << " " << i.second.d_inst.size() + << ")" << std::endl; + } + else + { + // take the name + i.second.d_quant = name; + Assert(d_env->getOptions().printer.printInstMode + == options::PrintInstMode::LIST); + out << i.second; + } + printed = true; + } + // if we did not print anything, we indicate this + if (!printed) + { + out << "none" << std::endl; + } +} + +void SmtEngine::getInstantiationTermVectors( + std::map>>& insts) +{ + SmtScope smts(this); + finishInit(); + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiationTermVectors"); + // get the list of all instantiations + qe->getInstantiationTermVectors(insts); +} + +bool SmtEngine::getSynthSolutions(std::map& solMap) +{ + SmtScope smts(this); + finishInit(); + return d_sygusSolver->getSynthSolutions(solMap); +} + +Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) +{ + SmtScope smts(this); + finishInit(); + const LogicInfo& logic = getLogicInfo(); + if (!logic.isPure(THEORY_ARITH) && strict) + { + Warning() << "Unexpected logic for quantifier elimination " << logic + << endl; + } + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); +} + +bool SmtEngine::getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol) +{ + SmtScope smts(this); + finishInit(); + std::vector axioms = getExpandedAssertions(); + bool success = + d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol); + // notify the state of whether the get-interpol call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetInterpol(success); + return success; +} + +bool SmtEngine::getInterpol(const Node& conj, Node& interpol) +{ + TypeNode grammarType; + return getInterpol(conj, grammarType, interpol); +} + +bool SmtEngine::getAbduct(const Node& conj, + const TypeNode& grammarType, + Node& abd) +{ + SmtScope smts(this); + finishInit(); + std::vector axioms = getExpandedAssertions(); + bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd); + // notify the state of whether the get-abduct call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetAbduct(success); + return success; +} + +bool SmtEngine::getAbduct(const Node& conj, Node& abd) +{ + TypeNode grammarType; + return getAbduct(conj, grammarType, abd); +} + +void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) +{ + SmtScope smts(this); + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas"); + qe->getInstantiatedQuantifiedFormulas(qs); +} + +void SmtEngine::getInstantiationTermVectors( + Node q, std::vector>& tvecs) +{ + SmtScope smts(this); + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiationTermVectors"); + qe->getInstantiationTermVectors(q, tvecs); +} + +std::vector SmtEngine::getAssertions() +{ + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetAssertions(d_env->getDumpOut()); + } + Trace("smt") << "SMT getAssertions()" << endl; + if (!d_env->getOptions().smt.produceAssertions) + { + const char* msg = + "Cannot query the current assertion list when not in " + "produce-assertions mode."; + throw ModalException(msg); + } + return getAssertionsInternal(); +} + +void SmtEngine::getDifficultyMap(std::map& dmap) +{ + Trace("smt") << "SMT getDifficultyMap()\n"; + SmtScope smts(this); + finishInit(); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetDifficulty(d_env->getDumpOut()); + } + if (!d_env->getOptions().smt.produceDifficulty) + { + throw ModalException( + "Cannot get difficulty when difficulty option is off."); + } + // the prop engine has the proof of false + Assert(d_pfManager); + // get difficulty map from theory engine first + TheoryEngine* te = getTheoryEngine(); + te->getDifficultyMap(dmap); + // then ask proof manager to translate dmap in terms of the input + d_pfManager->translateDifficultyMap(dmap, *d_asserts); +} + +void SmtEngine::push() +{ + SmtScope smts(this); + finishInit(); + d_state->doPendingPops(); + Trace("smt") << "SMT push()" << endl; + d_smtSolver->processAssertions(*d_asserts); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdPush(d_env->getDumpOut()); + } + d_state->userPush(); +} + +void SmtEngine::pop() +{ + SmtScope smts(this); + finishInit(); + Trace("smt") << "SMT pop()" << endl; + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdPop(d_env->getDumpOut()); + } + d_state->userPop(); + + // Clear out assertion queues etc., in case anything is still in there + d_asserts->clearCurrent(); + // clear the learned literals from the preprocessor + d_pp->clearLearnedLiterals(); + + Trace("userpushpop") << "SmtEngine: 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() +{ + SmtScope smts(this); + + if (!d_state->isFullyInited()) + { + // We're still in Start Mode, nothing asserted yet, do nothing. + // (see solver execution modes in the SMT-LIB standard) + Assert(getContext()->getLevel() == 0); + Assert(getUserContext()->getLevel() == 0); + getDumpManager()->resetAssertions(); + return; + } + + Trace("smt") << "SMT resetAssertions()" << endl; + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdResetAssertions(d_env->getDumpOut()); + } + + d_asserts->clearCurrent(); + d_state->notifyResetAssertions(); + getDumpManager()->resetAssertions(); + // push the state to maintain global context around everything + d_state->setup(); + + // reset SmtSolver, which will construct a new prop engine + d_smtSolver->resetAssertions(); +} + +void SmtEngine::interrupt() +{ + if (!d_state->isFullyInited()) + { + return; + } + d_smtSolver->interrupt(); +} + +void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) +{ + if (cumulative) + { + d_env->d_options.base.cumulativeResourceLimit = units; + } + else + { + d_env->d_options.base.perCallResourceLimit = units; + } +} +void SmtEngine::setTimeLimit(uint64_t millis) +{ + d_env->d_options.base.perCallMillisecondLimit = millis; +} + +unsigned long SmtEngine::getResourceUsage() const +{ + return getResourceManager()->getResourceUsage(); +} + +unsigned long SmtEngine::getTimeUsage() const +{ + return getResourceManager()->getTimeUsage(); +} + +unsigned long SmtEngine::getResourceRemaining() const +{ + return getResourceManager()->getResourceRemaining(); +} + +NodeManager* SmtEngine::getNodeManager() const +{ + return d_env->getNodeManager(); +} + +void SmtEngine::printStatisticsSafe(int fd) const +{ + d_env->getStatisticsRegistry().printSafe(fd); +} + +void SmtEngine::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) +{ + Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; + + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdSetOption(d_env->getDumpOut(), key, value); + } + + if (key == "command-verbosity") + { + size_t fstIndex = value.find(" "); + size_t sndIndex = value.find(" ", fstIndex + 1); + if (sndIndex == std::string::npos) + { + string c = value.substr(1, fstIndex - 1); + int v = + std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1)); + if (v < 0 || v > 2) + { + throw OptionException("command-verbosity must be 0, 1, or 2"); + } + d_commandVerbosity[c] = v; + return; + } + throw OptionException( + "command-verbosity value must be a tuple (command-name integer)"); + } + + if (value.find(" ") != std::string::npos) + { + throw OptionException("bad value for :" + key); + } + + std::string optionarg = value; + options::set(getOptions(), key, optionarg); +} + +void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } + +bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } + +std::string SmtEngine::getOption(const std::string& key) const +{ + NodeManager* nm = d_env->getNodeManager(); + + Trace("smt") << "SMT getOption(" << key << ")" << endl; + + if (key.find("command-verbosity:") == 0) + { + auto it = + d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); + if (it != d_commandVerbosity.end()) + { + return std::to_string(it->second); + } + it = d_commandVerbosity.find("*"); + if (it != d_commandVerbosity.end()) + { + return std::to_string(it->second); + } + return "2"; + } + + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key); + } + + if (key == "command-verbosity") + { + vector result; + Node defaultVerbosity; + 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 + Node name = nm->mkBoundVar(verb.first, nm->integerType()); + Node value = nm->mkConst(Rational(verb.second)); + if (verb.first == "*") + { + // put the default at the end of the SExpr + defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value); + } + else + { + result.push_back(nm->mkNode(Kind::SEXPR, name, value)); + } + } + // ensure the default is always listed + if (defaultVerbosity.isNull()) + { + defaultVerbosity = nm->mkNode(Kind::SEXPR, + nm->mkBoundVar("*", nm->integerType()), + nm->mkConst(Rational(2))); + } + result.push_back(defaultVerbosity); + return nm->mkNode(Kind::SEXPR, result).toString(); + } + + return options::get(getOptions(), key); +} + +Options& SmtEngine::getOptions() { return d_env->d_options; } + +const Options& SmtEngine::getOptions() const { return d_env->getOptions(); } + +ResourceManager* SmtEngine::getResourceManager() const +{ + return d_env->getResourceManager(); +} + +DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); } + +const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); } + +OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } + +theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } + +} // namespace cvc5 diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h new file mode 100644 index 000000000..92fe30fa1 --- /dev/null +++ b/src/smt/solver_engine.h @@ -0,0 +1,1124 @@ +/****************************************************************************** + * Top contributors (to current version): + + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * SmtEngine: the main public entry point of libcvc5. + */ + +#include "cvc5_public.h" + +#ifndef CVC5__SMT_ENGINE_H +#define CVC5__SMT_ENGINE_H + +#include +#include +#include +#include + +#include "context/cdhashmap_forward.h" +#include "cvc5_export.h" +#include "options/options.h" +#include "smt/output_manager.h" +#include "smt/smt_mode.h" +#include "theory/logic_info.h" +#include "util/result.h" + +namespace cvc5 { + +template +class NodeTemplate; +typedef NodeTemplate Node; +typedef NodeTemplate TNode; +class TypeNode; + +class Env; +class NodeManager; +class TheoryEngine; +class UnsatCore; +class StatisticsRegistry; +class Printer; +class ResourceManager; +struct InstantiationList; + +/* -------------------------------------------------------------------------- */ + +namespace api { +class Solver; +} // namespace api + +/* -------------------------------------------------------------------------- */ + +namespace context { +class Context; +class UserContext; +} // namespace context + +/* -------------------------------------------------------------------------- */ + +namespace preprocessing { +class PreprocessingPassContext; +} + +/* -------------------------------------------------------------------------- */ + +namespace prop { +class PropEngine; +} // namespace prop + +/* -------------------------------------------------------------------------- */ + +namespace smt { +/** Utilities */ +class SmtEngineState; +class AbstractValues; +class Assertions; +class DumpManager; +class ResourceOutListener; +class SmtNodeManagerListener; +class OptionsManager; +class Preprocessor; +class CheckModels; +/** Subsolvers */ +class SmtSolver; +class SygusSolver; +class AbductionSolver; +class InterpolationSolver; +class QuantElimSolver; + +struct SmtEngineStatistics; +class SmtScope; +class PfManager; +class UnsatCoreManager; + +} // namespace smt + +/* -------------------------------------------------------------------------- */ + +namespace theory { +class TheoryModel; +class Rewriter; +class QuantifiersEngine; +} // namespace theory + +/* -------------------------------------------------------------------------- */ + +class CVC5_EXPORT SmtEngine +{ + friend class ::cvc5::api::Solver; + friend class ::cvc5::smt::SmtEngineState; + friend class ::cvc5::smt::SmtScope; + + /* ....................................................................... */ + public: + /* ....................................................................... */ + + /** + * 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. + */ + SmtEngine(NodeManager* nm, const Options* optr = nullptr); + /** Destruct the SMT engine. */ + ~SmtEngine(); + + //--------------------------------------------- concerning the state + + /** + * This is the main initialization procedure of the SmtEngine. + * + * 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 + * assertions and queries are made). + * + * Internally, this creates the theory engine, prop engine, decision engine, + * and other utilities whose initialization depends on the final set of + * 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 + * to simplify() is issued, a scope is pushed, etc. + */ + void finishInit(); + /** + * Return true if this SmtEngine is fully initialized (post-construction) + * by the above call. + */ + bool isFullyInited() const; + /** + * Return true if a checkEntailed() or checkSatisfiability() has been made. + */ + bool isQueryMade() const; + /** Return the user context level. */ + size_t getNumUserLevels() const; + /** Return the current mode of the solver. */ + SmtMode getSmtMode() const; + /** + * Whether the SmtMode allows for get-value, get-model, get-assignment, etc. + * This is equivalent to: + * getSmtMode()==SmtMode::SAT || getSmtMode()==SmtMode::SAT_UNKNOWN + */ + bool isSmtModeSat() const; + /** + * Returns the most recent result of checkSat/checkEntailed or + * (set-info :status). + */ + Result getStatusOfLastCommand() const; + //--------------------------------------------- end concerning the state + + /** + * Set the logic of the script. + * @throw ModalException, LogicException + */ + void setLogic(const std::string& logic); + + /** + * Set the logic of the script. + * @throw ModalException, LogicException + */ + void setLogic(const char* logic); + + /** + * Set the logic of the script. + * @throw ModalException + */ + void setLogic(const LogicInfo& logic); + + /** Get the logic information currently set. */ + const LogicInfo& getLogicInfo() const; + + /** Get the logic information set by the user. */ + LogicInfo getUserLogicInfo() const; + + /** + * Set information about the script executing. + */ + void setInfo(const std::string& key, const std::string& value); + + /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */ + bool isValidGetInfoFlag(const std::string& key) const; + + /** Query information about the SMT environment. */ + std::string getInfo(const std::string& key) const; + + /** + * Set an aspect of the current SMT execution environment. + * @throw OptionException, ModalException + */ + void setOption(const std::string& key, const std::string& value); + + /** 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 + * --sygus-abduct. + */ + void setIsInternalSubsolver(); + /** Is this an internal subsolver? */ + bool isInternalSubsolver() const; + + /** + * Block the current model. Can be called only if immediately preceded by + * a SAT or INVALID query. Only permitted if produce-models is on, and the + * block-models option is set to a mode other than "none". + * + * This adds an assertion to the assertion stack that blocks the current + * model based on the current options configured by cvc5. + * + * The return value has the same meaning as that of assertFormula. + */ + Result blockModel(); + + /** + * Block the current model values of (at least) the values in exprs. + * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query. + * Only permitted if produce-models is on, and the block-models option is set + * to a mode other than "none". + * + * This adds an assertion to the assertion stack of the form: + * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn))) + * where M0 ... Mn are the current model values of exprs[0] ... exprs[n]. + * + * The return value has the same meaning as that of assertFormula. + */ + Result blockModelValues(const std::vector& exprs); + + /** + * Declare heap. For smt2 inputs, this is called when the command + * (declare-heap (locT datat)) is invoked by the user. This sets locT as the + * location type and dataT is the data type for the heap. This command should + * be executed only once, and must be invoked before solving separation logic + * inputs. + */ + void declareSepHeap(TypeNode locT, TypeNode dataT); + + /** + * Get the separation heap types, which extracts which types were passed to + * the method above. + * + * @return true if the separation logic heap types have been declared. + */ + bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT); + + /** When using separation logic, obtain the expression for the heap. */ + Node getSepHeapExpr(); + + /** When using separation logic, obtain the expression for nil. */ + Node getSepNilExpr(); + + /** + * Get an aspect of the current SMT execution environment. + * @throw OptionException + */ + std::string getOption(const std::string& key) const; + + /** + * Define function func in the current context to be: + * (lambda (formals) formula) + * This adds func to the list of defined functions, which indicates that + * all occurrences of func should be expanded during expandDefinitions. + * + * @param func a variable of function type that expects the arguments in + * formal + * @param formals a list of BOUND_VARIABLE expressions + * @param formula The body of the function, must not contain func + * @param global True if this definition is global (i.e. should persist when + * popping the user context) + */ + void defineFunction(Node func, + const std::vector& formals, + Node formula, + bool global = false); + + /** + * Define functions recursive + * + * For each i, this constrains funcs[i] in the current context to be: + * (lambda (formals[i]) formulas[i]) + * where formulas[i] may contain variables from funcs. Unlike defineFunction + * above, we do not add funcs[i] to the set of defined functions. Instead, + * we consider funcs[i] to be a free uninterpreted function, and add: + * forall formals[i]. f(formals[i]) = formulas[i] + * to the set of assertions in the current context. + * This method expects input such that for each i: + * - func[i] : a variable of function type that expects the arguments in + * formals[i], and + * - formals[i] : a list of BOUND_VARIABLE expressions. + * + * @param global True if this definition is global (i.e. should persist when + * popping the user context) + */ + void defineFunctionsRec(const std::vector& funcs, + const std::vector>& formals, + const std::vector& formulas, + bool global = false); + /** + * Define function recursive + * Same as above, but for a single function. + */ + void defineFunctionRec(Node func, + const std::vector& formals, + Node formula, + bool global = false); + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false if + * immediately determined to be inconsistent. Note this formula will + * be included in the unsat core when applicable. + * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException + */ + Result assertFormula(const Node& formula); + + /** + * Reduce an unsatisfiable core to make it minimal. + */ + std::vector reduceUnsatCore(const std::vector& core); + + /** + * Check if a given (set of) expression(s) is entailed with respect to the + * current set of assertions. We check this by asserting the negation of + * the (big AND over the) given (set of) expression(s). + * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result. + * + * @throw Exception + */ + Result checkEntailed(const Node& assumption); + Result checkEntailed(const std::vector& assumptions); + + /** + * Assert a formula (if provided) to the current context and call + * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result. + * + * @throw Exception + */ + Result checkSat(); + Result checkSat(const Node& assumption); + Result checkSat(const std::vector& assumptions); + + /** + * Returns a set of so-called "failed" assumptions. + * + * The returned set is a subset of the set of assumptions of a previous + * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability + * with this set of failed assumptions still produces an unsat answer. + * + * Note that the returned set of failed assumptions is not necessarily + * minimal. + */ + std::vector getUnsatAssumptions(void); + + /*---------------------------- sygus commands ---------------------------*/ + + /** + * Add sygus variable declaration. + * + * Declared SyGuS variables may be used in SyGuS constraints, in which they + * are assumed to be universally quantified. + * + * In SyGuS semantics, declared functions are treated in the same manner as + * declared variables, i.e. as universally quantified (function) variables + * which can occur in the SyGuS constraints that compose the conjecture to + * which a function is being synthesized. Thus declared functions should use + * this method as well. + */ + void declareSygusVar(Node var); + + /** + * Add a function-to-synthesize declaration. + * + * The given sygusType may not correspond to the actual function type of func + * but to a datatype encoding the syntax restrictions for the + * function-to-synthesize. In this case this information is stored to be used + * during solving. + * + * vars contains the arguments of the function-to-synthesize. These variables + * are also stored to be used during solving. + * + * isInv determines whether the function-to-synthesize is actually an + * invariant. This information is necessary if we are dumping a command + * corresponding to this declaration, so that it can be properly printed. + */ + void declareSynthFun(Node func, + TypeNode sygusType, + bool isInv, + const std::vector& vars); + /** + * Same as above, without a sygus type. + */ + void declareSynthFun(Node func, bool isInv, const std::vector& vars); + + /** + * Add a regular sygus constraint or assumption. + * @param n The formula + * @param isAssume True if n is an assumption. + */ + void assertSygusConstraint(Node n, bool isAssume = false); + + /** + * Add an invariant constraint. + * + * Invariant constraints are not explicitly declared: they are given in terms + * of the invariant-to-synthesize, the pre condition, transition relation and + * post condition. The actual constraint is built based on the inputs of these + * place holder predicates : + * + * PRE(x) -> INV(x) + * INV() ^ TRANS(x, x') -> INV(x') + * INV(x) -> POST(x) + * + * The regular and primed variables are retrieved from the declaration of the + * invariant-to-synthesize. + */ + void assertSygusInvConstraint(Node inv, Node pre, Node trans, Node post); + /** + * Assert a synthesis conjecture to the current context and call + * check(). Returns sat, unsat, or unknown result. + * + * The actual synthesis conjecture is built based on the previously + * communicated information to this module (universal variables, defined + * functions, functions-to-synthesize, and which constraints compose it). The + * built conjecture is a higher-order formula of the form + * + * exists f1...fn . forall v1...vm . F + * + * in which f1...fn are the functions-to-synthesize, v1...vm are the declared + * universal variables and F is the set of declared constraints. + * + * @throw Exception + */ + Result checkSynth(); + + /*------------------------- end of sygus commands ------------------------*/ + + /** + * Declare pool whose initial value is the terms in initValue. A pool is + * a variable of type (Set T) that is used in quantifier annotations and does + * not occur in constraints. + * + * @param p The pool to declare, which should be a variable of type (Set T) + * for some type T. + * @param initValue The initial value of p, which should be a vector of terms + * of type T. + */ + void declarePool(const Node& p, const std::vector& initValue); + /** + * Simplify a formula without doing "much" work. Does not involve + * the SAT Engine in the simplification, but uses the current + * definitions, assertions, and the current partial model, if one + * has been constructed. It also involves theory normalization. + * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException + * + * @todo (design) is this meant to give an equivalent or an + * equisatisfiable formula? + */ + Node simplify(const Node& e); + + /** + * Expand the definitions in a term or formula. + * + * @param n The node to expand + * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException + */ + Node expandDefinitions(const Node& n); + + /** + * 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. + * + * @throw ModalException, TypeCheckingException, LogicException, + * UnsafeInterruptException + */ + Node getValue(const Node& e) const; + + /** + * Same as getValue but for a vector of expressions + */ + std::vector getValues(const std::vector& exprs) const; + + /** + * @return the domain elements for uninterpreted sort tn. + */ + std::vector getModelDomainElements(TypeNode tn) const; + + /** + * @return true if v is a model core symbol + */ + bool isModelCoreSymbol(Node v); + + /** + * Get a model (only if immediately preceded by an SAT or unknown query). + * Only permitted if the model option is on. + * + * @param declaredSorts The sorts to print in the model + * @param declaredFuns The free constants to print in the model. A subset + * of these may be printed based on isModelCoreSymbol. + * @return the string corresponding to the model. If the output language is + * smt2, then this corresponds to a response to the get-model command. + */ + std::string getModel(const std::vector& declaredSorts, + const std::vector& declaredFuns); + + /** print instantiations + * + * Print all instantiations for all quantified formulas on out, + * returns true if at least one instantiation was printed. The type of output + * (list, num, etc.) is determined by printInstMode. + */ + void printInstantiations(std::ostream& out); + /** + * Print the current proof. This method should be called after an UNSAT + * response. It gets the proof of false from the PropEngine and passes + * it to the ProofManager, which post-processes the proof and prints it + * in the proper format. + */ + void printProof(); + + /** + * Get synth solution. + * + * This method returns true if we are in a state immediately preceded by + * a successful call to checkSynth. + * + * This method adds entries to solMap that map functions-to-synthesize with + * their solutions, for all active conjectures. This should be called + * immediately after the solver answers unsat for sygus input. + * + * Specifically, given a sygus conjecture of the form + * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn ) + * where x1...xn are second order bound variables, we map each xi to + * lambda term in solMap such that + * forall y1...yn. P( solMap[x1]...solMap[xn], y1...yn ) + * is a valid formula. + */ + bool getSynthSolutions(std::map& solMap); + + /** + * Do quantifier elimination. + * + * This function takes as input a quantified formula q + * of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free + * formula in a logic that supports quantifier elimination. + * Currently, the only logics supported by quantifier + * elimination is LRA and LIA. + * + * This function returns a formula ret such that, given + * the current set of formulas A asserted to this SmtEngine : + * + * If doFull = true, then + * - ( A ^ q ) and ( A ^ ret ) are equivalent + * - ret is quantifier-free formula containing + * only free variables in y1...yn. + * + * If doFull = false, then + * - (A ^ q) => (A ^ ret) if Q is forall or + * (A ^ ret) => (A ^ q) if Q is exists, + * - ret is quantifier-free formula containing + * only free variables in y1...yn, + * - If Q is exists, let A^Q_n be the formula + * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n + * where for each i=1,...n, formula ret^Q_i + * is the result of calling doQuantifierElimination + * for q with the set of assertions A^Q_{i-1}. + * Similarly, if Q is forall, then let A^Q_n be + * A ^ ret^Q_1 ^ ... ^ ret^Q_n + * where ret^Q_i is the same as above. + * In either case, we have that ret^Q_j will + * eventually be true or false, for some finite j. + * + * The former feature is quantifier elimination, and + * is run on invocations of the smt2 extended command get-qe. + * The latter feature is referred to as partial quantifier + * elimination, and is run on invocations of the smt2 + * extended command get-qe-disjunct, which can be used + * for incrementally computing the result of a + * quantifier elimination. + * + * The argument strict is whether to output + * warnings, such as when an unexpected logic is used. + * + * throw@ Exception + */ + Node getQuantifierElimination(Node q, bool doFull, bool strict = true); + + /** + * This method asks this SMT engine to find an interpolant with respect to + * the current assertion stack (call it A) and the conjecture (call it B). If + * this method returns true, then interpolant is set to a formula I such that + * A ^ ~I and I ^ ~B are both unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shapes of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol); + + /** Same as above, but without user-provided grammar restrictions */ + bool getInterpol(const Node& conj, Node& interpol); + + /** + * This method asks this SMT engine to find an abduct with respect to the + * current assertion stack (call it A) and the conjecture (call it B). + * If this method returns true, then abd is set to a formula C such that + * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shape of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd); + + /** Same as above, but without user-provided grammar restrictions */ + bool getAbduct(const Node& conj, Node& abd); + + /** + * Get list of quantified formulas that were instantiated on the last call + * to check-sat. + */ + void getInstantiatedQuantifiedFormulas(std::vector& qs); + + /** + * Get instantiation term vectors for quantified formula q. + * + * This method is similar to above, but in the example above, we return the + * (vectors of) terms t1, ..., tn instead. + * + * Notice that these are not guaranteed to come in the same order as the + * instantiation lemmas above. + */ + void getInstantiationTermVectors(Node q, + std::vector>& tvecs); + /** + * As above but only the instantiations that were relevant for the + * refutation. + */ + void getRelevantInstantiationTermVectors( + std::map& insts, bool getDebugInfo = false); + /** + * Get instantiation term vectors, which maps each instantiated quantified + * formula to the list of instantiations for that quantified formula. This + * list is minimized if proofs are enabled, and this call is immediately + * preceded by an UNSAT or ENTAILED query + */ + void getInstantiationTermVectors( + std::map>>& insts); + + /** + * Get an unsatisfiable core (only if immediately preceded by an UNSAT or + * ENTAILED query). Only permitted if cvc5 was built with unsat-core support + * and produce-unsat-cores is on. + */ + UnsatCore getUnsatCore(); + + /** + * Get a refutation proof (only if immediately preceded by an UNSAT or + * ENTAILED query). Only permitted if cvc5 was built with proof support and + * the proof option is on. */ + std::string getProof(); + + /** + * Get the current set of assertions. Only permitted if the + * SmtEngine is set to operate interactively. + */ + std::vector getAssertions(); + + /** + * Get difficulty map, which populates dmap, mapping input assertions + * to a value that estimates their difficulty for solving the current problem. + */ + void getDifficultyMap(std::map& dmap); + + /** + * Push a user-level context. + * throw@ ModalException, LogicException, UnsafeInterruptException + */ + void push(); + + /** + * Pop a user-level context. Throws an exception if nothing to pop. + * @throw ModalException + */ + void pop(); + + /** Reset all assertions, global declarations, etc. */ + void resetAssertions(); + + /** + * Interrupt a running query. This can be called from another thread + * or from a signal handler. Throws a ModalException if the SmtEngine + * isn't currently in a query. + * + * @throw ModalException + */ + void interrupt(); + + /** + * Set a resource limit for SmtEngine 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 + * versions of cvc5 (as may the number of conflicts required, anyway), + * and it might even be different between instances of the same version + * of cvc5 on different platforms. + * + * A cumulative and non-cumulative (per-call) resource limit can be + * set at the same time. A call to setResourceLimit() with + * 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 + * at the same time. + * + * When an SmtEngine is first created, it has no time or resource + * limits. + * + * Currently, these limits only cause the SmtEngine 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 + * 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. + * + * 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. + * + * Note that the per-call timer only ticks away when one of the + * SmtEngine'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 + * limits. + * + * Currently, these limits only cause the SmtEngine 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 millis the time limit in milliseconds, or 0 for no limit + */ + void setTimeLimit(uint64_t millis); + + /** + * Get the current resource usage count for this SmtEngine. 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. */ + unsigned long getTimeUsage() const; + + /** + * Get the remaining resources that can be consumed by this SmtEngine + * according to the currently-set cumulative resource limit. If there + * is not a cumulative resource limit set, this function throws a + * ModalException. + * + * @throw ModalException + */ + unsigned long getResourceRemaining() const; + + /** Permit access to the underlying NodeManager. */ + NodeManager* getNodeManager() const; + + /** + * Print statistics from the statistics registry in the env object owned by + * this SmtEngine. 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 + * time. Internally prints the diff and then stores a snapshot for the next + * call. + */ + void printStatisticsDiff() const; + + /** Get the options object (const and non-const versions) */ + Options& getOptions(); + const Options& getOptions() const; + + /** Get a pointer to the UserContext owned by this SmtEngine. */ + context::UserContext* getUserContext(); + + /** Get a pointer to the Context owned by this SmtEngine. */ + context::Context* getContext(); + + /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ + TheoryEngine* getTheoryEngine(); + + /** Get a pointer to the PropEngine owned by this SmtEngine. */ + prop::PropEngine* getPropEngine(); + + /** Get the resource manager of this SMT engine */ + ResourceManager* getResourceManager() const; + + /** Permit access to the underlying dump manager. */ + smt::DumpManager* getDumpManager(); + + /** Get the printer used by this SMT engine */ + const Printer& getPrinter() const; + + /** Get the output manager for this SMT engine */ + OutputManager& getOutputManager(); + + /** Get a pointer to the Rewriter owned by this SmtEngine. */ + theory::Rewriter* getRewriter(); + /** + * Get expanded assertions. + * + * Return the set of assertions, after expanding definitions. + */ + std::vector getExpandedAssertions(); + + /** + * !!!!! temporary, until the environment is passsed to all classes that + * require it. + */ + Env& getEnv(); + /* ....................................................................... */ + private: + /* ....................................................................... */ + + // disallow copy/assignment + SmtEngine(const SmtEngine&) = delete; + SmtEngine& operator=(const SmtEngine&) = delete; + + /** Set solver instance that owns this SmtEngine. */ + void setSolver(api::Solver* solver) { d_solver = solver; } + + /** Get a pointer to the (new) PfManager owned by this SmtEngine. */ + smt::PfManager* getPfManager() { return d_pfManager.get(); }; + + /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ + StatisticsRegistry& getStatisticsRegistry(); + + /** + * Internal method to get an unsatisfiable core (only if immediately preceded + * by an UNSAT or ENTAILED query). Only permitted if cvc5 was built with + * unsat-core support and produce-unsat-cores is on. Does not dump the + * command. + */ + UnsatCore getUnsatCoreInternal(); + + /** + * Check that a generated proof checks. This method is the same as printProof, + * but does not print the proof. Like that method, it should be called + * after an UNSAT response. It ensures that a well-formed proof of false + * can be constructed by the combination of the PropEngine and ProofManager. + */ + void checkProof(); + + /** + * Check that an unsatisfiable core is indeed unsatisfiable. + */ + void checkUnsatCore(); + + /** + * Check that a generated Model (via getModel()) actually satisfies + * all user assertions. + */ + void checkModel(bool hardFailure = true); + + /** + * Check that a solution to an interpolation problem is indeed a solution. + * + * The check is made by determining that the assertions imply the solution of + * the interpolation problem (interpol), and the solution implies the goal + * (conj). If these criteria are not met, an internal error is thrown. + */ + void checkInterpol(Node interpol, + const std::vector& easserts, + const Node& conj); + + /** + * This is called by the destructor, 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(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + /** + * Get the (SMT-level) model pointer, if we are in SAT mode. Otherwise, + * return nullptr. + * + * This ensures that the underlying theory model of the SmtSolver maintained + * by this class is currently available, which means that cvc5 is producing + * models, and is in "SAT mode", otherwise a recoverable exception is thrown. + * + * @param c used for giving an error message to indicate the context + * this method was called. + */ + theory::TheoryModel* getAvailableModel(const char* c) const; + /** + * Get available quantifiers engine, which throws a modal exception if it + * does not exist. This can happen if a quantifiers-specific call (e.g. + * getInstantiatedQuantifiedFormulas) is called in a non-quantified logic. + * + * @param c used for giving an error message to indicate the context + * this method was called. + */ + theory::QuantifiersEngine* getAvailableQuantifiersEngine(const char* c) const; + + // --------------------------------------- callbacks from the state + /** + * Notify push pre, which is called just before the user context of the state + * pushes. This processes all pending assertions. + */ + void notifyPushPre(); + /** + * Notify push post, which is called just after the user context of the state + * pushes. This performs a push on the underlying prop engine. + */ + void notifyPushPost(); + /** + * Notify pop pre, which is called just before the user context of the state + * pops. This performs a pop on the underlying prop engine. + */ + void notifyPopPre(); + /** + * Notify post solve pre, which is called once per check-sat query. It + * is triggered when the first d_state.doPendingPops() is issued after the + * check-sat. This method is called before the contexts pop in the method + * doPendingPops. + */ + void notifyPostSolvePre(); + /** + * Same as above, but after contexts are popped. This calls the postsolve + * method of the underlying TheoryEngine. + */ + void notifyPostSolvePost(); + // --------------------------------------- end callbacks from the state + + /** + * Internally handle the setting of a logic. This function should always + * be called when d_logic is updated. + */ + void setLogicInternal(); + + /* + * Check satisfiability (used to check satisfiability and entailment). + */ + Result checkSatInternal(const std::vector& assumptions, + bool isEntailmentCheck); + + /** + * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is + * the function that the formal argument list is for. This method is used + * as a helper function when defining (recursive) functions. + */ + void debugCheckFormals(const std::vector& formals, Node func); + + /** + * Checks whether formula is a valid function body for func whose formal + * argument list is stored in formals. This method is + * used as a helper function when defining (recursive) functions. + */ + void debugCheckFunctionBody(Node formula, + const std::vector& formals, + Node func); + + /** + * Helper method to obtain both the heap and nil from the solver. Returns a + * std::pair where the first element is the heap expression and the second + * element is the nil expression. + */ + std::pair getSepHeapAndNilExpr(); + /** + * Get assertions internal, which is only called after initialization. This + * should be used internally to get the assertions instead of getAssertions + * or getExpandedAssertions, which may trigger initialization and SMT state + * changes. + */ + std::vector getAssertionsInternal(); + /* Members -------------------------------------------------------------- */ + + /** Solver instance that owns this SmtEngine instance. */ + api::Solver* d_solver = nullptr; + + /** + * The environment object, which contains all utilities that are globally + * available to internal code. + */ + std::unique_ptr d_env; + /** + * The state of this SmtEngine, which is responsible for maintaining which + * SMT mode we are in, the contexts, the last result, etc. + */ + std::unique_ptr d_state; + + /** Abstract values */ + std::unique_ptr d_absValues; + /** Assertions manager */ + std::unique_ptr d_asserts; + /** Resource out listener */ + std::unique_ptr d_routListener; + /** Node manager listener */ + std::unique_ptr d_snmListener; + + /** The SMT solver */ + std::unique_ptr d_smtSolver; + + /** + * The utility used for checking models + */ + std::unique_ptr d_checkModels; + + /** + * The proof manager, which manages all things related to checking, + * processing, and printing proofs. + */ + std::unique_ptr d_pfManager; + + /** + * The unsat core manager, which produces unsat cores and related information + * from refutations. */ + std::unique_ptr d_ucManager; + + /** The solver for sygus queries */ + std::unique_ptr d_sygusSolver; + + /** The solver for abduction queries */ + std::unique_ptr d_abductSolver; + /** The solver for interpolation queries */ + std::unique_ptr d_interpolSolver; + /** The solver for quantifier elimination queries */ + std::unique_ptr d_quantElimSolver; + + /** + * The logic set by the user. The actual logic, which may extend the user's + * logic, lives in the Env class. + */ + LogicInfo d_userLogic; + + /** Whether this is an internal subsolver. */ + bool d_isInternalSubsolver; + + /** + * Verbosity of various commands. + */ + std::map d_commandVerbosity; + + /** The statistics class */ + std::unique_ptr d_stats; + + /** the output manager for commands */ + mutable OutputManager d_outMgr; + /** + * The preprocessor. + */ + 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. + */ + std::unique_ptr d_scope; +}; /* class SmtEngine */ + +/* -------------------------------------------------------------------------- */ + +} // namespace cvc5 + +#endif /* CVC5__SMT_ENGINE_H */ 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"