Difference between revisions of "Separation Logic"
From CVC4
| Line 5: | Line 5: | ||
Given a base theory T, CVC4 supports reasoning about SL(T)_{Loc,Data} formulas, where "Loc" and "Data" are any sort belonging to T. | 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: | A SL(T)_{Loc,Data} formula is one from the following grammar: | ||
| − | F : L | emp | (pto t1 t2) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op F2 | + | 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. | + | 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= | =Syntax= | ||
Revision as of 12:49, 28 November 2016
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);
|
