This is in preparation for renaming SmtEngine to SolverEngine.
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
#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"
#include "main/main.h"
#include "smt/command.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
namespace cvc5 {
namespace main {
#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;
#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;
#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 {
#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"
#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"
#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"
#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;
#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"
#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;
#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"
#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"
#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 {
#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;
#include "smt/output_manager.h"
#include "options/base_options.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
namespace cvc5 {
#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;
#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"
#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"
+++ /dev/null
-/******************************************************************************
- * 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<std::string>(
- "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<unsigned long int>::max());
- return toSExpr(ulevel);
- }
- Assert(key == "all-options");
- // get the options, like all-statistics
- std::vector<std::vector<std::string>> res;
- for (const auto& opt: options::getNames())
- {
- res.emplace_back(std::vector<std::string>{opt, options::get(getOptions(), opt)});
- }
- return toSExpr(res);
-}
-
-void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
-{
- for (std::vector<Node>::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<Node>& 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<Node>& 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<Node>& funcs,
- const std::vector<std::vector<Node>>& formals,
- const std::vector<Node>& 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<Node> 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<Node>& formals,
- Node formula,
- bool global)
-{
- std::vector<Node> funcs;
- funcs.push_back(func);
- std::vector<std::vector<Node>> formals_multi;
- formals_multi.push_back(formals);
- std::vector<Node> 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<Node> assump;
- if (!assumption.isNull())
- {
- assump.push_back(assumption);
- }
- return checkSatInternal(assump, false);
-}
-
-Result SmtEngine::checkSat(const std::vector<Node>& 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<Node>() : std::vector<Node>{node},
- true)
- .asEntailmentResult();
-}
-
-Result SmtEngine::checkEntailed(const std::vector<Node>& nodes)
-{
- return checkSatInternal(nodes, true).asEntailmentResult();
-}
-
-Result SmtEngine::checkSatInternal(const std::vector<Node>& 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<Node> 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<Node> res;
- std::vector<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
-{
- std::vector<Node> result;
- for (const Node& e : exprs)
- {
- result.push_back(getValue(e));
- }
- return result;
-}
-
-std::vector<Node> 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<Node> 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<TypeNode>& declaredSorts,
- const std::vector<Node>& 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<Node, Node> 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<Node> 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<Node>& 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<Node> 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<Node, Node> 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<Node> SmtEngine::getAssertionsInternal()
-{
- Assert(d_state->isFullyInited());
- context::CDList<Node>* al = d_asserts->getAssertionList();
- Assert(al != nullptr);
- std::vector<Node> res;
- for (const Node& n : *al)
- {
- res.emplace_back(n);
- }
- return res;
-}
-
-std::vector<Node> SmtEngine::getExpandedAssertions()
-{
- std::vector<Node> 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<ProofNode> 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<ProofNode> pepf;
- if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
- {
- pepf = pe->getRefutation();
- }
- else
- {
- pepf = pe->getProof();
- }
- Assert(pepf != nullptr);
- std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
- std::vector<Node> core;
- d_ucManager->getUnsatCore(pfn, *d_asserts, core);
- if (options::minimalUnsatCores())
- {
- core = reduceUnsatCore(core);
- }
- return UnsatCore(core);
-}
-
-std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
-{
- Assert(options::unsatCores())
- << "cannot reduce unsat core if unsat cores are turned off";
-
- Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl;
- std::unordered_set<Node> removed;
- for (const Node& skip : core)
- {
- std::unique_ptr<SmtEngine> 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<Node> 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<SmtEngine> 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<Node>* 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<Node, InstantiationList>& 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<ProofNode> 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<Node, std::vector<Node>> sks;
- qe->getSkolemTermVectors(sks);
- for (const std::pair<const Node, std::vector<Node>>& 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<Node, InstantiationList> 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<Node, std::vector<std::vector<Node>>> insts;
- getInstantiationTermVectors(insts);
- for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
- {
- // convert to instantiation list
- Node q = i.first;
- InstantiationList& ilq = rinsts[q];
- ilq.initialize(q);
- for (const std::vector<Node>& ii : i.second)
- {
- ilq.d_inst.push_back(InstantiationVec(ii));
- }
- }
- }
- for (std::pair<const Node, InstantiationList>& 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<Node, std::vector<std::vector<Node>>>& insts)
-{
- SmtScope smts(this);
- finishInit();
- QuantifiersEngine* qe =
- getAvailableQuantifiersEngine("getInstantiationTermVectors");
- // get the list of all instantiations
- qe->getInstantiationTermVectors(insts);
-}
-
-bool SmtEngine::getSynthSolutions(std::map<Node, Node>& 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<Node> 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<Node> 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<Node>& qs)
-{
- SmtScope smts(this);
- QuantifiersEngine* qe =
- getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
- qe->getInstantiatedQuantifiedFormulas(qs);
-}
-
-void SmtEngine::getInstantiationTermVectors(
- Node q, std::vector<std::vector<Node>>& tvecs)
-{
- SmtScope smts(this);
- QuantifiersEngine* qe =
- getAvailableQuantifiersEngine("getInstantiationTermVectors");
- qe->getInstantiationTermVectors(q, tvecs);
-}
-
-std::vector<Node> 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<Node, Node>& 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<Node> 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
+++ /dev/null
-/******************************************************************************
- * 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 <map>
-#include <memory>
-#include <string>
-#include <vector>
-
-#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 <bool ref_count> class NodeTemplate;
-typedef NodeTemplate<true> Node;
-typedef NodeTemplate<false> 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<Node>& 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<Node>& 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<Node>& funcs,
- const std::vector<std::vector<Node>>& formals,
- const std::vector<Node>& formulas,
- bool global = false);
- /**
- * Define function recursive
- * Same as above, but for a single function.
- */
- void defineFunctionRec(Node func,
- const std::vector<Node>& 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<Node> reduceUnsatCore(const std::vector<Node>& 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<Node>& 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<Node>& 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<Node> 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<Node>& vars);
- /**
- * Same as above, without a sygus type.
- */
- void declareSynthFun(Node func, bool isInv, const std::vector<Node>& 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<Node>& 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<Node> getValues(const std::vector<Node>& exprs) const;
-
- /**
- * @return the domain elements for uninterpreted sort tn.
- */
- std::vector<Node> 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<TypeNode>& declaredSorts,
- const std::vector<Node>& 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<Node, Node>& 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<Node>& 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<std::vector<Node>>& tvecs);
- /**
- * As above but only the instantiations that were relevant for the
- * refutation.
- */
- void getRelevantInstantiationTermVectors(
- std::map<Node, InstantiationList>& 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<Node, std::vector<std::vector<Node>>>& 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<Node> 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<Node, Node>& 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<Node> 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node, Node> 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<Node> 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<Env> 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<smt::SmtEngineState> d_state;
-
- /** Abstract values */
- std::unique_ptr<smt::AbstractValues> d_absValues;
- /** Assertions manager */
- std::unique_ptr<smt::Assertions> d_asserts;
- /** Resource out listener */
- std::unique_ptr<smt::ResourceOutListener> d_routListener;
- /** Node manager listener */
- std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
-
- /** The SMT solver */
- std::unique_ptr<smt::SmtSolver> d_smtSolver;
-
- /**
- * The utility used for checking models
- */
- std::unique_ptr<smt::CheckModels> d_checkModels;
-
- /**
- * The proof manager, which manages all things related to checking,
- * processing, and printing proofs.
- */
- std::unique_ptr<smt::PfManager> d_pfManager;
-
- /**
- * The unsat core manager, which produces unsat cores and related information
- * from refutations. */
- std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
-
- /** The solver for sygus queries */
- std::unique_ptr<smt::SygusSolver> d_sygusSolver;
-
- /** The solver for abduction queries */
- std::unique_ptr<smt::AbductionSolver> d_abductSolver;
- /** The solver for interpolation queries */
- std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
- /** The solver for quantifier elimination queries */
- std::unique_ptr<smt::QuantElimSolver> 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<std::string, int> d_commandVerbosity;
-
- /** The statistics class */
- std::unique_ptr<smt::SmtEngineStatistics> d_stats;
-
- /** the output manager for commands */
- mutable OutputManager d_outMgr;
- /**
- * The preprocessor.
- */
- std::unique_ptr<smt::Preprocessor> 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<smt::SmtScope> d_scope;
-}; /* class SmtEngine */
-
-/* -------------------------------------------------------------------------- */
-
-} // namespace cvc5
-
-#endif /* CVC5__SMT_ENGINE_H */
#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 {
#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 {
#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"
--- /dev/null
+/******************************************************************************
+ * 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<std::string>(
+ "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<unsigned long int>::max());
+ return toSExpr(ulevel);
+ }
+ Assert(key == "all-options");
+ // get the options, like all-statistics
+ std::vector<std::vector<std::string>> res;
+ for (const auto& opt : options::getNames())
+ {
+ res.emplace_back(
+ std::vector<std::string>{opt, options::get(getOptions(), opt)});
+ }
+ return toSExpr(res);
+}
+
+void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
+{
+ for (std::vector<Node>::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<Node>& 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<Node>& 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<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& 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<Node> 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<Node>& formals,
+ Node formula,
+ bool global)
+{
+ std::vector<Node> funcs;
+ funcs.push_back(func);
+ std::vector<std::vector<Node>> formals_multi;
+ formals_multi.push_back(formals);
+ std::vector<Node> 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<Node> assump;
+ if (!assumption.isNull())
+ {
+ assump.push_back(assumption);
+ }
+ return checkSatInternal(assump, false);
+}
+
+Result SmtEngine::checkSat(const std::vector<Node>& 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<Node>() : std::vector<Node>{node},
+ true)
+ .asEntailmentResult();
+}
+
+Result SmtEngine::checkEntailed(const std::vector<Node>& nodes)
+{
+ return checkSatInternal(nodes, true).asEntailmentResult();
+}
+
+Result SmtEngine::checkSatInternal(const std::vector<Node>& 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<Node> 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<Node> res;
+ std::vector<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
+{
+ std::vector<Node> result;
+ for (const Node& e : exprs)
+ {
+ result.push_back(getValue(e));
+ }
+ return result;
+}
+
+std::vector<Node> 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<Node> 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<TypeNode>& declaredSorts,
+ const std::vector<Node>& 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<Node, Node> 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<Node> 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<Node>& 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<Node> 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<Node, Node> 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<Node> SmtEngine::getAssertionsInternal()
+{
+ Assert(d_state->isFullyInited());
+ context::CDList<Node>* al = d_asserts->getAssertionList();
+ Assert(al != nullptr);
+ std::vector<Node> res;
+ for (const Node& n : *al)
+ {
+ res.emplace_back(n);
+ }
+ return res;
+}
+
+std::vector<Node> SmtEngine::getExpandedAssertions()
+{
+ std::vector<Node> 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<ProofNode> 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<ProofNode> pepf;
+ if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
+ {
+ pepf = pe->getRefutation();
+ }
+ else
+ {
+ pepf = pe->getProof();
+ }
+ Assert(pepf != nullptr);
+ std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
+ std::vector<Node> core;
+ d_ucManager->getUnsatCore(pfn, *d_asserts, core);
+ if (options::minimalUnsatCores())
+ {
+ core = reduceUnsatCore(core);
+ }
+ return UnsatCore(core);
+}
+
+std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
+{
+ Assert(options::unsatCores())
+ << "cannot reduce unsat core if unsat cores are turned off";
+
+ Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl;
+ std::unordered_set<Node> removed;
+ for (const Node& skip : core)
+ {
+ std::unique_ptr<SmtEngine> 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<Node> 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<SmtEngine> 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<Node>* 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<Node, InstantiationList>& 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<ProofNode> 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<Node, std::vector<Node>> sks;
+ qe->getSkolemTermVectors(sks);
+ for (const std::pair<const Node, std::vector<Node>>& 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<Node, InstantiationList> 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<Node, std::vector<std::vector<Node>>> insts;
+ getInstantiationTermVectors(insts);
+ for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
+ {
+ // convert to instantiation list
+ Node q = i.first;
+ InstantiationList& ilq = rinsts[q];
+ ilq.initialize(q);
+ for (const std::vector<Node>& ii : i.second)
+ {
+ ilq.d_inst.push_back(InstantiationVec(ii));
+ }
+ }
+ }
+ for (std::pair<const Node, InstantiationList>& 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<Node, std::vector<std::vector<Node>>>& insts)
+{
+ SmtScope smts(this);
+ finishInit();
+ QuantifiersEngine* qe =
+ getAvailableQuantifiersEngine("getInstantiationTermVectors");
+ // get the list of all instantiations
+ qe->getInstantiationTermVectors(insts);
+}
+
+bool SmtEngine::getSynthSolutions(std::map<Node, Node>& 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<Node> 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<Node> 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<Node>& qs)
+{
+ SmtScope smts(this);
+ QuantifiersEngine* qe =
+ getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
+ qe->getInstantiatedQuantifiedFormulas(qs);
+}
+
+void SmtEngine::getInstantiationTermVectors(
+ Node q, std::vector<std::vector<Node>>& tvecs)
+{
+ SmtScope smts(this);
+ QuantifiersEngine* qe =
+ getAvailableQuantifiersEngine("getInstantiationTermVectors");
+ qe->getInstantiationTermVectors(q, tvecs);
+}
+
+std::vector<Node> 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<Node, Node>& 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<Node> 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
--- /dev/null
+/******************************************************************************
+ * 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 <map>
+#include <memory>
+#include <string>
+#include <vector>
+
+#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 <bool ref_count>
+class NodeTemplate;
+typedef NodeTemplate<true> Node;
+typedef NodeTemplate<false> 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<Node>& 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<Node>& 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<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas,
+ bool global = false);
+ /**
+ * Define function recursive
+ * Same as above, but for a single function.
+ */
+ void defineFunctionRec(Node func,
+ const std::vector<Node>& 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<Node> reduceUnsatCore(const std::vector<Node>& 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<Node>& 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<Node>& 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<Node> 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<Node>& vars);
+ /**
+ * Same as above, without a sygus type.
+ */
+ void declareSynthFun(Node func, bool isInv, const std::vector<Node>& 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<Node>& 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<Node> getValues(const std::vector<Node>& exprs) const;
+
+ /**
+ * @return the domain elements for uninterpreted sort tn.
+ */
+ std::vector<Node> 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<TypeNode>& declaredSorts,
+ const std::vector<Node>& 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<Node, Node>& 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<Node>& 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<std::vector<Node>>& tvecs);
+ /**
+ * As above but only the instantiations that were relevant for the
+ * refutation.
+ */
+ void getRelevantInstantiationTermVectors(
+ std::map<Node, InstantiationList>& 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<Node, std::vector<std::vector<Node>>>& 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<Node> 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<Node, Node>& 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<Node> 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node, Node> 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<Node> 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<Env> 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<smt::SmtEngineState> d_state;
+
+ /** Abstract values */
+ std::unique_ptr<smt::AbstractValues> d_absValues;
+ /** Assertions manager */
+ std::unique_ptr<smt::Assertions> d_asserts;
+ /** Resource out listener */
+ std::unique_ptr<smt::ResourceOutListener> d_routListener;
+ /** Node manager listener */
+ std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
+
+ /** The SMT solver */
+ std::unique_ptr<smt::SmtSolver> d_smtSolver;
+
+ /**
+ * The utility used for checking models
+ */
+ std::unique_ptr<smt::CheckModels> d_checkModels;
+
+ /**
+ * The proof manager, which manages all things related to checking,
+ * processing, and printing proofs.
+ */
+ std::unique_ptr<smt::PfManager> d_pfManager;
+
+ /**
+ * The unsat core manager, which produces unsat cores and related information
+ * from refutations. */
+ std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
+
+ /** The solver for sygus queries */
+ std::unique_ptr<smt::SygusSolver> d_sygusSolver;
+
+ /** The solver for abduction queries */
+ std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+ /** The solver for interpolation queries */
+ std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
+ /** The solver for quantifier elimination queries */
+ std::unique_ptr<smt::QuantElimSolver> 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<std::string, int> d_commandVerbosity;
+
+ /** The statistics class */
+ std::unique_ptr<smt::SmtEngineStatistics> d_stats;
+
+ /** the output manager for commands */
+ mutable OutputManager d_outMgr;
+ /**
+ * The preprocessor.
+ */
+ std::unique_ptr<smt::Preprocessor> 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<smt::SmtScope> d_scope;
+}; /* class SmtEngine */
+
+/* -------------------------------------------------------------------------- */
+
+} // namespace cvc5
+
+#endif /* CVC5__SMT_ENGINE_H */
#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"
#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"
#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"
#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"
#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"
#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"
#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"
#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"
#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 {
#include <vector>
#include "expr/node.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
namespace cvc5 {
namespace theory {
#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"
#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;
#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"
#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"
#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"
#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"
#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"
#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"
#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 {
#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 {
#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"
projects / cvc5.git / commitdiff