This PR contains a variety of fixed and improvements to the documentation.
- `Doxygen <https://www.doxygen.nl>`_
- `Sphinx <https://www.sphinx-doc.org>`_,
+ `sphinx-rtd-theme <https://sphinx-rtd-theme.readthedocs.io/>`_,
`sphinx-tabs <https://sphinx-tabs.readthedocs.io/>`_,
- `sphinxcontrib-bibtex <https://sphinxcontrib-bibtex.readthedocs.io>`_
+ `sphinxcontrib-bibtex <https://sphinxcontrib-bibtex.readthedocs.io>`_,
+ `sphinxcontrib-programoutput <https://sphinxcontrib-programoutput.readthedocs.io>`_
- `Breathe <https://breathe.readthedocs.io>`_
To build the documentation, configure cvc5 with ``./configure.sh --docs`` and
.. toctree::
- :maxdepth: 2
+ :hidden:
quickstart
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
Using the flag :ref:`proof-format-mode=dot <lbl-option-proof-format-mode>`, cvc5 outputs proofs in the DOT format.
-The DOT format is a graph description language (see e.g. a description `here <https://en.wikipedia.org/wiki/DOT_(graph_description_language)>`_.). It can be used, among other things, for visualization.
+The DOT format is a graph description language (see e.g. `this description <https://en.wikipedia.org/wiki/DOT_(graph_description_language)>`_). 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 <https://ufmg-smite.github.io/proof-visualizer>`_. 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 <https://ufmg-smite.github.io/proof-visualizer>`_. 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.
+++ /dev/null
-Proof format: Lean
-==================
\ No newline at end of file
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 <lbl-option-proof-granularity>` 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
reasoning. Here is a comprehensive description of the :doc:`proof rules
<proof_rules>`.
+.. toctree::
+ :hidden:
+
+ proof_rules
+
Optionally cvc5 can convert and output its internal proofs into the following
external formats:
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}
The term:
.. code:: smtlib
+
((_ update Sij) t u)
is equivalent to replacing the field of ``t`` denoted by the selector ``Sij``
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
bags
datatypes
separation-logic
+ sequences
sets-and-relations
transcendentals
* (block-model)
*
* Requires enabling option
- * :ref:`produce-models <lbl-option-produce-models>`
- * and setting option
- * :ref:`block-models <lbl-option-block-models>`
- * to a mode other than ``none``.
+ * :ref:`produce-models <lbl-option-produce-models>`.
* \endverbatim
*
* @warning This method is experimental and may change in future versions.
*
* - ``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:
*
* .. 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``
* .. code:: smtlib
*
* (match l (((cons h t) h) (nil 0)))
+ *
* is represented by the AST
*
* .. code:: lisp
* .. 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
*
* \rst
* .. note:: Should only be used as a child of
- * :cpp:enumerator`INST_PATTERN_LIST`.
+ * :cpp:enumerator:`INST_PATTERN_LIST`.
* \endrst
*
* - Arity: ``n > 0``
"""
.. warning:: This method is experimental and may change in future
versions.
+
:return: True if this datatype is parametric.
"""
return self.cd.isParametric()
"""
.. warning:: This method is experimental and may change in future
versions.
+
:return: True if this datatype corresponds to a record.
"""
return self.cd.isRecord()
"""
Get some information about the given option.
Returns the information provided by the C++
- :cpp:func:`OptionInfo <cvc5::OptionInfo>` as a dictionary.
+ :cpp:class:`OptionInfo <cvc5::OptionInfo>` as a dictionary.
:return: Information about the given option.
"""
.. 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.
cdef Term result = Term(self)
result.cterm = self.csolver.getInterpolantNext()
return result
+
+
def getAbduct(self, Term conj, Grammar grammar=None):
"""
Get an abduct.
.. 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.
Requires enabling option
:ref:`produce-models <lbl-option-produce-models>`
- and setting option
- :ref:`block-models <lbl-option-block-models>`
to a mode other than ``none``.
.. warning:: This method is experimental and may change in future
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.
"""
.. 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()
"""
:return: The sort the cardinality constraint is for and its upper
bound.
+
.. warning:: This method is experimental and may change in future
versions.
"""
projects / cvc5.git / commitdiff