Updates for the theory reference for separation logic (#8366)

diff --git a/docs/references.bib b/docs/references.bib
index 12eecc8ba1fc5f9362271f552760a3d7fe8979c8..478b694a0596b37ad3768f56e3cd5f4015be8ac4 100644 (file)
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -119,3 +119,13 @@
   biburl    = {https://dblp.org/rec/journals/jsat/BarrettST07.bib},
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
+
+
+@TECHREPORT{BarFT-RR-17,
+  author =      {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+  title =       {{The SMT-LIB Standard: Version 2.6}},
+  institution =         {Department of Computer Science, The University of Iowa},
+  year =        2017,
+  note =        {Available at {\tt www.SMT-LIB.org}}
+}
+

diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst
index 36d3a165fdf7a24907b5bdd1979523844ebd1271..a971c76fb7e0ffc65ebfd96bb481e09fb88655fa 100644 (file)
--- a/docs/theories/separation-logic.rst
+++ b/docs/theories/separation-logic.rst
@@ -1,7 +1,7 @@
 Theory Reference: Separation Logic
 ==================================
 
-cvc5 supports a syntax for separation logic as an extension of the SMT-LIB 2
+cvc5 supports a syntax for separation logic as an extension of the SMT-LIB 2.6
 language.
 
 Signature
@@ -15,13 +15,13 @@ A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar:
 
 .. code::
 
-  F : L | (emp t u) | (pto t u) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op ... op Fn
+  F : L | sep.emp | (pto t u) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op ... op Fn
 
 where ``op`` is any classical Boolean connective, ``t`` and ``u`` are terms
 built from symbols in the signature of :math:`T` of sort :math:`Loc` and
 :math:`Data` respectively, and :math:`L` is a :math:`T`-literal.
 
-The operator ``emp`` denotes the empty heap constraint, the operator ``pto``
+The operator ``sep.emp`` denotes the empty heap constraint, the operator ``pto``
 denotes the points-to predicate, the operator ``sep`` denotes separation start
 and is variadic, and the operator ``wand`` denote magic wand.
 
@@ -56,18 +56,19 @@ where :math:`h_1 \uplus \ldots \uplus h_n` denotes the disjoint union of heaps
 :math:`Loc`.
 All classical Boolean connectives are interpreted as expected.
 
-.. note::
-  The arguments of ``emp`` are used to denote the sort of the heap and have no
-  meaning otherwise.
-
 Syntax
 ------
 
-Separation logic in cvc5 requires the ``QF_ALL`` logic.
+Separation logic in cvc5 requires the ``QF_ALL`` logic, and for the types of the heap to be declared via the `declare-heap` command:
+
+.. code:: smtlib
+
+  (declare-heap (T1 T2))
+
+This command must be executed when the solver is in its Start mode (see page 52 of the SMT-LIB 2.6 standard :cite:`BarFT-RR-17`). This command sets the location type of the heap :math:`Loc` to :math:`T1` and the data type :math:`Data` to :math:`T2`, where :math:`T1` and :math:`T2` are any defined types. This command can only be executed once in any context, and is reset only via a `reset` command.
 
 The syntax for the operators of separation logic is summarized in the following
-table.
-For the C++ API examples in this table, we assume that we have created
+table. For the C++ API examples in this table, we assume that we have created
 a :cpp:class:`cvc5::api::Solver` object.
 
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
@@ -75,7 +76,7 @@ a :cpp:class:`cvc5::api::Solver` object.
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 | Logic String         | ``(set-logic QF_ALL)``                       | ``solver.setLogic("QF_ALL");``                                     |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Empty Heap           | ``(_ emp <Sort_1> <Sort_2>)``                | ``solver.mkTerm(Kind::SEP_EMP, x, y);``                            |
+| Empty Heap           | ``sep.emp``                                  | ``solver.mkSepEmp();``                                             |
 |                      |                                              |                                                                    |
 |                      |                                              | where ``x`` and ``y`` are of sort ``<Sort_1>`` and ``<Sort_2>``    |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
@@ -85,7 +86,7 @@ a :cpp:class:`cvc5::api::Solver` object.
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 | Magic Wand           | ``(wand c1 c1)``                             | ``solver.mkTerm(Kind::SEP_WAND, c1, c2);``                         |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Nil Element          | ``(as nil <Sort>)``                          | ``solver.mkSepNil(cvc5::api::Sort sort);``                         |
+| Nil Element          | ``(as sep.nil <Sort>)``                      | ``solver.mkSepNil(cvc5::api::Sort sort);``                         |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 
 
@@ -97,6 +98,7 @@ The following input on heaps ``Int -> Int`` is unsatisfiable:
 .. code:: smtlib
 
   (set-logic QF_ALL)
+  (declare-heap (Int Int))
   (set-info :status unsat)
   (declare-const x Int)
   (declare-const a Int)
@@ -107,17 +109,18 @@ The following input on heaps ``Int -> Int`` is unsatisfiable:
 
 
 The following input on heaps ``U -> Int`` is satisfiable. Notice that the
-formula ``(not (emp x 0))`` is satisfied by heaps ``U -> Int`` (the sorts of
-``x`` and ``0`` respectively) whose domain is non-empty.
+formula ``(not sep.emp)`` is satisfied by heaps ``U -> Int`` whose domain is
+non-empty.
 
 .. code:: smtlib
 
   (set-logic QF_ALL)
   (set-info :status sat)
   (declare-sort U 0)
+  (declare-heap (U Int))
   (declare-const x U)
   (declare-const a Int)
-  (assert (and (not (_ emp U Int)) (pto x a)))
+  (assert (and (not sep.emp) (pto x a)))
   (check-sat)
 
 The following input on heaps ``Int -> Node`` is satisfiable, where ``Node``
@@ -131,23 +134,23 @@ denotes a user-defined inductive :doc:`datatypes`.
   (declare-const y Int)
   (declare-const z Int)
   (declare-datatype Node ((node (data Int) (left Int) (right Int))))
+  (declare-heap (Int Node))
   (assert (pto x (node 0 y z)))
   (check-sat)
 
 .. note::
 
-  Given a separation logic input, the sorts :math:`Loc` and :math:`Data` are
-  inferred by cvc5, and must be consistent across all predicates occurring in
-  an input.
-  cvc5 does not accept an input such as:
+  Given a separation logic input, the sorts :math:`Loc` and :math:`Data`
+  declared via the `declare-heap` command must match all separation logic
+  predicates in the input. cvc5 does not accept an input such as:
 
   .. code:: smtlib
 
     (set-logic QF_ALL)
     (declare-sort U 0)
+    (declare-heap (U Int))
     (declare-const x U)
     (assert (and (pto x 0) (pto 1 2)))
     (check-sat)
 
-  since the sorts of the first arguments of the points-to predicates do not
-  agree.
+  since the second points-to predicate uses Int for its location type.