diff options
| -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 |
4 files changed, 102 insertions, 12 deletions
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..43c114404 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:`ReynoldsIS016`, +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 | |