Theory Reference: Separation Logic
cvc5 supports a syntax for separation logic as an extension of the SMTLIB 2.6 language.
Signature
Given a (decidable) base theory \(T\) , cvc5 implements a decision procedure for quantifierfree \(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 pointsto 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
declareheap
command:
(declareheap (T1 T2))
This command must be executed when the solver is in its Start mode (see page 52 of the SMTLIB 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 


Empty Heap 

where

PointsTo 


Separation Star 


Magic Wand 


Nil Element 


Examples
The following input on heaps
Int
>
Int
is unsatisfiable:
(setlogic QF_ALL)
(declareheap (Int Int))
(setinfo :status unsat)
(declareconst x Int)
(declareconst a Int)
(declareconst b Int)
(assert (and (pto x a) (pto x b)))
(assert (not (= a b)))
(checksat)
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
nonempty.
(setlogic QF_ALL)
(setinfo :status sat)
(declaresort U 0)
(declareheap (U Int))
(declareconst x U)
(declareconst a Int)
(assert (and (not sep.emp) (pto x a)))
(checksat)
The following input on heaps
Int
>
Node
is satisfiable, where
Node
denotes a userdefined inductive
Theory Reference: Datatypes
.
(setlogic QF_ALL)
(setinfo :status sat)
(declareconst x Int)
(declareconst y Int)
(declareconst z Int)
(declaredatatype Node ((node (data Int) (left Int) (right Int))))
(declareheap (Int Node))
(assert (pto x (node 0 y z)))
(checksat)
Note
Given a separation logic input, the sorts \(Loc\) and \(Data\) declared via the declareheap command must match all separation logic predicates in the input. cvc5 does not accept an input such as:
(setlogic QF_ALL)
(declaresort U 0)
(declareheap (U Int))
(declareconst x U)
(assert (and (pto x 0) (pto 1 2)))
(checksat)
since the second pointsto predicate uses Int for its location type.