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 | |
parent | f270410e420d4c464c94c249e107451c5f1341ee (diff) |
Adding API access methods to get heap/nil expressions when using separation logic (#2194)
-rw-r--r-- | src/smt/smt_engine.cpp | 24 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 10 |
2 files changed, 34 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 71256e3d8..a275c7d63 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5251,6 +5251,30 @@ Model* SmtEngine::getModel() { return m; } +Expr SmtEngine::getHeapExpr() { + NodeManagerScope nms(d_nodeManager); + Expr heap; + Expr nil; // we don't actually use this + Model* m = getModel(); + if (m->getHeapModel( heap, nil )) + { + return heap; + } + InternalError("SmtEngine::getHeapExpr(): failed to obtain heap expression from theory model."); +} + +Expr SmtEngine::getNilExpr() { + NodeManagerScope nms(d_nodeManager); + Expr heap; // we don't actually use this + Expr nil; + Model* m = getModel(); + if (m->getHeapModel( heap, nil )) + { + return nil; + } + InternalError("SmtEngine::getNilExpr(): failed to obtain nil expression from theory model."); +} + void SmtEngine::checkUnsatCore() { Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off"); 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 |