From d46b2c596befb493905d0037553fc0d0b5871df3 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 7 Jan 2022 09:49:22 -0800 Subject: [PATCH] Some minor improvements to the theory references (#7881) --- docs/index.rst | 2 +- docs/theories/datatypes.rst | 2 ++ docs/theories/sets-and-relations.rst | 45 ++++++++++++---------------- docs/theories/theories.rst | 13 ++++++++ docs/theory.rst | 10 ------- 5 files changed, 35 insertions(+), 37 deletions(-) create mode 100644 docs/theories/theories.rst delete mode 100644 docs/theory.rst diff --git a/docs/index.rst b/docs/index.rst index 27b7b728d..133ad958c 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -18,6 +18,6 @@ Table of Contents binary/binary api/api examples/examples - theory + theories/theories references genindex diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 1211a43ee..c9a15ad24 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -1,6 +1,8 @@ Theory Reference: Datatypes =========================== +cvc5 implements some extensions to the support for datatypes in SMT-LIB 2. + Logic ----- diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 8dd76dbfb..5184603be 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -4,25 +4,8 @@ Theory Reference: Sets and Relations Finite Sets ----------- -cvc5 supports the theory of finite sets. -The simplest way to get a sense of the syntax is to look at an example: - -.. api-examples:: - /api/cpp/sets.cpp - /api/java/Sets.java - /api/python/sets.py - /api/smtlib/sets.smt2 - -The source code of these examples is available at: - -* `SMT-LIB 2 language example `__ -* `C++ API example `__ -* `Java API example `__ -* `Python API example `__ - - -Below is a short summary of the sorts, constants, functions and -predicates. More details can be found in :cite:`BansalBRT17`. +cvc5 supports the theory of finite sets using the following sorts, constants, +functions and 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. @@ -144,16 +127,21 @@ Above, notice that we were able to find a model for the universe set of sort The reason for that is that making this formula (and similar ones) `unsat` is counter-intuitive when quantifiers are present. -Finite Relations ----------------- -Example: +Below is a more extensive example on how to use finite sets: .. api-examples:: - /api/smtlib/relations.smt2 + /api/cpp/sets.cpp + /api/java/Sets.java + /api/python/sets.py + /api/smtlib/sets.smt2 -For reference, below is a short summary of the sorts, constants, functions and -predicates. + +Finite Relations +---------------- + +cvc5 also supports the theory of finite relations, using the following sorts, +constants, functions and predicates. More details can be found in :cite:`MengRTB17`. +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ @@ -173,7 +161,7 @@ More details can be found in :cite:`MengRTB17`. +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ | Tuple Constructor | ``(tuple , ..., )`` | ``Term t = solver.mkTuple({, ..., }, {Term_1>, ..., });`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ -| Tuple Selector | ``((_ tuple_select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` | +| Tuple Selector | ``((_ tuple_select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` | | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | @@ -195,3 +183,8 @@ More details can be found in :cite:`MengRTB17`. +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ | Product | ``(rel.product X Y)`` | ``Term t = solver.mkTerm(Kind::RELATION_PRODUCT, X, Y);`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ + +Example: + +.. api-examples:: + /api/smtlib/relations.smt2 diff --git a/docs/theories/theories.rst b/docs/theories/theories.rst new file mode 100644 index 000000000..dd4f2c8a1 --- /dev/null +++ b/docs/theories/theories.rst @@ -0,0 +1,13 @@ +Theory References +================= + +cvc5 implements several theories that are not (yet) standardized in SMT-LIB, or +that extend beyond the respective standardized theory. + +.. toctree:: + :maxdepth: 1 + + datatypes + separation-logic + sets-and-relations + transcendentals diff --git a/docs/theory.rst b/docs/theory.rst deleted file mode 100644 index 075de8ba4..000000000 --- a/docs/theory.rst +++ /dev/null @@ -1,10 +0,0 @@ -Theory References -================= - -.. toctree:: - :maxdepth: 1 - - theories/datatypes - theories/separation-logic - theories/sets-and-relations - theories/transcendentals -- 2.30.2