This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).
smt/smt_engine.h
smt/smt_engine_scope.cpp
smt/smt_engine_scope.h
+ smt/smt_engine_state.cpp
+ smt/smt_engine_state.h
smt/smt_engine_stats.cpp
smt/smt_engine_stats.h
+ smt/smt_mode.cpp
+ smt/smt_mode.h
smt/smt_statistics_registry.cpp
smt/smt_statistics_registry.h
smt/term_formula_removal.cpp
#include "options/smt_options.h"
#include "smt/model.h"
#include "smt/smt_engine.h"
+#include "smt/smt_mode.h"
#include "theory/logic_info.h"
#include "theory/theory_model.h"
#include "util/random.h"
CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions])
<< "Cannot get unsat assumptions unless explicitly enabled "
"(try --produce-unsat-assumptions)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode()
- == SmtEngine::SmtMode::SMT_MODE_UNSAT)
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
<< "Cannot get unsat assumptions unless in unsat mode.";
std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions();
CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
<< "Cannot get unsat core unless explicitly enabled "
"(try --produce-unsat-cores)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode()
- == SmtEngine::SmtMode::SMT_MODE_UNSAT)
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
<< "Cannot get unsat core unless in unsat mode.";
UnsatCore core = d_smtEngine->getUnsatCore();
/* Can not use
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode()
- != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
<< "Cannot get value when in unsat mode.";
std::vector<Term> res;
for (size_t i = 0, n = terms.size(); i < n; ++i)
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation heap term unless model generation is enabled "
"(try --produce-models)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode()
- != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
<< "Cannot get separtion heap term when in unsat mode.";
theory::TheoryModel* m =
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation nil term unless model generation is enabled "
"(try --produce-models)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode()
- != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
<< "Cannot get separtion nil term when in unsat mode.";
theory::TheoryModel* m =
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode()
- != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
<< "Cannot get value when in unsat mode.";
out << *d_smtEngine->getModel();
CVC4_API_SOLVER_TRY_CATCH_END;
bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
{
spendResource(ResourceManager::Resource::PreprocessStep);
- Assert(d_smt.d_pendingPops == 0);
try
{
ScopeCounter depth(d_simplifyAssertionsDepth);
#include "smt/options_manager.h"
#include "smt/preprocessor.h"
#include "smt/smt_engine_scope.h"
+#include "smt/smt_engine_state.h"
#include "smt/smt_engine_stats.h"
#include "smt/term_formula_removal.h"
#include "smt/update_ostream.h"
}/* namespace CVC4::smt */
SmtEngine::SmtEngine(ExprManager* em, Options* optr)
- : d_context(new Context()),
- d_userContext(new UserContext()),
- d_userLevels(),
+ : d_state(new SmtEngineState(*this)),
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
d_absValues(new AbstractValues(d_nodeManager)),
- d_asserts(new Assertions(d_userContext.get(), *d_absValues.get())),
- d_exprNames(new ExprNames(d_userContext.get())),
- d_dumpm(new DumpManager(d_userContext.get())),
+ d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
+ d_exprNames(new ExprNames(getUserContext())),
+ d_dumpm(new DumpManager(getUserContext())),
d_routListener(new ResourceOutListener(*this)),
d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
d_theoryEngine(nullptr),
d_logic(),
d_originalOptions(),
d_isInternalSubsolver(false),
- d_pendingPops(0),
- d_fullyInited(false),
- d_queryMade(false),
- d_needPostsolve(false),
- d_status(),
- d_expectedStatus(),
- d_smtMode(SMT_MODE_START),
d_private(nullptr),
d_statisticsRegistry(nullptr),
d_stats(nullptr),
new ResourceManager(*d_statisticsRegistry.get(), d_options));
d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
d_pp.reset(
- new smt::Preprocessor(*this, d_userContext.get(), *d_absValues.get()));
+ new smt::Preprocessor(*this, getUserContext(), *d_absValues.get()));
d_private.reset(new smt::SmtEnginePrivate(*this));
// listen to node manager events
d_nodeManager->subscribeEvents(d_snmListener.get());
d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
}
+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(); }
+Result SmtEngine::getStatusOfLastCommand() const
+{
+ return d_state->getStatus();
+}
+context::UserContext* SmtEngine::getUserContext()
+{
+ return d_state->getUserContext();
+}
+context::Context* SmtEngine::getContext() { return d_state->getContext(); }
+
void SmtEngine::finishInit()
{
- // Notice that finishInit is called when options are finalized. If we are
- // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
+ 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
+ if (!d_logic.isLocked())
+ {
+ setLogicInternal();
+ }
+
// set the random seed
Random::getRandom().setSeed(options::seed());
// global push/pop around everything, to ensure proper destruction
// of context-dependent data structures
- d_userContext->push();
- d_context->push();
+ d_state->setup();
Trace("smt-debug") << "Set up assertions..." << std::endl;
d_asserts->finishInit();
}
});
d_pp->finishInit();
- Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
-}
-
-void SmtEngine::finalOptionsAreSet() {
- if(d_fullyInited) {
- return;
- }
-
- if(! d_logic.isLocked()) {
- setLogicInternal();
- }
-
- // finish initialization, create the prop engine, etc.
- finishInit();
AlwaysAssert(d_propEngine->getAssertionLevel() == 0)
<< "The PropEngine has pushed but the SmtEngine "
"hasn't finished initializing!";
- d_fullyInited = true;
Assert(d_logic.isLocked());
+
+ // store that we are finished initializing
+ d_state->finishInit();
+ Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
}
void SmtEngine::shutdown() {
- doPendingPops();
-
- while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
- internalPop(true);
- }
+ d_state->shutdown();
if (d_propEngine != nullptr)
{
// global push/pop around everything, to ensure proper destruction
// of context-dependent data structures
- d_context->popto(0);
- d_userContext->popto(0);
+ d_state->cleanup();
if(d_assignments != NULL) {
d_assignments->deleteSelf();
// d_resourceManager must be destroyed before d_statisticsRegistry
d_resourceManager.reset(nullptr);
d_statisticsRegistry.reset(nullptr);
-
-
- d_userContext.reset(nullptr);
- d_context.reset(nullptr);
+ // destroy the state
+ d_state.reset(nullptr);
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
void SmtEngine::setLogic(const LogicInfo& logic)
{
SmtScope smts(this);
- if(d_fullyInited) {
+ if (d_state->isFullyInited())
+ {
throw ModalException("Cannot set logic in SmtEngine after the engine has "
"finished initializing.");
}
void SmtEngine::notifyStartParsing(std::string filename)
{
- d_filename = filename;
-
+ d_state->setFilename(filename);
// 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);
}
-std::string SmtEngine::getFilename() const { return d_filename; }
+const std::string& SmtEngine::getFilename() const
+{
+ return d_state->getFilename();
+}
void SmtEngine::setLogicInternal()
{
- Assert(!d_fullyInited)
+ Assert(!d_state->isFullyInited())
<< "setting logic in SmtEngine but the engine has already"
" finished initializing for this run";
d_logic.lock();
}
else if (key == "filename")
{
- d_filename = value.getValue();
+ d_state->setFilename(value.getValue());
return;
}
else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
throw OptionException("argument to (set-info :status ..) must be "
"`sat' or `unsat' or `unknown'");
}
- d_expectedStatus = Result(s, d_filename);
+ d_state->notifyExpectedStatus(s);
return;
}
throw UnrecognizedOptionException();
if (key == "status")
{
// sat | unsat | unknown
- switch (d_status.asSatisfiabilityResult().isSat())
+ Result status = d_state->getStatus();
+ switch (status.asSatisfiabilityResult().isSat())
{
case Result::SAT: return SExpr(SExpr::Keyword("sat"));
case Result::UNSAT: return SExpr(SExpr::Keyword("unsat"));
}
if (key == "reason-unknown")
{
- if (!d_status.isNull() && d_status.isUnknown())
+ Result status = d_state->getStatus();
+ if (!status.isNull() && status.isUnknown())
{
- stringstream ss;
- ss << d_status.whyUnknown();
+ std::stringstream ss;
+ ss << status.whyUnknown();
string s = ss.str();
transform(s.begin(), s.end(), s.begin(), ::tolower);
return SExpr(SExpr::Keyword(s));
}
if (key == "assertion-stack-levels")
{
- AlwaysAssert(d_userLevels.size()
- <= std::numeric_limits<unsigned long int>::max());
- return SExpr(static_cast<unsigned long int>(d_userLevels.size()));
+ size_t ulevel = d_state->getNumUserLevels();
+ AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max());
+ return SExpr(static_cast<unsigned long int>(ulevel));
}
Assert(key == "all-options");
// get the options, like all-statistics
bool global)
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
debugCheckFormals(formals, func);
bool global)
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
if (funcs.size() != formals.size() && funcs.size() != formulas.size())
}
Result SmtEngine::check() {
- Assert(d_fullyInited);
- Assert(d_pendingPops == 0);
+ Assert(d_state->isFullyReady());
Trace("smt") << "SmtEngine::check()" << endl;
-
+ const std::string& filename = d_state->getFilename();
if (d_resourceManager->out())
{
Result::UnknownExplanation why = d_resourceManager->outOfResources()
? Result::RESOURCEOUT
: Result::TIMEOUT;
- return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
+ return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
}
d_resourceManager->beginCall();
<< d_resourceManager->getTimeUsage() << ", resources "
<< d_resourceManager->getResourceUsage() << endl;
- return Result(result, d_filename);
+ return Result(result, filename);
}
Result SmtEngine::quickCheck() {
- Assert(d_fullyInited);
+ Assert(d_state->isFullyInited());
Trace("smt") << "SMT quickCheck()" << endl;
+ const std::string& filename = d_state->getFilename();
return Result(
- Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
+ Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
}
theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
throw RecoverableModalException(ss.str().c_str());
}
- if (d_smtMode != SMT_MODE_SAT && d_smtMode != SMT_MODE_SAT_UNKNOWN)
+ if (d_state->getMode() != SmtMode::SAT
+ && d_state->getMode() != SmtMode::SAT_UNKNOWN)
{
std::stringstream ss;
ss << "Cannot " << c
return m;
}
+void SmtEngine::notifyPushPre() { processAssertionsInternal(); }
+void SmtEngine::notifyPushPost()
+{
+ TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
+ d_propEngine->push();
+}
+void SmtEngine::notifyPopPre()
+{
+ TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
+ d_propEngine->pop();
+}
+void SmtEngine::notifyPostSolvePre() { d_propEngine->resetTrail(); }
+void SmtEngine::notifyPostSolvePost() { d_theoryEngine->postsolve(); }
+
void SmtEngine::processAssertionsInternal()
{
TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime);
d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
- Assert(d_fullyInited);
- Assert(d_pendingPops == 0);
+ Assert(d_state->isFullyReady());
AssertionPipeline& ap = d_asserts->getAssertionPipeline();
try
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
Trace("smt") << "SmtEngine::"
<< (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
<< assumptions << ")" << endl;
-
- if(d_queryMade && !options::incrementalSolving()) {
- throw ModalException("Cannot make multiple queries unless "
- "incremental solving is enabled "
- "(try --incremental)");
- }
-
- // Note that a query has been made and we are in assert mode
- d_queryMade = true;
- d_smtMode = SMT_MODE_ASSERT;
-
- // push if there are assumptions
- bool didInternalPush = false;
- if (!assumptions.empty())
- {
- internalPush();
- didInternalPush = true;
- }
+ // update the state to indicate we are about to run a check-sat
+ bool hasAssumptions = !assumptions.empty();
+ d_state->notifyCheckSat(hasAssumptions);
// then, initialize the assertions
d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
Trace("smt") << "SmtEngine::global negate returned " << r << std::endl;
}
- d_needPostsolve = true;
-
- // Pop the context
- if (didInternalPush)
- {
- internalPop();
- }
-
- // Remember the status
- d_status = r;
- // Check against expected status
- if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
- && d_status != d_expectedStatus)
- {
- CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got "
- << d_status;
- }
- d_expectedStatus = Result();
- // Update the SMT mode
- if (d_status.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- d_smtMode = SMT_MODE_UNSAT;
- }
- else if (d_status.asSatisfiabilityResult().isSat() == Result::SAT)
- {
- d_smtMode = SMT_MODE_SAT;
- }
- else
- {
- d_smtMode = SMT_MODE_SAT_UNKNOWN;
- }
+ // notify our state of the check-sat result
+ d_state->notifyCheckSatResult(hasAssumptions, r);
Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
<< "(" << assumptions << ") => " << r << endl;
return r;
} catch (UnsafeInterruptException& e) {
AlwaysAssert(d_resourceManager->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::RESOURCEOUT
: Result::TIMEOUT;
- return Result(Result::SAT_UNKNOWN, why, d_filename);
+ return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
}
}
"Cannot get unsat assumptions when produce-unsat-assumptions option "
"is off.");
}
- if (d_smtMode != SMT_MODE_UNSAT)
+ if (d_state->getMode() != SmtMode::UNSAT)
{
throw RecoverableModalException(
"Cannot get unsat assumptions unless immediately preceded by "
"UNSAT/ENTAILED.");
}
- finalOptionsAreSet();
+ finishInit();
if (Dump.isOn("benchmark"))
{
Dump("benchmark") << GetUnsatAssumptionsCommand();
Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
d_private->d_sygusVars.push_back(Node::fromExpr(var));
Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
Type type)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
d_private->d_sygusVars.push_back(Node::fromExpr(var));
Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
const std::vector<Expr>& vars)
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
Node fn = Node::fromExpr(func);
d_private->d_sygusFunSymbols.push_back(fn);
if (!vars.empty())
void SmtEngine::assertSygusConstraint(const Node& constraint)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
d_private->d_sygusConstraints.push_back(constraint);
Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
const Expr& post)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
// build invariant constraint
// get variables (regular and their respective primed versions)
d_private->d_sygusConjectureStale = false;
- if (options::incrementalSolving())
- {
- // we push a context so that this conjecture is removed if we modify it
- // later
- internalPush();
- assertFormula(body, true);
- }
- else
- {
- query = body.toExpr();
- }
+ // TODO (project #7): if incremental, we should push a context and assert
+ query = body.toExpr();
}
Result r = checkSatisfiability(query, true, false);
Node SmtEngine::simplify(const Node& ex)
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
// ensure we've processed assertions
processAssertionsInternal();
return d_pp->simplify(ex);
d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
// set expandOnly flag to true
return d_pp->expandDefinitions(ex, true);
}
bool SmtEngine::addToAssignment(const Expr& ex) {
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
// Substitute out any abstract values in ex
Node n = d_absValues->substituteAbstractValues(Node::fromExpr(ex));
TypeNode type = n.getType(options::typeChecking());
{
Trace("smt") << "SMT getAssignment()" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssignmentCommand();
}
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetModelCommand();
std::vector<Expr> eassertsProc = getExpandedAssertions();
ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode());
}
- m->d_inputName = d_filename;
- m->d_isKnownSat = (d_smtMode == SMT_MODE_SAT);
+ m->d_inputName = d_state->getFilename();
+ m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
return m;
}
Trace("smt") << "SMT blockModel()" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if (Dump.isOn("benchmark"))
{
Trace("smt") << "SMT blockModelValues()" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
PrettyCheckArgument(
!exprs.empty(),
throw ModalException(
"Cannot get an unsat core when produce-unsat-cores option is off.");
}
- if (d_smtMode != SMT_MODE_UNSAT)
+ if (d_state->getMode() != SmtMode::UNSAT)
{
throw RecoverableModalException(
"Cannot get an unsat core unless immediately preceded by "
UnsatCore SmtEngine::getUnsatCore() {
Trace("smt") << "SMT getUnsatCore()" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetUnsatCoreCommand();
}
{
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetProofCommand();
}
if(!options::proof()) {
throw ModalException("Cannot get a proof when produce-proofs option is off.");
}
- if (d_smtMode != SMT_MODE_UNSAT)
+ if (d_state->getMode() != SmtMode::UNSAT)
{
throw RecoverableModalException(
"Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
void SmtEngine::printInstantiations( std::ostream& out ) {
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if (options::instFormatMode() == options::InstFormatMode::SZS)
{
- out << "% SZS output start Proof for " << d_filename.c_str() << std::endl;
+ out << "% SZS output start Proof for " << d_state->getFilename()
+ << std::endl;
}
if( d_theoryEngine ){
d_theoryEngine->printInstantiations( out );
}
if (options::instFormatMode() == options::InstFormatMode::SZS)
{
- out << "% SZS output end Proof for " << d_filename.c_str() << std::endl;
+ out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
}
}
void SmtEngine::printSynthSolution( std::ostream& out ) {
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if( d_theoryEngine ){
d_theoryEngine->printSynthSolution( out );
}else{
bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
std::map<Node, std::map<Node, Node>> sol_mapn;
Assert(d_theoryEngine != nullptr);
// fail if the theory engine does not have synthesis solutions
Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
if(!d_logic.isPure(THEORY_ARITH) && strict){
Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
}
const TypeNode& grammarType,
Node& abd)
{
- if (d_abductSolver->getAbduct(conj, grammarType, abd))
- {
- // successfully generated an abduct, update to abduct state
- d_smtMode = SMT_MODE_ABDUCT;
- return true;
- }
- // failed, we revert to the assert state
- d_smtMode = SMT_MODE_ASSERT;
- return false;
+ bool success = d_abductSolver->getAbduct(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)
}
}
-vector<Expr> SmtEngine::getAssertions() {
+std::vector<Expr> SmtEngine::getAssertions()
+{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssertionsCommand();
}
void SmtEngine::push()
{
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ finishInit();
+ d_state->doPendingPops();
Trace("smt") << "SMT push()" << endl;
processAssertionsInternal();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PushCommand();
}
- if(!options::incrementalSolving()) {
- throw ModalException("Cannot push when not solving incrementally (use --incremental)");
- }
-
-
- // The problem isn't really "extended" yet, but this disallows
- // get-model after a push, simplifying our lives somewhat and
- // staying symmetric with pop.
- d_smtMode = SMT_MODE_ASSERT;
-
- d_userLevels.push_back(d_userContext->getLevel());
- internalPush();
- Trace("userpushpop") << "SmtEngine: pushed to level "
- << d_userContext->getLevel() << endl;
+ d_state->userPush();
}
void SmtEngine::pop() {
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
Trace("smt") << "SMT pop()" << endl;
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PopCommand();
}
- if(!options::incrementalSolving()) {
- throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
- }
- if(d_userLevels.size() == 0) {
- throw ModalException("Cannot pop beyond the first user frame");
- }
-
- // The problem isn't really "extended" yet, but this disallows
- // get-model after a pop, simplifying our lives somewhat. It might
- // not be strictly necessary to do so, since the pops occur lazily,
- // but also it would be weird to have a legally-executed (get-model)
- // that only returns a subset of the assignment (because the rest
- // is no longer in scope!).
- d_smtMode = SMT_MODE_ASSERT;
-
- AlwaysAssert(d_userContext->getLevel() > 0);
- AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
- while (d_userLevels.back() < d_userContext->getLevel()) {
- internalPop(true);
- }
- d_userLevels.pop_back();
+ d_state->userPop();
// Clear out assertion queues etc., in case anything is still in there
d_asserts->clearCurrent();
d_pp->clearLearnedLiterals();
Trace("userpushpop") << "SmtEngine: popped to level "
- << d_userContext->getLevel() << endl;
- // FIXME: should we reset d_status here?
+ << getUserContext()->getLevel() << endl;
+ // should we reset d_status here?
// SMT-LIBv2 spec seems to imply no, but it would make sense to..
}
-void SmtEngine::internalPush() {
- Assert(d_fullyInited);
- Trace("smt") << "SmtEngine::internalPush()" << endl;
- doPendingPops();
- if(options::incrementalSolving()) {
- processAssertionsInternal();
- TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
- d_userContext->push();
- // the d_context push is done inside of the SAT solver
- d_propEngine->push();
- }
-}
-
-void SmtEngine::internalPop(bool immediate) {
- Assert(d_fullyInited);
- Trace("smt") << "SmtEngine::internalPop()" << endl;
- if(options::incrementalSolving()) {
- ++d_pendingPops;
- }
- if(immediate) {
- doPendingPops();
- }
-}
-
-void SmtEngine::doPendingPops() {
- Trace("smt") << "SmtEngine::doPendingPops()" << endl;
- Assert(d_pendingPops == 0 || options::incrementalSolving());
- // check to see if a postsolve() is pending
- if (d_needPostsolve)
- {
- d_propEngine->resetTrail();
- }
- while(d_pendingPops > 0) {
- TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
- d_propEngine->pop();
- // the d_context pop is done inside of the SAT solver
- d_userContext->pop();
- --d_pendingPops;
- }
- if (d_needPostsolve)
- {
- d_theoryEngine->postsolve();
- d_needPostsolve = false;
- }
-}
-
void SmtEngine::reset()
{
SmtScope smts(this);
{
SmtScope smts(this);
- if (!d_fullyInited)
+ 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(d_context->getLevel() == 0);
- Assert(d_userContext->getLevel() == 0);
+ Assert(getContext()->getLevel() == 0);
+ Assert(getUserContext()->getLevel() == 0);
d_dumpm->resetAssertions();
return;
}
- doPendingPops();
Trace("smt") << "SMT resetAssertions()" << endl;
if (Dump.isOn("benchmark"))
Dump("benchmark") << ResetAssertionsCommand();
}
- while (!d_userLevels.empty())
- {
- pop();
- }
-
- // 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);
- d_context->popto(0);
- d_userContext->popto(0);
+ d_state->notifyResetAssertions();
d_dumpm->resetAssertions();
- d_userContext->push();
- d_context->push();
+ // push the state to maintain global context around everything
+ d_state->setup();
/* Create new PropEngine.
* First force destruction of referenced PropEngine to enforce that
void SmtEngine::interrupt()
{
- if(!d_fullyInited) {
+ if (!d_state->isFullyInited())
+ {
return;
}
d_propEngine->interrupt();
const std::string& str_value)
{
SmtScope smts(this);
- finalOptionsAreSet();
+ finishInit();
std::vector<Node> node_values;
- for( unsigned i=0; i<expr_values.size(); i++ ){
+ for (std::size_t i = 0, n = expr_values.size(); i < n; i++)
+ {
node_values.push_back( expr_values[i].getNode() );
}
d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
// Always check whether the SmtEngine has been initialized (which is done
// upon entering Assert mode the first time). No option can be set after
// initialized.
- if(d_fullyInited) {
+ if (d_state->isFullyInited())
+ {
throw ModalException("SmtEngine::setOption called after initialization.");
}
NodeManagerScope nms(d_nodeManager);
return;
}
d_private->d_sygusConjectureStale = true;
- if (options::incrementalSolving())
- {
- internalPop();
- }
+ // TODO (project #7): if incremental, we should pop a context
}
}/* CVC4 namespace */
#include "options/options.h"
#include "proof/unsat_core.h"
#include "smt/logic_exception.h"
+#include "smt/smt_mode.h"
#include "theory/logic_info.h"
#include "util/hash.h"
#include "util/proof.h"
namespace smt {
/** Utilities */
+class SmtEngineState;
class AbstractValues;
class Assertions;
class ExprNames;
// TODO (Issue #1096): Remove this friend relationship.
friend class ::CVC4::preprocessing::PreprocessingPassContext;
friend class ::CVC4::smt::SmtEnginePrivate;
+ friend class ::CVC4::smt::SmtEngineState;
friend class ::CVC4::smt::SmtScope;
friend class ::CVC4::smt::ProcessAssertions;
friend ProofManager* ::CVC4::smt::currentProofManager();
public:
/* ....................................................................... */
- /**
- * The current mode of the solver, which is an extension of Figure 4.1 on
- * page 52 of the SMT-LIB version 2.6 standard
- * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
- */
- enum SmtMode
- {
- // the initial state of the solver
- SMT_MODE_START,
- // normal state of the solver, after assert/push/pop/declare/define
- SMT_MODE_ASSERT,
- // immediately after a check-sat returning "sat"
- SMT_MODE_SAT,
- // immediately after a check-sat returning "unknown"
- SMT_MODE_SAT_UNKNOWN,
- // immediately after a check-sat returning "unsat"
- SMT_MODE_UNSAT,
- // immediately after a successful call to get-abduct
- SMT_MODE_ABDUCT,
- // immediately after a successful call to get-interpol
- SMT_MODE_INTERPOL
- };
-
/**
* Construct an SmtEngine with the given expression manager.
* If provided, optr is a pointer to a set of options that should initialize the values
/** Destruct the SMT engine. */
~SmtEngine();
+ //--------------------------------------------- concerning the state
+
/**
- * Return true if this SmtEngine is fully initialized (post-construction).
+ * 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.
*/
- bool isFullyInited() { return d_fullyInited; }
-
+ 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() { return d_queryMade; }
-
+ bool isQueryMade() const;
/** Return the user context level. */
- size_t getNumUserLevels() { return d_userLevels.size(); }
-
+ size_t getNumUserLevels() const;
/** Return the current mode of the solver. */
- SmtMode getSmtMode() { return d_smtMode; }
+ SmtMode getSmtMode() 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.
*/
void notifyStartParsing(std::string filename);
/** return the input name (if any) */
- std::string getFilename() const;
+ const std::string& getFilename() const;
/**
* Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
/** Flush statistic from this SmtEngine. Safe to use in a signal handler. */
void safeFlushStatistics(int fd) const;
- /**
- * Returns the most recent result of checkSat/checkEntailed or
- * (set-info :status).
- */
- Result getStatusOfLastCommand() const { return d_status; }
-
/**
* Set user attribute.
* This function is called when an attribute is set by a user.
/** Set solver instance that owns this SmtEngine. */
void setSolver(api::Solver* solver) { d_solver = solver; }
+ /** 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() { return d_theoryEngine.get(); }
/** Get a pointer to the PropEngine owned by this SmtEngine. */
prop::PropEngine* getPropEngine() { return d_propEngine.get(); }
- /** Get a pointer to the UserContext owned by this SmtEngine. */
- context::UserContext* getUserContext() { return d_userContext.get(); };
-
- /** Get a pointer to the Context owned by this SmtEngine. */
- context::Context* getContext() { return d_context.get(); };
-
/** Get a pointer to the ProofManager owned by this SmtEngine. */
ProofManager* getProofManager() { return d_proofManager.get(); };
*/
void checkAbduct(Node a);
- /**
- * This is something of an "init" procedure, but is idempotent; call
- * as often as you like. 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).
- */
- void finalOptionsAreSet();
-
- /**
- * Create theory engine, prop engine, decision engine. Called by
- * finalOptionsAreSet()
- */
- void finishInit();
-
/**
* This is called by the destructor, just before destroying the
* PropEngine, TheoryEngine, and DecisionEngine (in that order). It
*/
theory::TheoryModel* getAvailableModel(const char* c) const;
- void internalPush();
-
- void internalPop(bool immediate = false);
-
- void doPendingPops();
+ // --------------------------------------- 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
/** Solver instance that owns this SmtEngine instance. */
api::Solver* d_solver = nullptr;
- /** Expr manager context */
- std::unique_ptr<context::Context> d_context;
- /** User level context */
- std::unique_ptr<context::UserContext> d_userContext;
- /** The context levels of user pushes */
- std::vector<int> d_userLevels;
+ /**
+ * 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;
/** Our expression manager */
ExprManager* d_exprManager;
/** Whether this is an internal subsolver. */
bool d_isInternalSubsolver;
- /**
- * Number of internal pops that have been deferred.
- */
- unsigned d_pendingPops;
-
- /**
- * Whether or not this SmtEngine is fully initialized (post-construction).
- * 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.
- */
- bool d_fullyInited;
-
- /**
- * Whether or not a checkEntailed() or checkSatisfiability() has already been
- * made through this SmtEngine. If true, and incrementalSolving is false,
- * then attempting an additional checkEntailed() or checkSat() will fail with
- * a ModalException.
- */
- bool d_queryMade;
-
- /**
- * Internal status flag to indicate whether we've sent a theory
- * presolve() notification and need to match it with a postsolve().
- */
- bool d_needPostsolve;
-
- /**
- * Most recent result of last checkSatisfiability/checkEntailed or
- * (set-info :status).
- */
- Result d_status;
-
- /**
- * The expected status of the next satisfiability check.
- */
- Result d_expectedStatus;
-
- SmtMode d_smtMode;
-
- /**
- * The input file name (if any) or the name set through setInfo (if any)
- */
- std::string d_filename;
-
/**
* Verbosity of various commands.
*/
--- /dev/null
+/********************* */
+/*! \file smt_engine_state.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Utility for maintaining the state of the SMT engine.
+ **/
+
+#include "smt/smt_engine_state.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+namespace smt {
+
+SmtEngineState::SmtEngineState(SmtEngine& smt)
+ : d_smt(smt),
+ d_context(new context::Context()),
+ d_userContext(new context::UserContext()),
+ d_pendingPops(0),
+ d_fullyInited(false),
+ d_queryMade(false),
+ d_needPostsolve(false),
+ d_status(),
+ d_expectedStatus(),
+ d_smtMode(SmtMode::START)
+{
+}
+
+void SmtEngineState::notifyExpectedStatus(const std::string& status)
+{
+ Assert(status == "sat" || status == "unsat" || status == "unknown")
+ << "SmtEngineState::notifyExpectedStatus: unexpected status string "
+ << status;
+ d_expectedStatus = Result(status, d_filename);
+}
+
+void SmtEngineState::notifyResetAssertions()
+{
+ doPendingPops();
+ while (!d_userLevels.empty())
+ {
+ userPop();
+ }
+ // 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);
+ popto(0);
+}
+
+void SmtEngineState::notifyCheckSat(bool hasAssumptions)
+{
+ // process the pending pops
+ doPendingPops();
+ if (d_queryMade && !options::incrementalSolving())
+ {
+ throw ModalException(
+ "Cannot make multiple queries unless "
+ "incremental solving is enabled "
+ "(try --incremental)");
+ }
+
+ // Note that a query has been made and we are in assert mode
+ d_queryMade = true;
+ d_smtMode = SmtMode::ASSERT;
+
+ // push if there are assumptions
+ if (hasAssumptions)
+ {
+ internalPush();
+ }
+}
+
+void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r)
+{
+ d_needPostsolve = true;
+
+ // Pop the context
+ if (hasAssumptions)
+ {
+ internalPop();
+ }
+
+ // Remember the status
+ d_status = r;
+ // Check against expected status
+ if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
+ && d_status != d_expectedStatus)
+ {
+ CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got "
+ << d_status;
+ }
+ // clear expected status
+ d_expectedStatus = Result();
+ // Update the SMT mode
+ switch (d_status.asSatisfiabilityResult().isSat())
+ {
+ case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break;
+ case Result::SAT: d_smtMode = SmtMode::SAT; break;
+ default: d_smtMode = SmtMode::SAT_UNKNOWN;
+ }
+}
+
+void SmtEngineState::notifyGetAbduct(bool success)
+{
+ if (success)
+ {
+ // successfully generated an abduct, update to abduct state
+ d_smtMode = SmtMode::ABDUCT;
+ }
+ else
+ {
+ // failed, we revert to the assert state
+ d_smtMode = SmtMode::ASSERT;
+ }
+}
+
+void SmtEngineState::setup()
+{
+ // push a context
+ push();
+}
+
+void SmtEngineState::finishInit()
+{
+ // set the flag to remember that we are fully initialized
+ d_fullyInited = true;
+}
+
+void SmtEngineState::shutdown()
+{
+ doPendingPops();
+
+ while (options::incrementalSolving() && d_userContext->getLevel() > 1)
+ {
+ internalPop(true);
+ }
+}
+
+void SmtEngineState::cleanup()
+{
+ // pop to level zero
+ popto(0);
+}
+
+void SmtEngineState::setFilename(const std::string& filename)
+{
+ d_filename = filename;
+}
+
+void SmtEngineState::userPush()
+{
+ if (!options::incrementalSolving())
+ {
+ throw ModalException(
+ "Cannot push when not solving incrementally (use --incremental)");
+ }
+ // The problem isn't really "extended" yet, but this disallows
+ // get-model after a push, simplifying our lives somewhat and
+ // staying symmetric with pop.
+ d_smtMode = SmtMode::ASSERT;
+
+ d_userLevels.push_back(d_userContext->getLevel());
+ internalPush();
+ Trace("userpushpop") << "SmtEngineState: pushed to level "
+ << d_userContext->getLevel() << std::endl;
+}
+
+void SmtEngineState::userPop()
+{
+ if (!options::incrementalSolving())
+ {
+ throw ModalException(
+ "Cannot pop when not solving incrementally (use --incremental)");
+ }
+ if (d_userLevels.size() == 0)
+ {
+ throw ModalException("Cannot pop beyond the first user frame");
+ }
+ // The problem isn't really "extended" yet, but this disallows
+ // get-model after a pop, simplifying our lives somewhat. It might
+ // not be strictly necessary to do so, since the pops occur lazily,
+ // but also it would be weird to have a legally-executed (get-model)
+ // that only returns a subset of the assignment (because the rest
+ // 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())
+ {
+ internalPop(true);
+ }
+ d_userLevels.pop_back();
+}
+
+void SmtEngineState::push()
+{
+ d_userContext->push();
+ d_context->push();
+}
+
+void SmtEngineState::pop()
+{
+ d_userContext->pop();
+ d_context->pop();
+}
+
+void SmtEngineState::popto(int toLevel)
+{
+ d_context->popto(toLevel);
+ d_userContext->popto(toLevel);
+}
+
+context::UserContext* SmtEngineState::getUserContext()
+{
+ return d_userContext.get();
+}
+
+context::Context* SmtEngineState::getContext() { return d_context.get(); }
+
+Result SmtEngineState::getStatus() const { return d_status; }
+
+bool SmtEngineState::isFullyInited() const { return d_fullyInited; }
+bool SmtEngineState::isFullyReady() const
+{
+ return d_fullyInited && d_pendingPops == 0;
+}
+bool SmtEngineState::isQueryMade() const { return d_queryMade; }
+size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); }
+
+SmtMode SmtEngineState::getMode() const { return d_smtMode; }
+
+const std::string& SmtEngineState::getFilename() const { return d_filename; }
+
+void SmtEngineState::internalPush()
+{
+ Assert(d_fullyInited);
+ Trace("smt") << "SmtEngineState::internalPush()" << std::endl;
+ doPendingPops();
+ if (options::incrementalSolving())
+ {
+ // notifies the SmtEngine to process the assertions immediately
+ d_smt.notifyPushPre();
+ d_userContext->push();
+ // the context push is done inside of the SAT solver
+ d_smt.notifyPushPost();
+ }
+}
+
+void SmtEngineState::internalPop(bool immediate)
+{
+ Assert(d_fullyInited);
+ Trace("smt") << "SmtEngineState::internalPop()" << std::endl;
+ if (options::incrementalSolving())
+ {
+ ++d_pendingPops;
+ }
+ if (immediate)
+ {
+ doPendingPops();
+ }
+}
+
+void SmtEngineState::doPendingPops()
+{
+ Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl;
+ Assert(d_pendingPops == 0 || options::incrementalSolving());
+ // check to see if a postsolve() is pending
+ if (d_needPostsolve)
+ {
+ d_smt.notifyPostSolvePre();
+ }
+ while (d_pendingPops > 0)
+ {
+ // the context pop is done inside of the SAT solver
+ d_smt.notifyPopPre();
+ // pop the context
+ d_userContext->pop();
+ --d_pendingPops;
+ // no need for pop post (for now)
+ }
+ if (d_needPostsolve)
+ {
+ d_smt.notifyPostSolvePost();
+ d_needPostsolve = false;
+ }
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file smt_engine_state.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Utility for maintaining the state of the SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__SMT_ENGINE_STATE_H
+#define CVC4__SMT__SMT_ENGINE_STATE_H
+
+#include <string>
+
+#include "context/context.h"
+#include "smt/smt_mode.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * This utility is responsible for maintaining the basic state of the SmtEngine.
+ *
+ * It has no concept of anything related to the assertions of the SmtEngine,
+ * or more generally it does not depend on Node.
+ *
+ * This class has three sets of interfaces:
+ * (1) notification methods that are used by SmtEngine to notify when an event
+ * occurs (e.g. the beginning of a check-sat call),
+ * (2) maintaining the SAT and user contexts to be used by the SmtEngine,
+ * (3) general information queries, including the mode that the SmtEngine is
+ * in, based on the notifications it has received.
+ *
+ * It maintains a reference to the SmtEngine for the sake of making callbacks.
+ */
+class SmtEngineState
+{
+ public:
+ SmtEngineState(SmtEngine& smt);
+ ~SmtEngineState() {}
+ /**
+ * Notify that the expected status of the next check-sat is given by the
+ * string status, which should be one of "sat", "unsat" or "unknown".
+ */
+ void notifyExpectedStatus(const std::string& status);
+ /**
+ * Notify that the SmtEngine is fully initialized, which is called when
+ * options are finalized.
+ */
+ void notifyFullyInited();
+ /**
+ * Notify that we are resetting the assertions, called when a reset-assertions
+ * command is issued by the user.
+ */
+ void notifyResetAssertions();
+ /**
+ * Notify that we are about to call check-sat. This call is made prior to
+ * initializing the assertions. It processes pending pops and pushes a
+ * (user) context if necessary.
+ *
+ * @param hasAssumptions Whether the call to check-sat has assumptions. If
+ * so, we push a context.
+ */
+ void notifyCheckSat(bool hasAssumptions);
+ /**
+ * Notify that the result of the last check-sat was r. This should be called
+ * once immediately following notifyCheckSat() if the check-sat call
+ * returned normal (i.e. it was not interupted).
+ *
+ * @param hasAssumptions Whether the prior call to check-sat had assumptions.
+ * If so, we pop a context.
+ * @param r The result of the check-sat call.
+ */
+ void notifyCheckSatResult(bool hasAssumptions, Result r);
+ /**
+ * Notify that we finished an abduction query, where success is whether the
+ * command was successful. This is managed independently of the above
+ * calls for notifying check-sat. In other words, if a get-abduct command
+ * is issued to an SmtEngine, it may use a satisfiability call (if desired)
+ * to solve the abduction query. This method is called *in addition* to
+ * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
+ * In particular, it is called after these two methods are completed.
+ * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction
+ * was successful.
+ */
+ void notifyGetAbduct(bool success);
+ /**
+ * Setup the context, which makes a single push to maintain a global
+ * context around everything.
+ */
+ void setup();
+ /**
+ * Set that we are in a fully initialized state.
+ */
+ void finishInit();
+ /**
+ * Prepare for a shutdown of the SmtEngine, which does pending pops and
+ * pops the user context to zero.
+ */
+ void shutdown();
+ /**
+ * 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
+ /**
+ * Do all pending pops, which ensures that the context levels are up-to-date.
+ * This method should be called by the SmtEngine before using any of its
+ * members that rely on the context (e.g. PropEngine or TheoryEngine).
+ */
+ void doPendingPops();
+ /**
+ * Called when the user of SmtEngine issues a push. This corresponds to
+ * the SMT-LIB command push.
+ */
+ void userPush();
+ /**
+ * Called when the user of SmtEngine issues a pop. This corresponds to
+ * 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
+ /**
+ * Return true if the SmtEngine is fully initialized (post-construction).
+ * 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.
+ */
+ bool isFullyInited() const;
+ /**
+ * Return true if the SmtEngine is fully initialized and there are no
+ * pending pops.
+ */
+ bool isFullyReady() const;
+ /**
+ * Return true if a notifyCheckSat call has been made, e.g. a query has been
+ * issued to the SmtEngine.
+ */
+ bool isQueryMade() const;
+ /** Return the user context level. */
+ size_t getNumUserLevels() const;
+ /** Get the status of the last check-sat */
+ 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:
+ /** Pushes the user and SAT contexts */
+ void push();
+ /** Pops the user and SAT contexts */
+ void pop();
+ /** Pops the user and SAT contexts to the given level */
+ void popto(int toLevel);
+ /**
+ * Internal push, which processes any pending pops, and pushes (if in
+ * incremental mode).
+ */
+ void internalPush();
+ /**
+ * Internal pop. If immediate is true, this processes any pending pops, and
+ * pops (if in incremental mode). Otherwise, it increments the pending pop
+ * counter and does nothing.
+ */
+ void internalPop(bool immediate = false);
+ /** Reference to the SmtEngine */
+ SmtEngine& d_smt;
+ /** Expr manager context */
+ std::unique_ptr<context::Context> d_context;
+ /** User level context */
+ std::unique_ptr<context::UserContext> d_userContext;
+ /** The context levels of user pushes */
+ std::vector<int> d_userLevels;
+
+ /**
+ * Number of internal pops that have been deferred.
+ */
+ unsigned d_pendingPops;
+
+ /**
+ * Whether or not the SmtEngine is fully initialized (post-construction).
+ * This post-construction initialization is automatically triggered by the
+ * use of the SmtEngine which calls the finishInit method above; e.g. when
+ * the first formula is asserted, a call to simplify() is issued, a scope is
+ * pushed, etc.
+ */
+ bool d_fullyInited;
+
+ /**
+ * Whether or not a notifyCheckSat call has been made, which corresponds to
+ * when a checkEntailed() or checkSatisfiability() has already been
+ * made through the SmtEngine. If true, and incrementalSolving is false,
+ * then attempting an additional checks for satisfiability will fail with
+ * a ModalException during notifyCheckSat.
+ */
+ bool d_queryMade;
+
+ /**
+ * Internal status flag to indicate whether we have been issued a
+ * notifyCheckSat call and have yet to process the "postsolve" methods of
+ * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost.
+ */
+ bool d_needPostsolve;
+
+ /**
+ * Most recent result of last checkSatisfiability/checkEntailed in the
+ * SmtEngine.
+ */
+ Result d_status;
+
+ /**
+ * The expected status of the next satisfiability check.
+ */
+ Result d_expectedStatus;
+
+ /** 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
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \file smt_mode.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Enumeration type for the mode of an SmtEngine.
+ **/
+
+#include "smt/smt_mode.h"
+
+#include <iostream>
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, SmtMode m)
+{
+ switch (m)
+ {
+ case SmtMode::START: out << "START"; break;
+ case SmtMode::ASSERT: out << "ASSERT"; break;
+ case SmtMode::SAT: out << "SAT"; break;
+ case SmtMode::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
+ case SmtMode::UNSAT: out << "UNSAT"; break;
+ case SmtMode::ABDUCT: out << "ABDUCT"; break;
+ case SmtMode::INTERPOL: out << "INTERPOL"; break;
+ default: out << "SmtMode!Unknown"; break;
+ }
+ return out;
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file smt_mode.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Enumeration type for the mode of an SmtEngine.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__SMT__SMT_MODE_H
+#define CVC4__SMT__SMT_MODE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+/**
+ * The mode of the solver, which is an extension of Figure 4.1 on
+ * page 52 of the SMT-LIB version 2.6 standard
+ * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
+ */
+enum class SmtMode
+{
+ // the initial state of the solver
+ START,
+ // normal state of the solver, after assert/push/pop/declare/define
+ ASSERT,
+ // immediately after a check-sat returning "sat"
+ SAT,
+ // immediately after a check-sat returning "unknown"
+ SAT_UNKNOWN,
+ // immediately after a check-sat returning "unsat"
+ UNSAT,
+ // immediately after a successful call to get-abduct
+ ABDUCT,
+ // immediately after a successful call to get-interpol
+ INTERPOL
+};
+/**
+ * Writes a SmtMode to a stream.
+ *
+ * @param out The stream to write to
+ * @param m The mode to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, SmtMode m);
+
+} // namespace CVC4
+
+#endif
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
d_zero = bv::utils::mkZero(16);
// Notice that this unit test uses the theory engine of a created SMT
// engine d_smt. We must ensure that d_smt is properly initialized via
// the following call, which constructs its underlying theory engine.
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
d_theoryEngine = d_smt->getTheoryEngine();
d_satSolver = new FakeSatSolver();
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
}
void tearDown() override
d_em = new ExprManager;
d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
d_rewriter = new ExtendedRewriter(true);
d_nm = NodeManager::currentNM();
// Notice that this unit test uses the theory engine of a created SMT
// engine d_smt. We must ensure that d_smt is properly initialized via
// the following call, which constructs its underlying theory engine.
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]->setOutputChannel(
d_outputChannel);
d_em = new ExprManager;
d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
d_nm = NodeManager::currentNM();
}
// Notice that this unit test uses the theory engine of a created SMT
// engine d_smt. We must ensure that d_smt is properly initialized via
// the following call, which constructs its underlying theory engine.
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
EagerBitblaster* bb = new EagerBitblaster(
dynamic_cast<TheoryBV*>(
d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
// Notice that this unit test uses the theory engine of a created SMT
// engine d_smt. We must ensure that d_smt is properly initialized via
// the following call, which constructs its underlying theory engine.
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
d_theoryEngine = d_smt->getTheoryEngine();
for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) {
delete d_theoryEngine->d_theoryOut[id];
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
}
void BvInstantiatorWhite::tearDown()
d_smt = new SmtEngine(d_em);
d_nm = NodeManager::fromExprManager(d_em);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
}
void tearDown() override
// Notice that this unit test uses the theory engine of a created SMT
// engine d_smt. We must ensure that d_smt is properly initialized via
// the following call, which constructs its underlying theory engine.
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
// guard against duplicate statistics assertion errors
delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN];
delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN];
d_smt = new SmtEngine(d_em);
d_nm = NodeManager::fromExprManager(d_em);
d_scope = new SmtScope(d_smt);
- d_smt->finalOptionsAreSet();
+ d_smt->finishInit();
}
void tearDown() override
projects / cvc5.git / commitdiff