Difference between revisions of "Separation Logic"
| Line 60: | Line 60: | ||
|} | |} | ||
| − | =Examples | + | =Examples= |
The following input on heaps Int -> Int is unsatisfiable: | The following input on heaps Int -> Int is unsatisfiable: | ||
| Line 72: | Line 72: | ||
(check-sat) | (check-sat) | ||
| − | The following input on heaps Int -> Node is satisfiable, where Node denotes | + | The following input on heaps Int -> Node is satisfiable, where Node denotes a user-defined inductive [[Datatypes|datatype]]: |
(set-logic QF_ALL_SUPPORTED) | (set-logic QF_ALL_SUPPORTED) | ||
(set-info :status sat) | (set-info :status sat) | ||
| Line 79: | Line 79: | ||
(declare-const z Int) | (declare-const z Int) | ||
(declare-datatypes () ((Node (node (data Int) (left Int) (right Int))))) | (declare-datatypes () ((Node (node (data Int) (left Int) (right Int))))) | ||
| − | (assert (pto x ( | + | (assert (pto x (node 0 y z))) |
(check-sat) | (check-sat) | ||
Revision as of 12:00, 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 ... op Fn
where "op" is any classical Boolean connective, t1 and t2 are terms in the signature of T of sort Loc and Data respectively, and L is a T-literal. The operator "emp" denotes the empty heap constraint, the operator "pto" denotes the points-to predicate, the operator "sep" denotes separation start and is variadic, and the operator "wand" denote magic wand.
The semantics of these operators are as follows:
Notice that the arguments of "emp" are used to denote the type of the heap and have no meaning otherwise.
The sorts Loc and Data are inferred by CVC4, and must be consistent across all predicates occurring in an input. 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 QF_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);
|
Examples
The following input on heaps Int -> Int is unsatisfiable:
(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) (declare-const a Int) (declare-const b Int) (assert (and (pto x a) (pto x b))) (assert (not (= a b))) (check-sat)
The following input on heaps Int -> Node is satisfiable, where Node denotes a user-defined inductive datatype:
(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) (declare-const y Int) (declare-const z Int) (declare-datatypes () ((Node (node (data Int) (left Int) (right Int))))) (assert (pto x (node 0 y z))) (check-sat)
