diff options
| author | ayveejay <41393247+ayveejay@users.noreply.github.com> | 2018-07-24 22:16:16 +0100 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-24 16:16:16 -0500 |
| commit | 25d3eea9614a0882a5c18c455e5a14d118a78dce (patch) | |
| tree | 84242088cee9511a48ccd25030c712f894bc23a8 /src/smt/smt_engine.h | |
| parent | f270410e420d4c464c94c249e107451c5f1341ee (diff) | |
Adding API access methods to get heap/nil expressions when using separation logic (#2194)
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index dd1d1b88a..3536c5b1b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -487,6 +487,16 @@ class CVC4_PUBLIC SmtEngine { Model* getModel(); /** + * When using separation logic, obtain the expression for the heap. + */ + Expr getHeapExpr(); + + /** + * When using separation logic, obtain the expression for nil. + */ + Expr getNilExpr(); + + /** * Get an aspect of the current SMT execution environment. */ CVC4::SExpr getOption(const std::string& key) const |