--- /dev/null
+/********************* */
+/*! \file env.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 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.\endverbatim
+ **
+ ** \brief Smt Environment, main access to global utilities available to
+ ** internal code
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__SMT__ENV_H
+#define CVC4__SMT__ENV_H
+
+#include <memory>
+
+#include "options/options.h"
+#include "theory/logic_info.h"
+#include "util/sexpr.h"
+#include "util/statistics.h"
+
+namespace CVC4 {
+
+class NodeManager;
+class StatisticsRegistry;
+class ProofNodeManager;
+class Printer;
+class ResourceManager;
+
+namespace context {
+class Context;
+class UserContext;
+} // namespace context
+
+namespace smt {
+class DumpManager;
+}
+
+namespace theory {
+class Rewriter;
+}
+
+/**
+ * The environment class.
+ *
+ * This class lives in the SmtEngine and contains all utilities that are
+ * globally available to all internal code.
+ */
+class Env
+{
+ friend class SmtEngine;
+
+ public:
+ /**
+ * Construct an Env with the given node manager.
+ */
+ Env(NodeManager* nm);
+ /** Destruct the env. */
+ ~Env();
+
+ /* Access to members------------------------------------------------------- */
+ /** Get a pointer to the Context owned by this Env. */
+ context::Context* getContext();
+
+ /** Get a pointer to the UserContext owned by this Env. */
+ context::UserContext* getUserContext();
+
+ /** Get a pointer to the underlying NodeManager. */
+ NodeManager* getNodeManager() const;
+
+ /**
+ * Get the underlying proof node manager. Note since proofs depend on option
+ * initialization, this is only available after the SmtEngine that owns this
+ * environment is initialized, and only non-null if proofs are enabled.
+ */
+ ProofNodeManager* getProofNodeManager();
+
+ /** Get a pointer to the Rewriter owned by this Env. */
+ theory::Rewriter* getRewriter();
+
+ /** Get a pointer to the underlying dump manager. */
+ smt::DumpManager* getDumpManager();
+
+ /** Get the options object (const version only) owned by this Env. */
+ const Options& getOptions() const;
+
+ /** Get the resource manager owned by this Env. */
+ ResourceManager* getResourceManager() const;
+
+ /** Get the logic information currently set. */
+ const LogicInfo& getLogicInfo() const;
+
+ /** Get a pointer to the StatisticsRegistry. */
+ StatisticsRegistry* getStatisticsRegistry();
+
+ /* Option helpers---------------------------------------------------------- */
+
+ /**
+ * Get the current printer based on the current options
+ * @return the current printer
+ */
+ const Printer& getPrinter();
+
+ /**
+ * Get the output stream that --dump=X should print to
+ * @return the output stream
+ */
+ std::ostream& getDumpOut();
+
+ private:
+ /* Private initialization ------------------------------------------------- */
+
+ /** Set options, which makes a deep copy of optr if non-null */
+ void setOptions(Options* optr = nullptr);
+ /** Set the statistics registry */
+ void setStatisticsRegistry(StatisticsRegistry* statReg);
+ /** Set proof node manager if it exists */
+ void setProofNodeManager(ProofNodeManager* pnm);
+
+ /* Private shutdown ------------------------------------------------------- */
+ /**
+ * Shutdown method, which destroys the non-essential members of this class
+ * in preparation for destroying SMT engine.
+ */
+ void shutdown();
+ /* Members ---------------------------------------------------------------- */
+
+ /** The SAT context owned by this Env */
+ std::unique_ptr<context::Context> d_context;
+ /** User level context owned by this Env */
+ std::unique_ptr<context::UserContext> d_userContext;
+ /**
+ * A pointer to the node manager of this environment. A node manager is
+ * not necessarily unique to an SmtEngine instance.
+ */
+ NodeManager* d_nodeManager;
+ /**
+ * A pointer to the proof node manager, which is non-null if proofs are
+ * enabled. This is owned by the proof manager of the SmtEngine that owns
+ * this environment.
+ */
+ ProofNodeManager* d_proofNodeManager;
+ /**
+ * The rewriter owned by this Env. We have a different instance
+ * of the rewriter for each Env instance. This is because rewriters may
+ * hold references to objects that belong to theory solvers, which are
+ * specific to an SmtEngine/TheoryEngine instance.
+ */
+ std::unique_ptr<theory::Rewriter> d_rewriter;
+ /** The dump manager */
+ std::unique_ptr<smt::DumpManager> d_dumpManager;
+ /**
+ * The logic we're in. This logic may be an extension of the logic set by the
+ * user, which may be different from the user-provided logic due to the
+ * options we have set.
+ *
+ * This is the authorative copy of the logic that internal subsolvers should
+ * consider during solving and initialization.
+ */
+ LogicInfo d_logic;
+ /**
+ * The statistics registry, which is owned by the SmtEngine that owns this.
+ */
+ StatisticsRegistry* d_statisticsRegistry;
+ /**
+ * The options object, which contains the modified version of the options
+ * provided as input to the SmtEngine that owns this environment. Note
+ * that d_options may be modified by the options manager, e.g. based
+ * on the input logic.
+ *
+ * This is the authorative copy of the options that internal subsolvers should
+ * consider during solving and initialization.
+ */
+ Options d_options;
+ /** Manager for limiting time and abstract resource usage. */
+ std::unique_ptr<ResourceManager> d_resourceManager;
+}; /* class Env */
+
+} // namespace CVC4
+
+#endif /* CVC4__SMT__ENV_H */
#include "smt/defined_function.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"
namespace CVC4 {
SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
- : d_state(new SmtEngineState(*this)),
- d_nodeManager(nm),
- d_absValues(new AbstractValues(d_nodeManager)),
+ : d_env(new Env(nm)),
+ d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
+ d_absValues(new AbstractValues(getNodeManager())),
d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
- d_dumpm(new DumpManager(getUserContext())),
d_routListener(new ResourceOutListener(*this)),
- d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
+ d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
d_smtSolver(nullptr),
d_proofManager(nullptr),
d_model(nullptr),
d_checkModels(nullptr),
d_pfManager(nullptr),
d_ucManager(nullptr),
- d_rewriter(new theory::Rewriter()),
d_definedFunctions(nullptr),
d_sygusSolver(nullptr),
d_abductSolver(nullptr),
d_interpolSolver(nullptr),
d_quantElimSolver(nullptr),
- d_logic(),
d_originalOptions(),
d_isInternalSubsolver(false),
- d_statisticsRegistry(nullptr),
d_stats(nullptr),
d_outMgr(this),
- d_resourceManager(nullptr),
d_optm(nullptr),
d_pp(nullptr),
d_scope(nullptr)
// On the other hand, this hack breaks use cases where multiple SmtEngine
// objects are created by the user.
d_scope.reset(new SmtScope(this));
- if (optr != nullptr)
- {
- // if we provided a set of options, copy their values to the options
- // owned by this SmtEngine.
- d_options.copyValues(*optr);
- }
+ // Set options in the environment, which makes a deep copy of optr if
+ // non-null. This may throw an options exception.
+ d_env->setOptions(optr);
+ // now construct the statistics registry
d_statisticsRegistry.reset(new StatisticsRegistry());
- d_resourceManager.reset(
- new ResourceManager(*d_statisticsRegistry.get(), d_options));
- d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
+ // initialize the environment, which keeps a pointer to statistics registry
+ // and sets up resource manager
+ d_env->setStatisticsRegistry(d_statisticsRegistry.get());
+ // set the options manager
+ d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
// listen to node manager events
- d_nodeManager->subscribeEvents(d_snmListener.get());
+ getNodeManager()->subscribeEvents(d_snmListener.get());
// listen to resource out
- d_resourceManager->registerListener(d_routListener.get());
+ getResourceManager()->registerListener(d_routListener.get());
// make statistics
d_stats.reset(new SmtEngineStatistics());
// reset the preprocessor
*this, getUserContext(), *d_absValues.get(), *d_stats));
// make the SMT solver
d_smtSolver.reset(
- new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
+ new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats));
// make the SyGuS solver
d_sygusSolver.reset(
new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
}
context::UserContext* SmtEngine::getUserContext()
{
- return d_state->getUserContext();
+ return d_env->getUserContext();
}
-context::Context* SmtEngine::getContext() { return d_state->getContext(); }
+context::Context* SmtEngine::getContext() { return d_env->getContext(); }
TheoryEngine* SmtEngine::getTheoryEngine()
{
// of SMT-LIB 2.6 standard.
// set the logic
- if (!d_logic.isLocked())
+ const LogicInfo& logic = getLogicInfo();
+ if (!logic.isLocked())
{
setLogicInternal();
}
// Call finish init on the options manager. This inializes the resource
// manager based on the options, and sets up the best default options
// based on our heuristics.
- d_optm->finishInit(d_logic, d_isInternalSubsolver);
+ d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
ProofNodeManager* pnm = nullptr;
if (options::proof())
{
// ensure bound variable uses canonical bound variables
- d_nodeManager->getBoundVarManager()->enableKeepCacheValues();
+ getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
// make the proof manager
d_pfManager.reset(new PfManager(getUserContext(), this));
PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
d_ucManager.reset(new UnsatCoreManager());
// use this proof node manager
pnm = d_pfManager->getProofNodeManager();
- // enable proof support in the rewriter
- d_rewriter->setProofNodeManager(pnm);
+ // enable proof support in the environment/rewriter
+ d_env->setProofNodeManager(pnm);
// enable it in the assertions pipeline
d_asserts->setProofGenerator(pppg);
// enable it in the SmtSolver
}
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
- d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic));
+ d_smtSolver->finishInit(logic);
// now can construct the SMT-level model object
TheoryEngine* te = d_smtSolver->getTheoryEngine();
{
LogicInfo everything;
everything.lock();
- getOutputManager().getPrinter().toStreamCmdComment(
+ getPrinter().toStreamCmdComment(
getOutputManager().getDumpOut(),
"CVC4 always dumps the most general, all-supported logic (below), as "
"some internals might require the use of a logic more general than "
"the input.");
- getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
- getOutputManager().getDumpOut(), everything.getLogicString());
+ getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(),
+ everything.getLogicString());
}
// initialize the dump manager
- d_dumpm->finishInit();
+ getDumpManager()->finishInit();
// subsolvers
if (options::produceAbducts())
<< "The PropEngine has pushed but the SmtEngine "
"hasn't finished initializing!";
- Assert(d_logic.isLocked());
+ Assert(getLogicInfo().isLocked());
// store that we are finished initializing
d_state->finishInit();
d_state->shutdown();
d_smtSolver->shutdown();
+
+ d_env->shutdown();
}
SmtEngine::~SmtEngine()
#ifdef CVC4_PROOF
d_proofManager.reset(nullptr);
#endif
- d_rewriter.reset(nullptr);
d_pfManager.reset(nullptr);
d_ucManager.reset(nullptr);
d_absValues.reset(nullptr);
d_asserts.reset(nullptr);
- d_dumpm.reset(nullptr);
d_model.reset(nullptr);
d_sygusSolver.reset(nullptr);
d_smtSolver.reset(nullptr);
d_stats.reset(nullptr);
- d_nodeManager->unsubscribeEvents(d_snmListener.get());
+ getNodeManager()->unsubscribeEvents(d_snmListener.get());
d_snmListener.reset(nullptr);
d_routListener.reset(nullptr);
d_optm.reset(nullptr);
d_pp.reset(nullptr);
- // d_resourceManager must be destroyed before d_statisticsRegistry
- d_resourceManager.reset(nullptr);
d_statisticsRegistry.reset(nullptr);
// destroy the state
d_state.reset(nullptr);
+ // destroy the environment
+ d_env.reset(nullptr);
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
throw ModalException("Cannot set logic in SmtEngine after the engine has "
"finished initializing.");
}
- d_logic = logic;
+ d_env->d_logic = logic;
d_userLogic = logic;
setLogicInternal();
}
// dump out a set-logic command
if (Dump.isOn("raw-benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
- getOutputManager().getDumpOut(), d_logic.getLogicString());
+ getPrinter().toStreamCmdSetBenchmarkLogic(
+ getOutputManager().getDumpOut(), getLogicInfo().getLogicString());
}
}
catch (IllegalArgumentException& e)
void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
-const LogicInfo& SmtEngine::getLogicInfo() const { return d_logic; }
+const LogicInfo& SmtEngine::getLogicInfo() const
+{
+ return d_env->getLogicInfo();
+}
LogicInfo SmtEngine::getUserLogicInfo() const
{
// Copy the original options. This is called prior to beginning parsing.
// Hence reset should revert to these options, which note is after reading
// the command line.
- d_originalOptions.copyValues(d_options);
+ d_originalOptions.copyValues(getOptions());
}
const std::string& SmtEngine::getFilename() const
Assert(!d_state->isFullyInited())
<< "setting logic in SmtEngine but the engine has already"
" finished initializing for this run";
- d_logic.lock();
+ d_env->d_logic.lock();
d_userLogic.lock();
}
(value == "sat")
? Result::SAT
: ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
- getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus(
+ getPrinter().toStreamCmdSetBenchmarkStatus(
getOutputManager().getDumpOut(), status);
}
else
{
- getOutputManager().getPrinter().toStreamCmdSetInfo(
+ getPrinter().toStreamCmdSetInfo(
getOutputManager().getDumpOut(), key, value);
}
}
if (key == "all-statistics")
{
vector<SExpr> stats;
- StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry();
+ StatisticsRegistry* sr = getNodeManager()->getStatisticsRegistry();
for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end();
++i)
{
}
DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
- d_dumpm->addToDump(nc, "declarations");
+ getDumpManager()->addToDump(nc, "declarations");
// type check body
debugCheckFunctionBody(formula, formals, func);
if (Dump.isOn("raw-benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdDefineFunctionRec(
+ getPrinter().toStreamCmdDefineFunctionRec(
getOutputManager().getDumpOut(), funcs, formals, formulas);
}
{
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdCheckSat(
- getOutputManager().getDumpOut(), assumption);
+ getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut(),
+ assumption);
}
std::vector<Node> assump;
if (!assumption.isNull())
{
if (assumptions.empty())
{
- getOutputManager().getPrinter().toStreamCmdCheckSat(
- getOutputManager().getDumpOut());
+ getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut());
}
else
{
- getOutputManager().getPrinter().toStreamCmdCheckSatAssuming(
- getOutputManager().getDumpOut(), assumptions);
+ getPrinter().toStreamCmdCheckSatAssuming(getOutputManager().getDumpOut(),
+ assumptions);
}
}
return checkSatInternal(assumptions, inUnsatCore, false);
{
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdQuery(
- getOutputManager().getDumpOut(), node);
+ getPrinter().toStreamCmdQuery(getOutputManager().getDumpOut(), node);
}
return checkSatInternal(
node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
}
return r;
- } catch (UnsafeInterruptException& e) {
- AlwaysAssert(d_resourceManager->out());
+ }
+ 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 = d_resourceManager->outOfResources()
+ Result::UnknownExplanation why = getResourceManager()->outOfResources()
? Result::RESOURCEOUT
: Result::TIMEOUT;
return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
finishInit();
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions(
+ getPrinter().toStreamCmdGetUnsatAssumptions(
getOutputManager().getDumpOut());
}
UnsatCore core = getUnsatCoreInternal();
Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
- if (Dump.isOn("raw-benchmark")) {
- getOutputManager().getPrinter().toStreamCmdAssert(
- getOutputManager().getDumpOut(), formula);
+ if (Dump.isOn("raw-benchmark"))
+ {
+ getPrinter().toStreamCmdAssert(getOutputManager().getDumpOut(), formula);
}
// Substitute out any abstract values in ex
d_sygusSolver->declareSygusVar(var);
if (Dump.isOn("raw-benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdDeclareVar(
+ getPrinter().toStreamCmdDeclareVar(
getOutputManager().getDumpOut(), var, var.getType());
}
// don't need to set that the conjecture is stale
if (Dump.isOn("raw-benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdSynthFun(
+ getPrinter().toStreamCmdSynthFun(
getOutputManager().getDumpOut(), func, vars, isInv, sygusType);
}
}
d_sygusSolver->assertSygusConstraint(constraint);
if (Dump.isOn("raw-benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdConstraint(
- getOutputManager().getDumpOut(), constraint);
+ getPrinter().toStreamCmdConstraint(getOutputManager().getDumpOut(),
+ constraint);
}
}
d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
if (Dump.isOn("raw-benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdInvConstraint(
+ getPrinter().toStreamCmdInvConstraint(
getOutputManager().getDumpOut(), inv, pre, trans, post);
}
}
Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
{
- d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
+ getResourceManager()->spendResource(
+ ResourceManager::Resource::PreprocessStep);
SmtScope smts(this);
finishInit();
SmtScope smts(this);
Trace("smt") << "SMT getValue(" << ex << ")" << endl;
- if(Dump.isOn("benchmark")) {
- d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
+ if (Dump.isOn("benchmark"))
+ {
+ getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
}
TypeNode expectedType = ex.getType();
finishInit();
- if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdGetModel(
- getOutputManager().getDumpOut());
+ if (Dump.isOn("benchmark"))
+ {
+ getPrinter().toStreamCmdGetModel(getOutputManager().getDumpOut());
}
Model* m = getAvailableModel("get model");
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdBlockModel(
- getOutputManager().getDumpOut());
+ getPrinter().toStreamCmdBlockModel(getOutputManager().getDumpOut());
}
Model* m = getAvailableModel("block model");
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdBlockModelValues(
- getOutputManager().getDumpOut(), exprs);
+ getPrinter().toStreamCmdBlockModelValues(getOutputManager().getDumpOut(),
+ exprs);
}
Model* m = getAvailableModel("block model values");
std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
{
- if (!d_logic.isTheoryEnabled(THEORY_SEP))
+ if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
{
const char* msg =
"Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
throw RecoverableModalException(msg);
}
- NodeManagerScope nms(d_nodeManager);
+ NodeManagerScope nms(getNodeManager());
Node heap;
Node nil;
Model* m = getAvailableModel("get separation logic heap and nil");
void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
{
- if (!d_logic.isTheoryEnabled(THEORY_SEP))
+ if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
{
const char* msg =
"Cannot declare heap if not using the separation logic theory.";
}
}
+StatisticsRegistry* SmtEngine::getStatisticsRegistry()
+{
+ return d_statisticsRegistry.get();
+}
+
UnsatCore SmtEngine::getUnsatCoreInternal()
{
#if IS_PROOFS_BUILD
finishInit();
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdGetUnsatCore(
- getOutputManager().getDumpOut());
+ getPrinter().toStreamCmdGetUnsatCore(getOutputManager().getDumpOut());
}
return getUnsatCoreInternal();
}
finishInit();
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdGetProof(
- getOutputManager().getDumpOut());
+ getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
}
#if IS_PROOFS_BUILD
if (!options::proof())
{
SmtScope smts(this);
finishInit();
- if(!d_logic.isPure(THEORY_ARITH) && strict){
- Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
+ 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);
SmtScope smts(this);
finishInit();
d_state->doPendingPops();
- if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdGetAssertions(
- getOutputManager().getDumpOut());
+ if (Dump.isOn("benchmark"))
+ {
+ getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
}
Trace("smt") << "SMT getAssertions()" << endl;
if(!options::produceAssertions()) {
Trace("smt") << "SMT push()" << endl;
d_smtSolver->processAssertions(*d_asserts);
if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdPush(
- getOutputManager().getDumpOut());
+ getPrinter().toStreamCmdPush(getOutputManager().getDumpOut());
}
d_state->userPush();
}
SmtScope smts(this);
finishInit();
Trace("smt") << "SMT pop()" << endl;
- if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdPop(
- getOutputManager().getDumpOut());
+ if (Dump.isOn("benchmark"))
+ {
+ getPrinter().toStreamCmdPop(getOutputManager().getDumpOut());
}
d_state->userPop();
void SmtEngine::reset()
{
- SmtScope smts(this);
+ // save pointer to the current node manager
+ NodeManager* nm = getNodeManager();
Trace("smt") << "SMT reset()" << endl;
- if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdReset(
- getOutputManager().getDumpOut());
+ if (Dump.isOn("benchmark"))
+ {
+ getPrinter().toStreamCmdReset(getOutputManager().getDumpOut());
}
std::string filename = d_state->getFilename();
Options opts;
opts.copyValues(d_originalOptions);
this->~SmtEngine();
- new (this) SmtEngine(d_nodeManager, &opts);
+ new (this) SmtEngine(nm, &opts);
// Restore data set after creation
notifyStartParsing(filename);
}
// (see solver execution modes in the SMT-LIB standard)
Assert(getContext()->getLevel() == 0);
Assert(getUserContext()->getLevel() == 0);
- d_dumpm->resetAssertions();
+ getDumpManager()->resetAssertions();
return;
}
Trace("smt") << "SMT resetAssertions()" << endl;
if (Dump.isOn("benchmark"))
{
- getOutputManager().getPrinter().toStreamCmdResetAssertions(
- getOutputManager().getDumpOut());
+ getPrinter().toStreamCmdResetAssertions(getOutputManager().getDumpOut());
}
d_asserts->clearCurrent();
d_state->notifyResetAssertions();
- d_dumpm->resetAssertions();
+ getDumpManager()->resetAssertions();
// push the state to maintain global context around everything
d_state->setup();
d_smtSolver->interrupt();
}
-void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
- d_resourceManager->setResourceLimit(units, cumulative);
+void SmtEngine::setResourceLimit(unsigned long units, bool cumulative)
+{
+ getResourceManager()->setResourceLimit(units, cumulative);
}
void SmtEngine::setTimeLimit(unsigned long milis)
{
- d_resourceManager->setTimeLimit(milis);
+ getResourceManager()->setTimeLimit(milis);
}
-unsigned long SmtEngine::getResourceUsage() const {
- return d_resourceManager->getResourceUsage();
+unsigned long SmtEngine::getResourceUsage() const
+{
+ return getResourceManager()->getResourceUsage();
}
-unsigned long SmtEngine::getTimeUsage() const {
- return d_resourceManager->getTimeUsage();
+unsigned long SmtEngine::getTimeUsage() const
+{
+ return getResourceManager()->getTimeUsage();
}
unsigned long SmtEngine::getResourceRemaining() const
{
- return d_resourceManager->getResourceRemaining();
+ return getResourceManager()->getResourceRemaining();
}
-NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; }
+NodeManager* SmtEngine::getNodeManager() const
+{
+ return d_env->getNodeManager();
+}
Statistics SmtEngine::getStatistics() const
{
void SmtEngine::flushStatistics(std::ostream& out) const
{
- d_nodeManager->getStatisticsRegistry()->flushInformation(out);
+ getNodeManager()->getStatisticsRegistry()->flushInformation(out);
d_statisticsRegistry->flushInformation(out);
}
void SmtEngine::safeFlushStatistics(int fd) const
{
- d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
+ getNodeManager()->getStatisticsRegistry()->safeFlushInformation(fd);
d_statisticsRegistry->safeFlushInformation(fd);
}
void SmtEngine::setOption(const std::string& key, const std::string& value)
{
- NodeManagerScope nms(d_nodeManager);
+ NodeManagerScope nms(getNodeManager());
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdSetOption(
+ getPrinter().toStreamCmdSetOption(
getOutputManager().getDumpOut(), key, value);
}
}
std::string optionarg = value;
- d_options.setOption(key, optionarg);
+ getOptions().setOption(key, optionarg);
}
void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
CVC4::SExpr SmtEngine::getOption(const std::string& key) const
{
- NodeManagerScope nms(d_nodeManager);
+ NodeManagerScope nms(getNodeManager());
Trace("smt") << "SMT getOption(" << key << ")" << endl;
}
if(Dump.isOn("benchmark")) {
- d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
+ getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
}
if(key == "command-verbosity") {
return SExpr(result);
}
- return SExpr::parseAtom(d_options.getOption(key));
+ return SExpr::parseAtom(getOptions().getOption(key));
}
-Options& SmtEngine::getOptions() { return d_options; }
+Options& SmtEngine::getOptions() { return d_env->d_options; }
-const Options& SmtEngine::getOptions() const { return d_options; }
+const Options& SmtEngine::getOptions() const { return d_env->getOptions(); }
-ResourceManager* SmtEngine::getResourceManager()
+ResourceManager* SmtEngine::getResourceManager() const
{
- return d_resourceManager.get();
+ return d_env->getResourceManager();
}
-DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
+DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); }
-const Printer* SmtEngine::getPrinter() const
-{
- return Printer::getPrinter(d_options[options::outputLanguage]);
-}
+const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); }
OutputManager& SmtEngine::getOutputManager() { return d_outMgr; }
+theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); }
+
}/* CVC4 namespace */
projects / cvc5.git / commitdiff