Separation Logic

From CVC4
Revision as of 11:42, 28 November 2016 by Ajreynol (Talk | contribs)

Jump to: navigation, search

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