From 9079d4482aaeba27232fa01fefa4cb7ff8f88787 Mon Sep 17 00:00:00 2001 From: Cesare Tinelli Date: Fri, 1 Apr 2022 22:09:22 -0500 Subject: [PATCH] Minor edits in docs. (#8540) --- docs/index.rst | 5 +++-- docs/output-tags.rst | 4 ++-- docs/resource-limits.rst | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/docs/index.rst b/docs/index.rst index 746b18dac..f61319890 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -2,8 +2,9 @@ cvc5 Documentation ================== **cvc5** is an open-source automatic theorem prover for Satisfiability Modulo -Theories (SMT) problems in a large number of theories and their combination. -**cvc5** is the successor of `CVC4 `_ and is +Theories (SMT) problems that supports a large number of theories and their +combination. +It is the successor of `CVC4 `_ and is intended to be an open and extensible SMT engine. This space provides all documentation related to using cvc5. diff --git a/docs/output-tags.rst b/docs/output-tags.rst index 689e03ab8..51bce612a 100644 --- a/docs/output-tags.rst +++ b/docs/output-tags.rst @@ -2,9 +2,9 @@ Output tags =========== cvc5 supports printing information about certain aspects of the solving process -that is intended for regular users. These can be enabled using the +that is intended for regular users. This feature can be enabled using the :ref:`output ` option. -As of now, the following output tags are supported: +The following output tags are currently supported: .. include-build-file:: output_tags_generated.rst diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst index 8a3848bd4..f9d5b338b 100644 --- a/docs/resource-limits.rst +++ b/docs/resource-limits.rst @@ -9,7 +9,7 @@ All these options take a single non-negative number as an argument where giving 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. +Except for the overall time limit (see below), the limits are checked by cvc5 itself. This means that the solver remains in a safe state after a limit has been reached. 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. -- 2.30.2