diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/_static/custom.css | 10 | ||||
| -rw-r--r-- | docs/api/cpp/class_hierarchy.rst | 45 | ||||
| -rw-r--r-- | docs/api/cpp/cpp.rst | 80 | ||||
| -rw-r--r-- | docs/conf.py.in | 4 | ||||
| -rw-r--r-- | docs/examples/examples.rst | 8 | ||||
| -rw-r--r-- | docs/references.bib | 93 | ||||
| -rw-r--r-- | docs/theories/datatypes.rst | 8 | ||||
| -rw-r--r-- | docs/theories/separation-logic.rst | 7 | ||||
| -rw-r--r-- | docs/theories/sets-and-relations.rst | 6 |
9 files changed, 188 insertions, 73 deletions
diff --git a/docs/_static/custom.css b/docs/_static/custom.css index a5403c295..9d07edeaf 100644 --- a/docs/_static/custom.css +++ b/docs/_static/custom.css @@ -87,3 +87,13 @@ a:hover, a:focus { .highlight .m { color: #ba2121; } + +#c-api-class-hierarchy code { + font-size: 100%; + font-weight: normal; + font-family: "Lato","proxima-nova","Helvetica Neue","Arial","sans-serif"; +} + +.hide-toctree { + display: none; +} diff --git a/docs/api/cpp/class_hierarchy.rst b/docs/api/cpp/class_hierarchy.rst new file mode 100644 index 000000000..3fda2f348 --- /dev/null +++ b/docs/api/cpp/class_hierarchy.rst @@ -0,0 +1,45 @@ +C++ API Class Hierarchy +======================= + +``namespace cvc5::api {`` + + * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` + * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` + + * class :ref:`api/cpp/datatype:datatype` + + * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>` + + * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` + + * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>` + + * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl` + * class :ref:`api/cpp/datatypedecl:datatypedecl` + * class :ref:`api/cpp/datatypeselector:datatypeselector` + + * class :ref:`api/cpp/grammar:grammar` + + * class :ref:`api/cpp/kind:kind` + + * class :ref:`api/cpp/op:op` + + * class :ref:`api/cpp/result:result` + + * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>` + + * class :ref:`api/cpp/roundingmode:roundingmode` + + * class :ref:`api/cpp/solver:solver` + + * class :ref:`api/cpp/sort:sort` + + * class :cpp:class:`Stat <cvc5::api::Stat>` + + * class :cpp:class:`Statistics <cvc5::api::Statistics>` + + * class :ref:`api/cpp/term:term` + + * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>` + +``}`` diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index 8d302d60c..17e121a2c 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -6,63 +6,27 @@ C++ API Documentation .. toctree:: :maxdepth: 2 - datatype - datatypeconstructor - datatypeconstructordecl - datatypedecl - datatypeselector - exceptions - grammar - kind - op - result - roundingmode - solver - sort - statistics - term + class_hierarchy + +.. container:: hide-toctree + + .. toctree:: + :maxdepth: 0 + + datatype + datatypeconstructor + datatypeconstructordecl + datatypedecl + datatypeselector + exceptions + grammar + kind + op + result + roundingmode + solver + sort + statistics + term -Class Hierarchy ---------------- - -* namespace ``cvc5::api`` - - * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` - * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` - - * class :cpp:class:`Datatype <cvc5::api::Datatype>` - - * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>` - - * class :cpp:class:`DatatypeConstructor <cvc5::api::DatatypeConstructor>` - - * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>` - - * class :cpp:class:`DatatypeConstructorDecl <cvc5::api::DatatypeConstructorDecl>` - * class :cpp:class:`DatatypeDecl <cvc5::api::DatatypeDecl>` - * class :cpp:class:`DatatypeSelector <cvc5::api::DatatypeSelector>` - - * class :cpp:class:`Grammar <cvc5::api::Grammar>` - - * enum :cpp:enum:`Kind <cvc5::api::Kind>` - - * class :cpp:class:`Op <cvc5::api::Op>` - - * class :cpp:class:`Result <cvc5::api::Result>` - - * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>` - - * enum :cpp:enum:`RoundingMode <cvc5::api::RoundingMode>` - - * class :cpp:class:`Solver <cvc5::api::Solver>` - - * class :cpp:class:`Sort <cvc5::api::Sort>` - - * class :cpp:class:`Stat <cvc5::api::Stat>` - - * class :cpp:class:`Statistics <cvc5::api::Statistics>` - - * class :cpp:class:`Term <cvc5::api::Term>` - - * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>` diff --git a/docs/conf.py.in b/docs/conf.py.in index 65e880bc9..4447d1441 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -49,6 +49,9 @@ extensions = [ bibtex_bibfiles = ['references.bib'] +# Make sure the target is unique +autosectionlabel_prefix_document = True + # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] @@ -67,6 +70,7 @@ html_theme = 'sphinx_rtd_theme' html_theme_options = {} html_static_path = ['${CMAKE_CURRENT_SOURCE_DIR}/_static/'] html_css_files = ['custom.css'] +html_show_sourcelink = False # -- Breathe configuration --------------------------------------------------- breathe_default_project = "cvc5" diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index 5e17d524b..4132d1545 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -1,13 +1,15 @@ Examples =========== -The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) and input languages can be used. -For every example, the same problem is constructed and solved using different input mechanisms. +The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) +and input languages can be used. +For every example, the same problem is constructed and solved using different +input mechanisms. .. toctree:: :maxdepth: 2 - + helloworld exceptions bitvectors diff --git a/docs/references.bib b/docs/references.bib index 50e410e7b..8e3fd5e69 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -6,3 +6,96 @@ pages={1-84}, doi={10.1109/IEEESTD.2019.8766229} } + +@article{BansalBRT17, + author = {Kshitij Bansal and + Clark W. Barrett and + Andrew Reynolds and + Cesare Tinelli}, + title = {A New Decision Procedure for Finite Sets and Cardinality Constraints + in {SMT}}, + journal = {CoRR}, + volume = {abs/1702.06259}, + year = {2017}, + archivePrefix = {arXiv}, + eprint = {1702.06259}, + timestamp = {Mon, 13 Aug 2018 16:47:11 +0200}, + biburl = {https://dblp.org/rec/journals/corr/BansalBRT17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{MengRTB17, + author = {Baoluo Meng and + Andrew Reynolds and + Cesare Tinelli and + Clark W. Barrett}, + editor = {Leonardo de Moura}, + title = {Relational Constraint Solving in {SMT}}, + booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on + Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {10395}, + pages = {148--165}, + publisher = {Springer}, + year = {2017}, + doi = {10.1007/978-3-319-63046-5_10}, + timestamp = {Wed, 25 Sep 2019 18:19:14 +0200}, + biburl = {https://dblp.org/rec/conf/cade/MengRTB17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{ReynoldsISK16, + author = {Andrew Reynolds and + Radu Iosif and + Cristina Serban and + Tim King}, + editor = {Cyrille Artho and + Axel Legay and + Doron Peled}, + title = {A Decision Procedure for Separation Logic in {SMT}}, + booktitle = {Automated Technology for Verification and Analysis - 14th International + Symposium, {ATVA} 2016, Chiba, Japan, October 17-20, 2016, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {9938}, + pages = {244--261}, + year = {2016}, + doi = {10.1007/978-3-319-46520-3_16}, + timestamp = {Tue, 14 May 2019 10:00:49 +0200}, + biburl = {https://dblp.org/rec/conf/atva/ReynoldsIS016.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{ReynoldsB15, + author = {Andrew Reynolds and + Jasmin Christian Blanchette}, + editor = {Amy P. Felty and + Aart Middeldorp}, + title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers}, + booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on + Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {9195}, + pages = {197--213}, + publisher = {Springer}, + year = {2015}, + doi = {10.1007/978-3-319-21401-6_13}, + timestamp = {Tue, 14 May 2019 10:00:39 +0200}, + biburl = {https://dblp.org/rec/conf/cade/ReynoldsB15.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{BarrettST07, + author = {Clark W. Barrett and + Igor Shikanian and + Cesare Tinelli}, + title = {An Abstract Decision Procedure for a Theory of Inductive Data Types}, + journal = {J. Satisf. Boolean Model. Comput.}, + volume = {3}, + number = {1-2}, + pages = {21--46}, + year = {2007}, + doi = {10.3233/sat190028}, + timestamp = {Mon, 17 Aug 2020 18:32:39 +0200}, + biburl = {https://dblp.org/rec/journals/jsat/BarrettST07.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 5f02a8bf8..1211a43ee 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -45,8 +45,8 @@ evaluate to true iff their argument has top-symbol ``C``. Semantics --------- -The decision procedure for inductive datatypes can be found -`here <http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-JSAT-07.pdf>`__. +The decision procedure for inductive datatypes is described in +:cite:`BarrettST07`. Example Declarations -------------------- @@ -150,8 +150,8 @@ For example: Codatatypes ----------- -cvc5 also supports co-inductive datatypes, as described -`here <http://homepage.cs.uiowa.edu/~ajreynol/cade15.pdf>`__. +cvc5 also supports co-inductive datatypes, as described in +:cite:`ReynoldsB15`. The syntax for declaring mutually recursive coinductive datatype blocks is identical to inductive datatypes, except that ``declare-datatypes`` is replaced diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index c2dcda78e..86f802ef8 100644 --- a/docs/theories/separation-logic.rst +++ b/docs/theories/separation-logic.rst @@ -7,10 +7,9 @@ language. Signature --------- -Given a (decidable) base theory :math:`T`, cvc5 has a -`decision procedure <https://cvc4.github.io/publications/2016/RIS+16.pdf>`__ -for quantifier-free :math:`SL(T)_{Loc,Data}` formulas, where :math:`Loc` and -:math:`Data` are any sort belonging to :math:`T`. +Given a (decidable) base theory :math:`T`, cvc5 implements a decision procedure +for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsISK16`, +where :math:`Loc` and :math:`Data` are any sort belonging to :math:`T`. A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar: diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 79838334f..88671a837 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -20,8 +20,7 @@ The source code of these examples is available at: Below is a short summary of the sorts, constants, functions and -predicates. For more details, see -`this paper at IJCAR 2016 <https://cvc4.github.io/publications/2016/BRBT16.pdf>`__. +predicates. More details can be found in :cite:`BansalBRT17`. For the C++ API examples in the table below, we assume that we have created a `cvc5::api::Solver solver` object. @@ -151,8 +150,7 @@ Example: For reference, below is a short summary of the sorts, constants, functions and predicates. -For more details, see -`this paper at CADE 2017 <https://cvc4.github.io/publications/2017/MRT+17.pdf>`__. +More details can be found in :cite:`MengRTB17`. +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ | | SMTLIB language | C++ API | |