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

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e47dbbc6f..088e413bb 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -139,6 +139,9 @@ class TheoryEngine {
    * the cost of walking the DAG on registration, etc.
    */
   const LogicInfo& d_logicInfo;
+  /** The separation logic location and data types */
+  TypeNode d_sepLocType;
+  TypeNode d_sepDataType;
 
   /** Reference to the output manager of the smt engine */
   OutputManager& d_outMgr;
@@ -637,6 +640,16 @@ class TheoryEngine {
   }
   /** get the logic info used by this theory engine */
   const LogicInfo& getLogicInfo() const;
+  /** get the separation logic heap types */
+  bool getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const;
+
+  /**
+   * Declare heap. This is used for separation logics to set the location
+   * and data types. It should be called only once, and before any separation
+   * logic constraints are asserted to this theory engine.
+   */
+  void declareSepHeap(TypeNode locT, TypeNode dataT);
+
   /**
    * Returns the equality status of the two terms, from the theory
    * that owns the domain type.  The types of a and b must be the same.