Difference between revisions of "Separation Logic"
From CVC4
Line 5: | Line 5: | ||
=Syntax= | =Syntax= | ||
− | The syntax for the operators of separation logic | + | The syntax for the operators of separation logic is summarized in the following table: |
{| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse" | {| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse" |
Revision as of 11:38, 28 November 2016
Logic
CVC4 supports a syntax for separation logic as an extension of the *.smt2 language. Separation logic in CVC4 requires the "all supported" logic:
(set-logic ALL_SUPPORTED)
Syntax
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);
|