docs: Migrate separation logic theory reference. (#6702)

This migrates page https://cvc4.github.io/separation-logic.

3 files changed, 165 insertions, 1 deletions

diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py
index 5dd54d006..2ce860e39 100644
--- a/docs/ext/smtliblexer.py
+++ b/docs/ext/smtliblexer.py
@@ -9,13 +9,17 @@ class SmtLibLexer(RegexLexer):
         'root': [
             (r'QF_BV', token.Text),
             (r'QF_UFDT', token.Text),
-            (r'ALL_SUPPORTED', token.Text),
+            (r'ALL', token.Text),
+            (r'QF_ALL', token.Text),
+            (r'set-info', token.Keyword),
             (r'set-logic', token.Keyword),
             (r'set-option', token.Keyword),
             (r'declare-codatatypes', token.Keyword),
             (r'declare-const', token.Keyword),
+            (r'declare-datatype', token.Keyword),
             (r'declare-datatypes', token.Keyword),
             (r'declare-fun', token.Keyword),
+            (r'declare-sort', token.Keyword),
             (r'define-fun', token.Keyword),
             (r'assert\b', token.Keyword),
             (r'check-sat-assuming', token.Keyword),
@@ -32,6 +36,7 @@ class SmtLibLexer(RegexLexer):
             (r':produce-models', token.Name.Attribute),
             (r':produce-unsat-cores', token.Name.Attribute),
             (r':produce-unsat-assumptions', token.Name.Attribute),
+            (r':status', token.Name.Attribute),
             (r'!', token.Name.Attribute),
             (r'BitVec', token.Name.Attribute),
             (r'RNE', token.Name.Attribute),
@@ -48,11 +53,15 @@ class SmtLibLexer(RegexLexer):
             (r'bvult', token.Operator),
             (r'bvule', token.Operator),
             (r'bvsdiv', token.Operator),
+            (r'emp', token.Operator),
             (r'extract', token.Operator),
             (r'fp.gt', token.Operator),
             (r'ite', token.Operator),
             (r'mkTuple', token.Operator),
             (r'to_fp_unsigned', token.Operator),
+            (r'pto', token.Operator),
+            (r'sep', token.Operator),
+            (r'wand', token.Operator),
             (r'\+zero', token.Operator),
             (r'#b[0-1]+', token.Text),
             (r'bv[0-9]+', token.Text),
diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst
new file mode 100644
index 000000000..c2dcda78e
--- /dev/null
+++ b/docs/theories/separation-logic.rst
@@ -0,0 +1,154 @@
+Theory Reference: Separation Logic
+==================================
+
+cvc5 supports a syntax for separation logic as an extension of the SMT-LIB 2
+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`.
+
+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
+
+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``
+denotes the points-to predicate, the operator ``sep`` denotes separation start
+and is variadic, and the operator ``wand`` denote magic wand.
+
+Semantics
+---------
+
+A satisfiability relation :math:`I,h \models_{SL} \varphi` is defined for
+:math:`SL(T)_{Loc,Data}` formulas :math:`\varphi`,
+where :math:`I` is an interpretation, and :math:`h` is a heap.
+
+The semantics of separation logic operators are as follows:
+
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL} L`                                  | Iff  | :math:`I \models L`, if :math:`L` is a :math:`T`-literal                            |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (emp :math:`t \ u`)                | Iff  | :math:`h = \emptyset`                                                               |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (pto :math:`t \ u`)                | Iff  | :math:`h = \{(t^I,u^I)\} \text{ and } t^I\not=nil^I`                                |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (sep :math:`\phi_1 \ldots \phi_n)` | Iff  | there exist heaps :math:`h_1,\ldots,h_n` s.t. :math:`h=h_1\uplus \ldots \uplus h_n` |
+|                                                             |      |                                                                                     |
+|                                                             |      | and :math:`I,h_i \models_{SL} \phi_i, i = 1,\ldots,n`                               |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (wand :math:`\phi_1 \ \phi_2`)     | Iff  | for all heaps :math:`h'` if :math:`h'\#h` and :math:`I,h' \models_{SL} \phi_1`      |
+|                                                             |      |                                                                                     |
+|                                                             |      | then :math:`I,h'\uplus h \models_{SL} \phi_2`                                       |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+
+where :math:`h_1 \uplus \ldots \uplus h_n` denotes the disjoint union of heaps
+:math:`h_1, \ldots, h_n` and :math:`h'\#h` denotes that heaps :math:`h'` and
+:math:`h` are disjoint, and :math:`nil` is a distinguished variable of sort
+: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.
+
+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
+a :cpp:class:`cvc5::api::Solver` object.
+
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+|                      | SMTLIB language                              | C++ API                                                            |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Logic String         | ``(set-logic QF_ALL)``                       | ``solver.setLogic("QF_ALL");``                                     |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Empty Heap           | ``(_ emp <Sort_1> <Sort_2>)``                | ``solver.mkTerm(Kind::SEP_EMP, x, y);``                            |
+|                      |                                              |                                                                    |
+|                      |                                              | where ``x`` and ``y`` are of sort ``<Sort_1>`` and ``<Sort_2>``    |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Points-To            | ``(pto x y)``                                | ``solver.mkTerm(Kind::SEP_PTO, x, y);``                            |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Separation Star      | ``(sep c1 .. cn)``                           | ``solver.mkTerm(Kind::SEP_STAR, {c1, ..., cn});``                  |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Magic Wand           | ``(wand c1 c1)``                             | ``solver.mkTerm(Kind::SEP_WAND, c1, c2);``                         |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Nil Element          | ``(as nil <Sort>)``                          | ``solver.mkSepNil(cvc5::api::Sort sort);``                         |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+
+
+Examples
+--------
+
+The following input on heaps ``Int -> Int`` is unsatisfiable:
+
+.. code:: smtlib
+
+  (set-logic QF_ALL)
+  (set-info :status unsat)
+  (declare-const x Int)
+  (declare-const a Int)
+  (declare-const b Int)
+  (assert (and (pto x a) (pto x b)))
+  (assert (not (= a b)))
+  (check-sat)
+
+
+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.
+
+.. code:: smtlib
+
+  (set-logic QF_ALL)
+  (set-info :status sat)
+  (declare-sort U 0)
+  (declare-const x U)
+  (declare-const a Int)
+  (assert (and (not (_ emp U Int)) (pto x a)))
+  (check-sat)
+
+The following input on heaps ``Int -> Node`` is satisfiable, where ``Node``
+denotes a user-defined inductive `datatypes <datatypes>`__.
+
+.. code:: smtlib
+
+  (set-logic QF_ALL)
+  (set-info :status sat)
+  (declare-const x Int)
+  (declare-const y Int)
+  (declare-const z Int)
+  (declare-datatype Node ((node (data Int) (left Int) (right Int))))
+  (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:
+
+  .. code:: smtlib
+
+    (set-logic QF_ALL)
+    (declare-sort U 0)
+    (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.
diff --git a/docs/theory.rst b/docs/theory.rst
index 45be41b2e..f0b25aea4 100644
--- a/docs/theory.rst
+++ b/docs/theory.rst
@@ -5,3 +5,4 @@ Theory References
    :maxdepth: 1
 
    theories/datatypes
+   theories/separation-logic