We used to use UnsafeInterruptException to deal with resource outs in the resource manager: when resources were exhausted, we would throw this exception that was catched in the core solver engine. This had the significant downside of leaving the solver in a potentially inconsistent state. We moved away from using it long ago in #4732.
What remained was the UnsafeInterruptException class itself and a bunch of places that still catch this exception that is no longer thrown anywhere.
This PR removes this class for good.
<< Configuration::copyright() << std::endl;
while(true) {
- try {
- cmd.reset(shell.readCommand());
- } catch(UnsafeInterruptException& e) {
- dopts.out() << CommandInterrupted();
- break;
- }
+ cmd.reset(shell.readCommand());
if (cmd == nullptr)
break;
status = pExecutor->doCommand(cmd) && status;
pExecutor->reset();
break;
}
- try {
- cmd.reset(parser->nextCommand());
- if (cmd == nullptr) break;
- } catch (UnsafeInterruptException& e) {
- interrupted = true;
- continue;
- }
+ cmd.reset(parser->nextCommand());
+ if (cmd == nullptr) break;
status = pExecutor->doCommand(cmd);
if (cmd->interrupted() && status == 0) {
#include "parser/input.h"
#include "parser/parse_op.h"
#include "parser/parser_exception.h"
-#include "util/unsafe_interrupt_exception.h"
namespace cvc5 {
inline bool Solver::withinBudget(Resource r) const
{
Assert(d_proxy);
- // spendResource sets async_interrupt or throws UnsafeInterruptException
- // depending on whether hard-limit is enabled
+ // spendResource may interrupt the solver via a callback.
d_proxy->spendResource(r);
bool within_budget =
/**
* Informs the ResourceManager that a resource has been spent. If out of
- * resources, can throw an UnsafeInterruptException exception.
+ * resources, the solver is interrupted using a callback.
*/
void spendResource(Resource r);
* literals and conjunction of literals. Returns false if
* immediately determined to be inconsistent.
*
- * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+ * @throw TypeCheckingException, LogicException
*/
void assertFormula(const Node& n);
/**
#include "proof/unsat_core.h"
#include "smt/model.h"
#include "util/smt2_quote_string.h"
-#include "util/unsafe_interrupt_exception.h"
#include "util/utility.h"
using namespace std;
solver->assertFormula(d_term);
d_commandStatus = CommandSuccess::instance();
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
solver->push();
d_commandStatus = CommandSuccess::instance();
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
solver->pop();
d_commandStatus = CommandSuccess::instance();
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
d_result = solver->simplify(d_term);
d_commandStatus = CommandSuccess::instance();
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
- catch (UnsafeInterruptException& e)
- {
- d_commandStatus = new CommandInterrupted();
- }
catch (exception& e)
{
d_commandStatus = new CommandFailure(e.what());
{
Result r;
- try
- {
- SolverEngineScope smts(this);
- finishInit();
+ SolverEngineScope smts(this);
+ finishInit();
- Trace("smt") << "SolverEngine::"
- << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
- << assumptions << ")" << endl;
- // check the satisfiability with the solver object
- r = d_smtSolver->checkSatisfiability(
- *d_asserts.get(), assumptions, isEntailmentCheck);
+ Trace("smt") << "SolverEngine::"
+ << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
+ << assumptions << ")" << endl;
+ // check the satisfiability with the solver object
+ r = d_smtSolver->checkSatisfiability(
+ *d_asserts.get(), assumptions, isEntailmentCheck);
- Trace("smt") << "SolverEngine::"
- << (isEntailmentCheck ? "query" : "checkSat") << "("
- << assumptions << ") => " << r << endl;
+ Trace("smt") << "SolverEngine::"
+ << (isEntailmentCheck ? "query" : "checkSat") << "("
+ << assumptions << ") => " << r << endl;
- // Check that SAT results generate a model correctly.
- if (d_env->getOptions().smt.checkModels)
- {
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
- {
- checkModel();
- }
- }
- // Check that UNSAT results generate a proof correctly.
- if (d_env->getOptions().smt.checkProofs)
+ // Check that SAT results generate a model correctly.
+ if (d_env->getOptions().smt.checkModels)
+ {
+ if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- checkProof();
- }
+ checkModel();
}
- // Check that UNSAT results generate an unsat core correctly.
- if (d_env->getOptions().smt.checkUnsatCores)
+ }
+ // Check that UNSAT results generate a proof correctly.
+ if (d_env->getOptions().smt.checkProofs)
+ {
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
- checkUnsatCore();
- }
+ checkProof();
}
}
- catch (const UnsafeInterruptException& e)
+ // Check that UNSAT results generate an unsat core correctly.
+ if (d_env->getOptions().smt.checkUnsatCores)
{
- AlwaysAssert(getResourceManager()->out());
- // Notice that we do not notify the state of this result. If we wanted to
- // make the solver resume a working state after an interupt, then we would
- // implement a different callback and use it here, e.g.
- // d_state.notifyCheckSatInterupt.
- Result::UnknownExplanation why = getResourceManager()->outOfResources()
- ? Result::RESOURCEOUT
- : Result::TIMEOUT;
-
- r = Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
+ checkUnsatCore();
+ }
}
if (d_env->getOptions().base.statisticsEveryQuery)
* immediately determined to be inconsistent. Note this formula will
* be included in the unsat core when applicable.
*
- * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+ * @throw TypeCheckingException, LogicException
*/
Result assertFormula(const Node& formula);
* definitions, assertions, and the current partial model, if one
* has been constructed. It also involves theory normalization.
*
- * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+ * @throw TypeCheckingException, LogicException
*
* @todo (design) is this meant to give an equivalent or an
* equisatisfiable formula?
*
* @param n The node to expand
*
- * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+ * @throw TypeCheckingException, LogicException
*/
Node expandDefinitions(const Node& n);
* or NOT_ENTAILED query). Only permitted if the SolverEngine is set to
* operate interactively and produce-models is on.
*
- * @throw ModalException, TypeCheckingException, LogicException,
- * UnsafeInterruptException
+ * @throw ModalException, TypeCheckingException, LogicException
*/
Node getValue(const Node& e) const;
/**
* Push a user-level context.
- * throw@ ModalException, LogicException, UnsafeInterruptException
+ * throw@ ModalException, LogicException
*/
void push();
#include "theory/valuation.h"
#include "util/hash.h"
#include "util/statistics_stats.h"
-#include "util/unsafe_interrupt_exception.h"
namespace cvc5 {
string.h
uninterpreted_sort_value.cpp
uninterpreted_sort_value.h
- unsafe_interrupt_exception.h
utility.cpp
utility.h
)
uint64_t getResourceRemaining() const;
/**
- * Spends a given resource. Throws an UnsafeInterruptException if there are
- * no remaining resources.
+ * Spends a given resource. Calls the listener to interrupt the solver if
+ * there are no remaining resources.
*/
void spendResource(Resource r);
/**
- * Spends a given resource. Throws an UnsafeInterruptException if there are
- * no remaining resources.
+ * Spends a given resource. Calls the listener to interrupt the solver if
+ * there are no remaining resources.
*/
void spendResource(theory::InferenceId iid);
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Liana Hadarean, Mathias Preiner, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * An exception that is thrown when the solver is out of time/resources
- * and is interrupted in an unsafe state.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
-#define CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
-
-#include "base/exception.h"
-#include "cvc5_export.h"
-
-namespace cvc5 {
-
-class CVC5_EXPORT UnsafeInterruptException : public cvc5::Exception
-{
- public:
- UnsafeInterruptException() :
- Exception("Interrupted in unsafe state due to "
- "time/resource limit.") {
- }
-
- UnsafeInterruptException(const std::string& msg) :
- Exception(msg) {
- }
-
- UnsafeInterruptException(const char* msg) :
- Exception(msg) {
- }
-}; /* class UnsafeInterruptException */
-
-} // namespace cvc5
-
-#endif /* CVC5__UNSAFE_INTERRUPT_EXCEPTION_H */
#include "theory/theory_state.h"
#include "theory/valuation.h"
#include "util/resource_manager.h"
-#include "util/unsafe_interrupt_exception.h"
namespace cvc5 {
namespace test {
projects / cvc5.git / commitdiff