1 files changed, 17 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index de0daffd0..0661ae918 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -309,6 +309,23 @@ class CVC4_PUBLIC SmtEngine
    */
   Result blockModelValues(const std::vector<Node>& exprs);
 
+  /**
+   * Declare heap. For smt2 inputs, this is called when the command
+   * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
+   * location type and dataT is the data type for the heap. This command should
+   * be executed only once, and must be invoked before solving separation logic
+   * inputs.
+   */
+  void declareSepHeap(TypeNode locT, TypeNode dataT);
+
+  /**
+   * Get the separation heap types, which extracts which types were passed to
+   * the method above.
+   *
+   * @return true if the separation logic heap types have been declared.
+   */
+  bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT);
+
   /** When using separation logic, obtain the expression for the heap.  */
   Node getSepHeapExpr();