Difference between revisions of "Separation Logic"

From CVC4
Jump to: navigation, search
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 11: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);