Theory Reference: Separation Logic

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


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.


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\)


\(I \models L\) , if \(L\) is a \(T\) -literal

\(I,h \models_{SL}\) (emp \(t \ u\) )


\(h = \emptyset\)

\(I,h \models_{SL}\) (pto \(t \ u\) )


\(h = \{(t^I,u^I)\} \text{ and } t^I\not=nil^I\)

\(I,h \models_{SL}\) (sep \(\phi_1 \ldots \phi_n)\)


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\) )


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.


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


Logic String

(set-logic QF_ALL)


Empty Heap



where x and y are of sort <Sort_1> and <Sort_2>


(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);


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)))

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)))

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)))


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)))

since the second points-to predicate uses Int for its location type.