From 42f4798be4268e65b04d54b5711f5ca896b333ed Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 7 Feb 2022 13:49:31 -0800 Subject: [PATCH] Add user documentation for resource limits (#8058) Though we regularly get questions about how resource limits work, they were entirely undocumented. This PR adds some general explanation to the user docs. --- docs/binary/binary.rst | 1 + docs/binary/resource-limits.rst | 38 +++++++++++++++++++++++++++++++++ src/api/cpp/cvc5.h | 9 ++++---- 3 files changed, 44 insertions(+), 4 deletions(-) create mode 100644 docs/binary/resource-limits.rst diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index 44a177afb..66c23ccd6 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -16,3 +16,4 @@ Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different prog languages options output-tags + resource-limits diff --git a/docs/binary/resource-limits.rst b/docs/binary/resource-limits.rst new file mode 100644 index 000000000..f9fe06b5a --- /dev/null +++ b/docs/binary/resource-limits.rst @@ -0,0 +1,38 @@ +Resource limits +=============== + +cvc5 supports limiting the time or *resources* it uses during solving via the options +:ref:`tlimit `, :ref:`tlimit-per `, +:ref:`rlimit `, and :ref:`rlimit-per `. +All these options take a single non-negative number as an argument where giving zero explicitly disables the respective limit. For time limits the number is interpreted as the number of milliseconds, and for resource limits it indicates the amount of *resources*. + +The limits configured using :ref:`tlimit ` and :ref:`rlimit ` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver ` object, respectively. +In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`checkSatAssuming `, :cpp:func:`checkEntailed `, etc). + +Except for the overall time limit (see below), the limits are checked by cvc5 itself and the solver is in a safe state after exhausting a limit. +Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed. + + +Overall time limit (:ref:`--tlimit `) +-------------------------------------------------------- + +The :ref:`tlimit ` option limits the overall running time of the cvc5 solver binary. +It is implemented using an asynchronous interrupt that is usually managed by the operating system (using `setitimer`). +When this interrupt occurs, cvc5 outputs a corresponding message, prints the current statistics and immediately terminates its process. The same is done when an external resource limiting mechanism is in place, for example `ulimit`. + +This mechanism is inherently unsuited when cvc5 is used within another application process via one of its APIs: therefore, it is only honored when running as a standalone binary. +Setting :ref:`tlimit ` via the API or the `(set-option)` SMT-LIB command has thus no effect. + + +Resource manager and resource spending +-------------------------------------- + +All other limits are enforced centrally by the resource manager as follows. +Whenever certain parts of the solver execute, they instruct the resource manager to *spend* a resource. +As soon as the resource manager realizes that some limit is exhausted (either the resource limit or the per-check time limit is reached), it asynchronously instructs the core solver to interrupt the check. +To not invalidate the internal state of the solver, and allow to use it again after an interrupt, the solver continues its work until it reaches a safe point in one of the core solving components. +Then, it returns `unknown` (with an :cpp:enum:`explanation `). + +The intention of a resource limit is to be a deterministic measure that grows (linearly, if possible) with actual running time. +Resources are spent when lemmas are generated and during a few select events like preprocessing, rewriting, decisions and restarts in the SAT solver, or theory checks. +In case the resource spending does not properly reflect the running time, the weights of the individual resources can be modified using the :ref:`rweight ` option, for example with `--rweight=RestartStep=5`. \ No newline at end of file diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index bb67659df..5c2659190 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2793,13 +2793,14 @@ class CVC5_EXPORT DriverOptions * aliases, whether the option was explicitly set by the user, and information * concerning its value. The `valueInfo` member holds any of the following * alternatives: - * - VoidInfo if the option holds no value (or the value has no native type) - * - ValueInfo if the option is of type bool or std::string, holds the + * - `VoidInfo` if the option holds no value (or the value has no native type) + * - `ValueInfo` if the option is of type `bool` or `std::string`, holds the * current value and the default value. - * - NumberInfo if the option is of type int64_t, uint64_t or double, holds + * - `NumberInfo` if the option is of type `int64_t`, `uint64_t` or `double`, holds * the current and default value, as well as the minimum and maximum. - * - ModeInfo if the option is a mode option, holds the current and default + * - `ModeInfo` if the option is a mode option, holds the current and default * values, as well as a list of valid modes. + * * Additionally, this class provides convenience functions to obtain the * current value of an option in a type-safe manner using boolValue(), * stringValue(), intValue(), uintValue() and doubleValue(). They assert that -- 2.30.2