Add proper support for the declare-heap command for separation logic (#5405)

This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.

This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.

Fixes #5343, fixes #4926.

Work towards CVC4/cvc4-wishues#22.

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();