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} inputs.

 pto : 

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