Difference between revisions of "Separation Logic"
From CVC4
| Line 1: | Line 1: | ||
=Logic= | =Logic= | ||
CVC4 supports a syntax for separation logic as an extension of the *.smt2 language. | 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) | (set-logic ALL_SUPPORTED) | ||
=Syntax= | =Syntax= | ||
| − | The syntax for the operators of separation logic (points-to, emp, star, wand) is | + | The syntax for the operators of separation logic (points-to, emp, star, wand) is summarized in the following table: |
| + | |||
| + | {| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse" | ||
| + | |- | ||
| + | ! | ||
| + | ! CVC language | ||
| + | ! SMTLIB language | ||
| + | ! C++ API | ||
| + | |- | ||
| + | | Empty heap | ||
| + | | <code>N/A</code> | ||
| + | | <code>('''emp''' X Y)</code> | ||
| + | | <code></code> | ||
| + | |- | ||
| + | | Points-to | ||
| + | | <code>N/A</code> | ||
| + | | <code>('''pto''' X Y)</code> | ||
| + | | <code>em.mkExpr('''kind::SEP_PTO''', X, Y);</code> | ||
| + | |- | ||
| + | | Separation star | ||
| + | | <code>N/A</code> | ||
| + | | <code>('''sep''' C1 ... Cn)</code> | ||
| + | | <code>em.mkExpr('''kind::SEP_STAR''', C1, ..., Cn);</code> | ||
| + | |- | ||
| + | | Magic wand | ||
| + | | <code>N/A</code> | ||
| + | | <code>('''wand''' C1 C2)</code> | ||
| + | | <code>em.mkExpr('''kind::SEP_WAND''', C1, C2);</code> | ||
| + | |- | ||
| + | | Nil element | ||
| + | | <code>N/A</code> | ||
| + | | <code>('''as nil''' T)</code> | ||
| + | | <code>em.mk;</code> | ||
| + | |} | ||
Revision as of 10:26, 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 (points-to, emp, star, wand) is summarized in the following table:
| CVC language | SMTLIB language | C++ API | |
|---|---|---|---|
| Empty heap | N/A
|
(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.mk;
|
