diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 11:29:47 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-13 11:29:47 -0500 |
| commit | 8fd4ac8bff4aa7a4b4e04e35f6944d303d5cf498 (patch) | |
| tree | 0344ffc01fbc5d27faf19e0ef0a0de36551145eb /src/theory/logic_info.h | |
| parent | 47b910a85de71b6617e4d1d210dcb57de597961b (diff) | |
Properly implement logic info for separation logic (#3176)
Diffstat (limited to 'src/theory/logic_info.h')
| -rw-r--r-- | src/theory/logic_info.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 969810a6f..a19936c34 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -206,6 +206,11 @@ public: * This means enabling quantifiers, datatypes, UF, integers, and higher order. */ void enableSygus(); + /** + * Enable everything that is needed for separation logic. This means enabling + * the theories of separation logic, UF and sets. + */ + void enableSeparationLogic(); // these are for arithmetic |