docs: Add references instead of links in theory reference pages. (#6729)

diff --git a/docs/references.bib b/docs/references.bib
index 50e410e7bce87598f9306d45d5ca9b7afe64e1ec..8e3fd5e69e1c6993c909af60abde7c98f1ec454e 100644 (file)
--- 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 5f02a8bf84bd62aafb6b838f395f891c12cc4afd..1211a43ee63ddeeeff23f5a780840fc0b7667049 100644 (file)
--- 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 c2dcda78e2f9f4f89f8525a3e9320388078e4b61..43c114404617dd49dad2a826db43c75730264367 100644 (file)
--- 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 79838334fabbecc02c59b8c741fcc8d84081ea2a..88671a8379e2c2204b4a6b021414cf1594642c4d 100644 (file)
--- 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                                                                            |