From a9ae5086d11ca05caaf18d9709ac63951897cd18 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 4 Apr 2022 12:09:47 -0700 Subject: [PATCH] Various improvements and fixes in the documentation (#8551) This PR contains a variety of fixed and improvements to the documentation. --- INSTALL.rst | 4 +++- docs/binary/binary.rst | 2 +- docs/proofs/output_alethe.rst | 4 ++++ docs/proofs/output_dot.rst | 4 ++-- docs/proofs/output_lean.rst | 2 -- docs/proofs/output_lfsc.rst | 4 ++++ docs/proofs/proofs.rst | 5 +++++ docs/references.bib | 4 ++-- docs/theories/datatypes.rst | 2 ++ docs/theories/theories.rst | 1 + src/api/cpp/cvc5.h | 5 +---- src/api/cpp/cvc5_kind.h | 8 ++++++-- src/api/python/cvc5.pxi | 16 ++++++++++------ 13 files changed, 41 insertions(+), 20 deletions(-) delete mode 100644 docs/proofs/output_lean.rst diff --git a/INSTALL.rst b/INSTALL.rst index 5a8454d2c..b70913274 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -223,8 +223,10 @@ Building the API documentation of cvc5 requires the following dependencies: - `Doxygen `_ - `Sphinx `_, + `sphinx-rtd-theme `_, `sphinx-tabs `_, - `sphinxcontrib-bibtex `_ + `sphinxcontrib-bibtex `_, + `sphinxcontrib-programoutput `_ - `Breathe `_ To build the documentation, configure cvc5 with ``./configure.sh --docs`` and diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index f51160bcb..7788daf2b 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -16,6 +16,6 @@ Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different prog .. toctree:: - :maxdepth: 2 + :hidden: quickstart diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst index 937d7d1d4..b5cf4bdf2 100644 --- a/docs/proofs/output_alethe.rst +++ b/docs/proofs/output_alethe.rst @@ -20,3 +20,7 @@ available `here `_. Currently, only the theory of equality with uninterpreted functions, parts of the theory of arithmetic and parts of the theory of quantifiers are supported in cvc5's Alethe proofs. + +A simple example of cvc5 producing a proof in the Alethe proof format: + +.. run-command:: bin/cvc5 --dump-proofs --proof-format-mode=alethe --simplification=none --dag-thresh=0 --proof-granularity=theory-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2 diff --git a/docs/proofs/output_dot.rst b/docs/proofs/output_dot.rst index 30665cd72..968102461 100644 --- a/docs/proofs/output_dot.rst +++ b/docs/proofs/output_dot.rst @@ -3,6 +3,6 @@ Proof format: DOT Using the flag :ref:`proof-format-mode=dot `, cvc5 outputs proofs in the DOT format. -The DOT format is a graph description language (see e.g. a description `here `_.). It can be used, among other things, for visualization. +The DOT format is a graph description language (see e.g. `this description `_). It can be used, among other things, for visualization. -We leverage this format for visualizing cvc5 proofs, in the internal calculus, as a graph. One can use a default dot visualizer or the dedicated proof visualizer available `here `_. It suffices to upload the DOT proof outputted by cvc5, saved into a file. The visualizer offers several custom features, such as fold/unfold subproofs, coloring nodes, and stepwise expansion of let terms. +We leverage this format for visualizing cvc5 proofs, in the internal calculus, as a graph. One can use a default dot visualizer or the dedicated proof visualizer `available here `_. It suffices to upload the DOT proof outputted by cvc5, saved into a file. The visualizer offers several custom features, such as fold/unfold subproofs, coloring nodes, and stepwise expansion of let terms. diff --git a/docs/proofs/output_lean.rst b/docs/proofs/output_lean.rst deleted file mode 100644 index 6eaea77bc..000000000 --- a/docs/proofs/output_lean.rst +++ /dev/null @@ -1,2 +0,0 @@ -Proof format: Lean -================== \ No newline at end of file diff --git a/docs/proofs/output_lfsc.rst b/docs/proofs/output_lfsc.rst index 3b47e3962..f763498e8 100644 --- a/docs/proofs/output_lfsc.rst +++ b/docs/proofs/output_lfsc.rst @@ -12,3 +12,7 @@ LFSC is a meta-framework, meaning that the proof rules used by cvc5 are defined Note that several proof rules in the internal calculus are not yet supported in LFSC signatures, and are instead printed as `trust` steps in the LFSC proof. A trust step proves an arbitrary formula with no provided justification. The LFSC proof contains warnings for which proof rules from the internal calculus were recorded as trust steps in the LFSC proof. For more fine-grained proofs, the additional option :ref:`proof-granularity=theory-rewrite ` should be passed to cvc5. This often will result in LFSC proofs with more detail, and whose trust steps correspond only to equalities corresponding to theory rewrites. + +A simple example of cvc5 producing a proof in LFSC proof format: + +.. run-command:: bin/cvc5 --dump-proofs --proof-format-mode=lfsc --proof-granularity=theory-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2 diff --git a/docs/proofs/proofs.rst b/docs/proofs/proofs.rst index face73c30..6f1e09f66 100644 --- a/docs/proofs/proofs.rst +++ b/docs/proofs/proofs.rst @@ -5,6 +5,11 @@ cvc5 produces proofs in an internal proof calculus that faithfully reflects its reasoning. Here is a comprehensive description of the :doc:`proof rules `. +.. toctree:: + :hidden: + + proof_rules + Optionally cvc5 can convert and output its internal proofs into the following external formats: diff --git a/docs/references.bib b/docs/references.bib index 35224aa51..86f36c3f3 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -242,8 +242,8 @@ pages = {450--467}, publisher = {Springer}, year = {2021}, - url = {https://doi.org/10.1007/978-3-030-79876-5\_26}, - doi = {10.1007/978-3-030-79876-5\_26}, + url = {https://doi.org/10.1007/978-3-030-79876-5_26}, + doi = {10.1007/978-3-030-79876-5_26}, timestamp = {Mon, 12 Jul 2021 14:18:46 +0200}, biburl = {https://dblp.org/rec/conf/cade/SchurrFD21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 4106e31fe..2072be7bd 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -118,6 +118,7 @@ Datatype updaters are a (non-standard) extension available in datatype logics. The term: .. code:: smtlib + ((_ update Sij) t u) is equivalent to replacing the field of ``t`` denoted by the selector ``Sij`` @@ -125,6 +126,7 @@ with the value ``u``, or ``t`` itself if that selector does not apply to the constructor symbol of ``t``. For example, for the list datatype, we have that: .. code:: smtlib + ((_ update head) (cons 4 nil) 7) = (cons 7 nil) ((_ update tail) (cons 4 nil) (cons 5 nil)) = (cons 4 (cons 5 nil)) ((_ update head) nil 5) = nil diff --git a/docs/theories/theories.rst b/docs/theories/theories.rst index f1b980bc4..fd00cc658 100644 --- a/docs/theories/theories.rst +++ b/docs/theories/theories.rst @@ -32,5 +32,6 @@ Non-standard or extended theories bags datatypes separation-logic + sequences sets-and-relations transcendentals diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 44a30bfed..d9f816a6e 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4568,10 +4568,7 @@ class CVC5_EXPORT Solver * (block-model) * * Requires enabling option - * :ref:`produce-models ` - * and setting option - * :ref:`block-models ` - * to a mode other than ``none``. + * :ref:`produce-models `. * \endverbatim * * @warning This method is experimental and may change in future versions. diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 7d405891a..c350c377a 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -238,7 +238,7 @@ enum Kind : int32_t * * - ``1:`` Term of kind :cpp:enumerator:`VARIABLE_LIST` * - ``2:`` Term of Sort Bool (the body of the witness) - * - ``3:`` (optional) Term of kind :cpp:enumerator:`INST_PATTERN`_LIST + * - ``3:`` (optional) Term of kind :cpp:enumerator:`INST_PATTERN_LIST` * * - Create Term of this Kind with: * @@ -474,12 +474,14 @@ enum Kind : int32_t * .. code:: smtlib * * ((_ iand k) i_1 i_2) + * * is equivalent to * * .. code:: smtlib * * ((_ iand k) i_1 i_2) * (bv2int (bvand ((_ int2bv k) i_1) ((_ int2bv k) i_2))) + * * for all integers ``i_1``, ``i_2``. * * - Arity: ``2`` @@ -2620,6 +2622,7 @@ enum Kind : int32_t * .. code:: smtlib * * (match l (((cons h t) h) (nil 0))) + * * is represented by the AST * * .. code:: lisp @@ -4771,6 +4774,7 @@ enum Kind : int32_t * .. code:: smtlib * * (seq.++ (seq.unit c1) ... (seq.unit cn)) + * * where :math:`n \leq 0` and :math:`c_1, ..., c_n` are constants of some * sort. The elements can be extracted with Term::getSequenceValue(). * \endrst @@ -4895,7 +4899,7 @@ enum Kind : int32_t * * \rst * .. note:: Should only be used as a child of - * :cpp:enumerator`INST_PATTERN_LIST`. + * :cpp:enumerator:`INST_PATTERN_LIST`. * \endrst * * - Arity: ``n > 0`` diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index a02adec33..880be79d0 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -157,6 +157,7 @@ cdef class Datatype: """ .. warning:: This method is experimental and may change in future versions. + :return: True if this datatype is parametric. """ return self.cd.isParametric() @@ -177,6 +178,7 @@ cdef class Datatype: """ .. warning:: This method is experimental and may change in future versions. + :return: True if this datatype corresponds to a record. """ return self.cd.isRecord() @@ -2218,7 +2220,7 @@ cdef class Solver: """ Get some information about the given option. Returns the information provided by the C++ - :cpp:func:`OptionInfo ` as a dictionary. + :cpp:class:`OptionInfo ` as a dictionary. :return: Information about the given option. """ @@ -2711,6 +2713,7 @@ cdef class Solver: .. warning:: This method is experimental and may change in future versions. + :param conj: The conjecture term. :param grammar: A grammar for the inteprolant. :return: The interpolant. @@ -2751,6 +2754,8 @@ cdef class Solver: cdef Term result = Term(self) result.cterm = self.csolver.getInterpolantNext() return result + + def getAbduct(self, Term conj, Grammar grammar=None): """ Get an abduct. @@ -2767,6 +2772,7 @@ cdef class Solver: .. warning:: This method is experimental and may change in future versions. + :param conj: The conjecture term. :param grammar: A grammar for the abduct. :return: The abduct. @@ -2819,8 +2825,6 @@ cdef class Solver: Requires enabling option :ref:`produce-models ` - and setting option - :ref:`block-models ` to a mode other than ``none``. .. warning:: This method is experimental and may change in future @@ -3068,7 +3072,7 @@ cdef class Sort: Is this a record sort? .. warning:: This method is experimental and may change in future - versions. + versions. :return: True if the sort is a record sort. """ @@ -3614,8 +3618,7 @@ cdef class Term: .. note:: - This is safe to call when :py:meth:`hasOp()` returns True. - + This is safe to call when :py:meth:`hasOp()` returns True. """ cdef Op op = Op(self.solver) op.cop = self.cterm.getOp() @@ -3927,6 +3930,7 @@ cdef class Term: """ :return: The sort the cardinality constraint is for and its upper bound. + .. warning:: This method is experimental and may change in future versions. """ -- 2.30.2