From d8565b7d6b9817de525fea2c8eb04536476bb6b2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Mar 2022 16:24:52 -0500 Subject: [PATCH] Updates for the theory reference for separation logic (#8366) --- docs/references.bib | 10 +++++++ docs/theories/separation-logic.rst | 45 ++++++++++++++++-------------- 2 files changed, 34 insertions(+), 21 deletions(-) diff --git a/docs/references.bib b/docs/references.bib index 12eecc8ba..478b694a0 100644 --- 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 36d3a165f..a971c76fb 100644 --- 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 )`` | ``solver.mkTerm(Kind::SEP_EMP, x, y);`` | +| Empty Heap | ``sep.emp`` | ``solver.mkSepEmp();`` | | | | | | | | where ``x`` and ``y`` are of sort ```` and ```` | +----------------------+----------------------------------------------+--------------------------------------------------------------------+ @@ -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 )`` | ``solver.mkSepNil(cvc5::api::Sort sort);`` | +| Nil Element | ``(as sep.nil )`` | ``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. -- 2.30.2