Remove cumulative time limits and cpu time limits (#4711)

This PR removes two things from the resource manager:

cumulative time limits
cpu time limits
Cumulative time limiting has been moved to the binary and is (as before) accessible via --tlimit. As per discussion among the devs, we no longer support time limits based on CPU time and thus everything related to that is removed as well.
Note that this includes the option --cpu-time, removes an argument from SmtEngine::setTimeLimit() and the method SmtEngine::getTimeRemaining() .

1 files changed, 7 insertions, 24 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3ed2b987c..738a6c22a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -775,18 +775,14 @@ class CVC4_PUBLIC SmtEngine
   void setResourceLimit(unsigned long units, bool cumulative = false);
 
   /**
-   * Set a time limit for SmtEngine operations.
+   * Set a per-call time limit for SmtEngine operations.
    *
-   * A cumulative and non-cumulative (per-call) time limit can be
-   * set at the same time.  A call to setTimeLimit() with
-   * cumulative==true replaces any cumulative time limit currently
-   * in effect; a call with cumulative==false replaces any per-call
-   * time limit currently in effect.  Resource limits can be set in
-   * addition to time limits; the SmtEngine obeys both.  That means
-   * that up to four independent limits can control the SmtEngine
-   * at the same time.
+   * A per-call time limit can be set at the same time and replaces
+   * any per-call time limit currently in effect.
+   * Resource limits (either per-call or cumulative) can be set in
+   * addition to a time limit; the SmtEngine obeys all three of them.
    *
-   * Note that the cumulative timer only ticks away when one of the
+   * Note that the per-call timer only ticks away when one of the
    * SmtEngine's workhorse functions (things like assertFormula(),
    * checkEntailed(), checkSat(), and simplify()) are running.
    * Between calls, the timer is still.
@@ -800,11 +796,8 @@ class CVC4_PUBLIC SmtEngine
    * We reserve the right to change this in the future.
    *
    * @param millis the time limit in milliseconds, or 0 for no limit
-   * @param cumulative whether this time limit is to be a cumulative
-   * time limit for all remaining calls into the SmtEngine (true), or
-   * whether it's a per-call time limit (false); the default is false
    */
-  void setTimeLimit(unsigned long millis, bool cumulative = false);
+  void setTimeLimit(unsigned long millis);
 
   /**
    * Get the current resource usage count for this SmtEngine.  This
@@ -826,16 +819,6 @@ class CVC4_PUBLIC SmtEngine
    */
   unsigned long getResourceRemaining() const;
 
-  /**
-   * Get the remaining number of milliseconds that can be consumed by
-   * this SmtEngine according to the currently-set cumulative time limit.
-   * If there is not a cumulative resource limit set, this function
-   * throws a ModalException.
-   *
-   * @throw ModalException
-   */
-  unsigned long getTimeRemaining() const;
-
   /** Permit access to the underlying ExprManager. */
   ExprManager* getExprManager() const { return d_exprManager; }