Also moves d_filename to Env.
d_topLevelSubs->setProofNodeManager(pnm);
}
+void Env::setFilename(const std::string& filename) { d_filename = filename; }
+
void Env::shutdown()
{
d_rewriter.reset(nullptr);
ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
+const std::string& Env::getFilename() const { return d_filename; }
+
bool Env::isTheoryProofProducing() const
{
return d_proofNodeManager != nullptr
*/
ProofNodeManager* getProofNodeManager();
+ /** Return the input name, or the empty string if not set */
+ const std::string& getFilename() const;
+
/**
* Check whether theories should produce proofs as well. Other than whether
* the proof node manager is set, theory engine proofs are conditioned on the
/** Set proof node manager if it exists */
void setProofNodeManager(ProofNodeManager* pnm);
+ /**
+ * Set that the file name of the current instance is the given string. This
+ * is used for various purposes (e.g. get-info, SZS status).
+ */
+ void setFilename(const std::string& filename);
/* Private shutdown ------------------------------------------------------- */
/**
const Options* d_originalOptions;
/** Manager for limiting time and abstract resource usage. */
std::unique_ptr<ResourceManager> d_resourceManager;
+
+ /**
+ * The input file name or the name set through (set-info :filename ...), if
+ * any.
+ */
+ std::string d_filename;
}; /* class Env */
} // namespace cvc5
SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
: d_env(new Env(nm, optr)),
- d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
+ 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)),
void SmtEngine::notifyStartParsing(const std::string& filename)
{
- d_state->setFilename(filename);
+ d_env->setFilename(filename);
d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename",
filename);
// Copy the original options. This is called prior to beginning parsing.
const std::string& SmtEngine::getFilename() const
{
- return d_state->getFilename();
+ return d_env->getFilename();
}
void SmtEngine::setResultStatistic(const std::string& result) {
if (key == "filename")
{
- d_state->setFilename(value);
+ d_env->setFilename(value);
}
else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
{
Result SmtEngine::quickCheck() {
Assert(d_state->isFullyInited());
Trace("smt") << "SMT quickCheck()" << endl;
- const std::string& filename = d_state->getFilename();
+ const std::string& filename = d_env->getFilename();
return Result(
Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
}
{
printStatisticsDiff();
}
- return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
+ return Result(Result::SAT_UNKNOWN, why, d_env->getFilename());
}
}
}
// set the information on the SMT-level model
Assert(m != nullptr);
- m->d_inputName = d_state->getFilename();
+ m->d_inputName = d_env->getFilename();
m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
return m;
}
finishInit();
if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
{
- out << "% SZS output start Proof for " << d_state->getFilename()
- << std::endl;
+ out << "% SZS output start Proof for " << d_env->getFilename() << std::endl;
}
QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
}
if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
{
- out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
+ out << "% SZS output end Proof for " << d_env->getFilename() << std::endl;
}
}
#include "options/base_options.h"
#include "options/option_exception.h"
#include "options/smt_options.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
namespace cvc5 {
namespace smt {
-SmtEngineState::SmtEngineState(context::Context* c,
- context::UserContext* u,
- SmtEngine& smt)
+SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt)
: d_smt(smt),
- d_context(c),
- d_userContext(u),
+ d_env(env),
d_pendingPops(0),
d_fullyInited(false),
d_queryMade(false),
Assert(status == "sat" || status == "unsat" || status == "unknown")
<< "SmtEngineState::notifyExpectedStatus: unexpected status string "
<< status;
- d_expectedStatus = Result(status, d_filename);
+ d_expectedStatus = Result(status, d_env.getFilename());
}
void SmtEngineState::notifyResetAssertions()
}
// Remember the global push/pop around everything when beyond Start mode
// (see solver execution modes in the SMT-LIB standard)
- Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
+ Assert(d_userLevels.size() == 0 && getUserContext()->getLevel() == 1);
popto(0);
}
{
doPendingPops();
- while (options::incrementalSolving() && d_userContext->getLevel() > 1)
+ while (options::incrementalSolving() && getUserContext()->getLevel() > 1)
{
internalPop(true);
}
popto(0);
}
-void SmtEngineState::setFilename(const std::string& filename)
-{
- d_filename = filename;
-}
-
void SmtEngineState::userPush()
{
if (!options::incrementalSolving())
// staying symmetric with pop.
d_smtMode = SmtMode::ASSERT;
- d_userLevels.push_back(d_userContext->getLevel());
+ d_userLevels.push_back(getUserContext()->getLevel());
internalPush();
Trace("userpushpop") << "SmtEngineState: pushed to level "
- << d_userContext->getLevel() << std::endl;
+ << getUserContext()->getLevel() << std::endl;
}
void SmtEngineState::userPop()
// is no longer in scope!).
d_smtMode = SmtMode::ASSERT;
- AlwaysAssert(d_userContext->getLevel() > 0);
- AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
- while (d_userLevels.back() < d_userContext->getLevel())
+ AlwaysAssert(getUserContext()->getLevel() > 0);
+ AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel());
+ while (d_userLevels.back() < getUserContext()->getLevel())
{
internalPop(true);
}
d_userLevels.pop_back();
}
-
+context::Context* SmtEngineState::getContext() { return d_env.getContext(); }
+context::UserContext* SmtEngineState::getUserContext()
+{
+ return d_env.getUserContext();
+}
void SmtEngineState::push()
{
- d_userContext->push();
- d_context->push();
+ getUserContext()->push();
+ getContext()->push();
}
void SmtEngineState::pop()
{
- d_userContext->pop();
- d_context->pop();
+ getUserContext()->pop();
+ getContext()->pop();
}
void SmtEngineState::popto(int toLevel)
{
- d_context->popto(toLevel);
- d_userContext->popto(toLevel);
+ getContext()->popto(toLevel);
+ getUserContext()->popto(toLevel);
}
-context::UserContext* SmtEngineState::getUserContext() { return d_userContext; }
-
-context::Context* SmtEngineState::getContext() { return d_context; }
-
Result SmtEngineState::getStatus() const { return d_status; }
bool SmtEngineState::isFullyInited() const { return d_fullyInited; }
SmtMode SmtEngineState::getMode() const { return d_smtMode; }
-const std::string& SmtEngineState::getFilename() const { return d_filename; }
-
void SmtEngineState::internalPush()
{
Assert(d_fullyInited);
{
// notifies the SmtEngine to process the assertions immediately
d_smt.notifyPushPre();
- d_userContext->push();
+ getUserContext()->push();
// the context push is done inside of the SAT solver
d_smt.notifyPushPost();
}
// the context pop is done inside of the SAT solver
d_smt.notifyPopPre();
// pop the context
- d_userContext->pop();
+ getUserContext()->pop();
--d_pendingPops;
// no need for pop post (for now)
}
namespace cvc5 {
class SmtEngine;
+class Env;
namespace smt {
class SmtEngineState
{
public:
- SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt);
+ SmtEngineState(Env& env, SmtEngine& smt);
~SmtEngineState() {}
/**
* Notify that the expected status of the next check-sat is given by the
* Cleanup, which pops all contexts to level zero.
*/
void cleanup();
- /**
- * Set that the file name of the current instance is the given string. This
- * is used for various purposes (e.g. get-info, SZS status).
- */
- void setFilename(const std::string& filename);
//---------------------------- context management
/**
* the SMT-LIB command pop.
*/
void userPop();
- /** 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();
//---------------------------- end context management
//---------------------------- queries
Result getStatus() const;
/** Get the SMT mode we are in */
SmtMode getMode() const;
- /** return the input name (if any) */
- const std::string& getFilename() const;
//---------------------------- end queries
private:
+ /** get the sat context we are using */
+ context::Context* getContext();
+ /** get the user context we are using */
+ context::UserContext* getUserContext();
/** Pushes the user and SAT contexts */
void push();
/** Pops the user and SAT contexts */
void internalPop(bool immediate = false);
/** Reference to the SmtEngine */
SmtEngine& d_smt;
- /** Expr manager context */
- context::Context* d_context;
- /** User level context */
- context::UserContext* d_userContext;
+ /** Reference to the env of the parent SmtEngine */
+ Env& d_env;
/** The context levels of user pushes */
std::vector<int> d_userLevels;
/** The SMT mode, for details see enumeration above. */
SmtMode d_smtMode;
-
- /**
- * The input file name or the name set through (set-info :filename ...), if
- * any.
- */
- std::string d_filename;
};
} // namespace smt
Trace("smt") << "SmtSolver::check()" << endl;
- const std::string& filename = d_state.getFilename();
+ const std::string& filename = d_env.getFilename();
ResourceManager* rm = d_env.getResourceManager();
if (rm->out())
{
projects / cvc5.git / commitdiff