Theory Reference: Separation Logic ¶

cvc5 supports a syntax for separation logic as an extension of the SMT-LIB 2.6 language.

Signature ¶

Given a (decidable) base theory \(T\) , cvc5 implements a decision procedure for quantifier-free \(SL(T)_{Loc,Data}\) formulas [ RISK16 ] , where \(Loc\) and \(Data\) are any sort belonging to \(T\) .

A \(SL(T)_{Loc,Data}\) formula is one from the following grammar:

            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 \(T\) of sort \(Loc\) and \(Data\) respectively, and \(L\) is a \(T\) -literal.

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.

Semantics ¶

A satisfiability relation \(I,h \models_{SL} \varphi\) is defined for \(SL(T)_{Loc,Data}\) formulas \(\varphi\) , where \(I\) is an interpretation, and \(h\) is a heap.

The semantics of separation logic operators are as follows:

\(I,h \models_{SL} L\)	Iff	\(I \models L\) , if \(L\) is a \(T\) -literal
\(I,h \models_{SL}\) (emp \(t \ u\) )	Iff	\(h = \emptyset\)
\(I,h \models_{SL}\) (pto \(t \ u\) )	Iff	\(h = \{(t^I,u^I)\} \text{ and } t^I\not=nil^I\)
\(I,h \models_{SL}\) (sep \(\phi_1 \ldots \phi_n)\)	Iff	there exist heaps \(h_1,\ldots,h_n\) s.t. \(h=h_1\uplus \ldots \uplus h_n\) and \(I,h_i \models_{SL} \phi_i, i = 1,\ldots,n\)
\(I,h \models_{SL}\) (wand \(\phi_1 \ \phi_2\) )	Iff	for all heaps \(h'\) if \(h'\#h\) and \(I,h' \models_{SL} \phi_1\) then \(I,h'\uplus h \models_{SL} \phi_2\)

where \(h_1 \uplus \ldots \uplus h_n\) denotes the disjoint union of heaps \(h_1, \ldots, h_n\) and \(h'\#h\) denotes that heaps \(h'\) and \(h\) are disjoint, and \(nil\) is a distinguished variable of sort \(Loc\) . All classical Boolean connectives are interpreted as expected.

Syntax ¶

Separation logic in cvc5 requires the QF_ALL logic, and for the types of the heap to be declared via the declare-heap command:

            (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 [ BFT17 ] ). This command sets the location type of the heap \(Loc\) to \(T1\) and the data type \(Data\) to \(T2\) , where \(T1\) and \(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 a cvc5::Solver object.

	SMTLIB language	C++ API
Logic String	`(set-logic QF_ALL)`	`solver.setLogic("QF_ALL");`
Empty Heap	`sep.emp`	`solver.mkSepEmp();` 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 sep.nil <Sort>)`	`solver.mkSepNil(cvc5::Sort sort);`

Examples ¶

The following input on heaps Int -> Int is unsatisfiable:

            (set-logic QF_ALL)
(declare-heap (Int Int))
(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 sep.emp) is satisfied by heaps U -> Int whose domain is non-empty.

            (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 sep.emp) (pto x a)))
(check-sat)

           

The following input on heaps Int -> Node is satisfiable, where Node denotes a user-defined inductive Theory Reference: Datatypes .

            (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))))
(declare-heap (Int Node))
(assert (pto x (node 0 y z)))
(check-sat)

           

Note

Given a separation logic input, the sorts \(Loc\) and \(Data\) declared via the declare-heap command must match all separation logic predicates in the input. cvc5 does not accept an input such as:

             (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 second points-to predicate uses Int for its location type.