From 5982baed871b6bef18a352a3bb31186f4a364932 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 1 Apr 2022 15:53:53 -0700 Subject: [PATCH] docs: Document UnknownExplanation. (#8508) --- docs/api/cpp/cpp.rst | 9 ++++----- docs/api/cpp/roundingmode.rst | 5 ----- docs/api/cpp/unknownexplanation.rst | 6 ++++++ docs/resource-limits.rst | 4 ++-- src/api/cpp/cvc5_types.h | 12 ++++++++++++ 5 files changed, 24 insertions(+), 12 deletions(-) create mode 100644 docs/api/cpp/unknownexplanation.rst diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index 6b17d1222..65704ed56 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -30,6 +30,7 @@ For most applications, the :cpp:class:`Solver ` class is the main statistics synthresult term + unknownexplanation Class hierarchy @@ -52,14 +53,9 @@ Class hierarchy * class :ref:`api/cpp/datatypeselector:datatypeselector` * class :ref:`api/cpp/driveroptions:driveroptions` * class :ref:`api/cpp/grammar:grammar` - * class :ref:`api/cpp/kind:kind` * class :ref:`api/cpp/op:op` * class :ref:`api/cpp/optioninfo:optioninfo` * class :ref:`api/cpp/result:result` - - * enum :cpp:enum:`UnknownExplanation ` - - * class :ref:`api/cpp/roundingmode:roundingmode` * class :ref:`api/cpp/solver:solver` * class :ref:`api/cpp/sort:sort` * class :cpp:class:`Stat ` @@ -69,6 +65,9 @@ Class hierarchy * class :cpp:class:`const_iterator ` + * enum :ref:`api/cpp/kind:kind` + * enum :ref:`api/cpp/roundingmode:roundingmode` + * enum :ref:`api/cpp/unknownexplanation:unknownexplanation` * modes enums :ref:`api/cpp/modes:modes` ``}`` diff --git a/docs/api/cpp/roundingmode.rst b/docs/api/cpp/roundingmode.rst index 6626157eb..6edad90a7 100644 --- a/docs/api/cpp/roundingmode.rst +++ b/docs/api/cpp/roundingmode.rst @@ -3,8 +3,3 @@ RoundingMode .. doxygenenum:: cvc5::RoundingMode :project: cvc5 - -.. doxygenstruct:: std::hash< cvc5::RoundingMode > - :project: std - :members: - :undoc-members: diff --git a/docs/api/cpp/unknownexplanation.rst b/docs/api/cpp/unknownexplanation.rst new file mode 100644 index 000000000..20091596d --- /dev/null +++ b/docs/api/cpp/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +================== + +.. doxygenenum:: cvc5::UnknownExplanation + :project: cvc5 + diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst index bb4e3fbdf..8a3848bd4 100644 --- a/docs/resource-limits.rst +++ b/docs/resource-limits.rst @@ -31,8 +31,8 @@ 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 `). +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 +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``. diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index db99cf3c8..c05ce0698 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -28,14 +28,26 @@ namespace cvc5 { */ enum UnknownExplanation { + /** + * Full satisfiability check required (e.g., if only preprocessing was + * performed). + */ REQUIRES_FULL_CHECK, + /** Incomplete theory solver. */ INCOMPLETE, + /** Time limit reached. */ TIMEOUT, + /** Resource limit reached. */ RESOURCEOUT, + /** Memory limit reached. */ MEMOUT, + /** Solver was interrupted. */ INTERRUPTED, + /** Unsupported feature encountered. */ UNSUPPORTED, + /** Other reason. */ OTHER, + /** No specific reason given. */ UNKNOWN_REASON }; -- 2.30.2