From: Aina Niemetz Date: Wed, 9 Jun 2021 07:20:14 +0000 (-0700) Subject: docs: Migrate separation logic theory reference. (#6702) X-Git-Tag: cvc5-1.0.0~1624 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b257f55a3051362cb3f86d23c2e90384311faa73;p=cvc5.git docs: Migrate separation logic theory reference. (#6702) This migrates page https://cvc4.github.io/separation-logic. --- 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 `__ +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 )`` | ``solver.mkTerm(Kind::SEP_EMP, x, y);`` | +| | | | +| | | where ``x`` and ``y`` are of sort ```` and ```` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| 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 )`` | ``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 `__. + +.. 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