Separation Logic

CVC4 supports a syntax for separation logic as an extension of the *.smt2 language.

Signature and semantics

Given a base theory T, CVC4 supports reasoning about SL(T)_{Loc,Data} formulas, where "Loc" and "Data" are any sort belonging to T. A SL(T)_{Loc,Data} formula is one from the following grammar:

 F : L | (emp t1 t2) | (pto t1 t2) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op F2

where "op" is any standard Boolean connective, t1 and t2 are terms in the signature of T of sort Loc and Data respectively, and L is a T-literal.

Notice that the sorts Loc and Data are fixed. Thus, CVC4 does not accept an input such as:

 (declare-sort U 0)
 (declare-const x U)
 (assert (and (pto x 0) (pto 1 2)))

since the sorts of the first arguments of the points-to predicates do not agree.

Syntax

Separation logic in CVC4 requires the "all supported" logic:

 (set-logic ALL_SUPPORTED)

The syntax for the operators of separation logic is summarized in the following table:

	CVC language	SMTLIB language	C++ API
Empty heap	N/A	(emp X Y)	em.mkExpr(kind::SEP_EMP, X, Y);
Points-to	N/A	(pto X Y)	em.mkExpr(kind::SEP_PTO, X, Y);
Separation star	N/A	(sep C1 ... Cn)	em.mkExpr(kind::SEP_STAR, C1, ..., Cn);
Magic wand	N/A	(wand C1 C2)	em.mkExpr(kind::SEP_WAND, C1, C2);
Nil element	N/A	(as nil T)	em.mkUniqueVar(T,kind::SEP_NIL);