From 39bd56468f08040f91ca1ed93f4741d8e76d6c38 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Feb 2022 20:09:52 +0100 Subject: [PATCH] Remove long obsolete unsafe interrupt exception (#8139) 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. --- src/main/driver_unified.cpp | 16 ++---- src/parser/parser.h | 1 - src/prop/minisat/core/Solver.cc | 3 +- src/prop/prop_engine.h | 2 +- src/smt/assertions.h | 2 +- src/smt/command.cpp | 37 -------------- src/smt/solver_engine.cpp | 74 +++++++++++---------------- src/smt/solver_engine.h | 11 ++-- src/theory/theory_engine.h | 1 - src/util/CMakeLists.txt | 1 - src/util/resource_manager.h | 8 +-- src/util/unsafe_interrupt_exception.h | 46 ----------------- test/unit/test_smt.h | 1 - 13 files changed, 44 insertions(+), 159 deletions(-) delete mode 100644 src/util/unsafe_interrupt_exception.h diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 418828382..73aa3ae7d 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -182,12 +182,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) << 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; @@ -226,13 +221,8 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) 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) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 1d9eb97ae..43edbf299 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -31,7 +31,6 @@ #include "parser/input.h" #include "parser/parse_op.h" #include "parser/parser_exception.h" -#include "util/unsafe_interrupt_exception.h" namespace cvc5 { diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 2b3974511..2d79e2900 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -2158,8 +2158,7 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to) 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 = diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 0497c6738..96cd2ce1d 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -255,7 +255,7 @@ class PropEngine : protected EnvObj /** * 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); diff --git a/src/smt/assertions.h b/src/smt/assertions.h index acc5f2a4c..ade5bbc81 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -80,7 +80,7 @@ class Assertions : protected EnvObj * 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); /** diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e22c39d0e..7a81aa0a0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -38,7 +38,6 @@ #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; @@ -344,10 +343,6 @@ void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->assertFormula(d_term); d_commandStatus = CommandSuccess::instance(); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -377,10 +372,6 @@ void PushCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->push(); d_commandStatus = CommandSuccess::instance(); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -409,10 +400,6 @@ void PopCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->pop(); d_commandStatus = CommandSuccess::instance(); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1509,10 +1496,6 @@ void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm) 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()); @@ -1588,10 +1571,6 @@ void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = new CommandRecoverableFailure(e.what()); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1667,10 +1646,6 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = new CommandRecoverableFailure(e.what()); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1728,10 +1703,6 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = new CommandRecoverableFailure(e.what()); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1783,10 +1754,6 @@ void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = new CommandRecoverableFailure(e.what()); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1837,10 +1804,6 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = new CommandRecoverableFailure(e.what()); } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index e67877fad..83d4a903f 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -771,60 +771,44 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions, { 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) diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 3d7dd5be7..a0c81f5fa 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -332,7 +332,7 @@ class CVC5_EXPORT SolverEngine * 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); @@ -477,7 +477,7 @@ class CVC5_EXPORT SolverEngine * 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? @@ -489,7 +489,7 @@ class CVC5_EXPORT SolverEngine * * @param n The node to expand * - * @throw TypeCheckingException, LogicException, UnsafeInterruptException + * @throw TypeCheckingException, LogicException */ Node expandDefinitions(const Node& n); @@ -498,8 +498,7 @@ class CVC5_EXPORT SolverEngine * 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; @@ -726,7 +725,7 @@ class CVC5_EXPORT SolverEngine /** * Push a user-level context. - * throw@ ModalException, LogicException, UnsafeInterruptException + * throw@ ModalException, LogicException */ void push(); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6b1da1078..f8a8fd736 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -39,7 +39,6 @@ #include "theory/valuation.h" #include "util/hash.h" #include "util/statistics_stats.h" -#include "util/unsafe_interrupt_exception.h" namespace cvc5 { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index bfa67d9c1..c8940ae94 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -78,7 +78,6 @@ libcvc5_add_sources( string.h uninterpreted_sort_value.cpp uninterpreted_sort_value.h - unsafe_interrupt_exception.h utility.cpp utility.h ) diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 27771c22c..117953b0a 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -147,13 +147,13 @@ class ResourceManager 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); diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h deleted file mode 100644 index 16364cba2..000000000 --- a/src/util/unsafe_interrupt_exception.h +++ /dev/null @@ -1,46 +0,0 @@ -/****************************************************************************** - * 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 */ diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index f97b01931..feb41822a 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -30,7 +30,6 @@ #include "theory/theory_state.h" #include "theory/valuation.h" #include "util/resource_manager.h" -#include "util/unsafe_interrupt_exception.h" namespace cvc5 { namespace test { -- 2.30.2