Difference between revisions of "Separation Logic"
From CVC4
(Created page with "The format for separation logic in the *.smt2 is ...") |
|||
| Line 1: | Line 1: | ||
| − | + | =Logic= | |
| + | CVC4 supports a syntax for separation logic as an extension of the *.smt2 language. | ||
| + | To enable separation logic, use the "all supported" logic: | ||
| + | (set-logic ALL_SUPPORTED) | ||
| + | |||
| + | =Syntax= | ||
| + | The syntax for the operators of separation logic (points-to, emp, star, wand) is as follows: | ||
Revision as of 10:21, 28 November 2016
Logic
CVC4 supports a syntax for separation logic as an extension of the *.smt2 language. To enable separation logic, use the "all supported" logic:
(set-logic ALL_SUPPORTED)
Syntax
The syntax for the operators of separation logic (points-to, emp, star, wand) is as follows:
