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, 9 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 9519624b7..6256360e4 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -249,6 +249,15 @@ class Theory {
   }
 
   /**
+   * Set separation logic heap. This is called when the location and data
+   * types for separation logic are determined. This should be called at
+   * most once, before solving.
+   *
+   * This currently should be overridden by the separation logic theory only.
+   */
+  virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
+
+  /**
    * The theory that owns the uninterpreted sort.
    */
   static TheoryId s_uninterpretedSortOwner;