From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 23 Feb 2022 19:09:52 +0000 (+0100)
Subject: Remove long obsolete unsafe interrupt exception (#8139)
X-Git-Tag: cvc5-1.0.0~396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39bd56468f08040f91ca1ed93f4741d8e76d6c38;p=cvc5.git

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.
---

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<api::Solver>& 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<api::Solver>& 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<Node>& 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 {