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.

20 files changed, 302 insertions, 55 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c0e6bad5f..566bcc3c7 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -5194,6 +5194,17 @@ Term Solver::getQuantifierEliminationDisjunct(api::Term q) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+void Solver::declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(
+      d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
+      << "Cannot obtain separation logic expressions if not using the "
+         "separation logic theory.";
+  d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode());
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::getSeparationHeap() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 13d4f6e23..db57af121 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3158,6 +3158,15 @@ class CVC4_PUBLIC Solver
   Term getQuantifierEliminationDisjunct(api::Term q) const;
 
   /**
+   * When using separation logic, this sets the location sort and the
+   * datatype sort to the given ones. This method should be invoked exactly
+   * once, before any separation logic constraints are provided.
+   * @param locSort The location sort of the heap
+   * @param dataSort The data sort of the heap
+   */
+  void declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const;
+
+  /**
    * When using separation logic, obtain the term for the heap.
    * @return The term for the heap
    */
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 13f4606da..29f997394 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -235,6 +235,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         vector[Term] getUnsatCore() except +
         Term getValue(Term term) except +
         vector[Term] getValue(const vector[Term]& terms) except +
+        void declareSeparationHeap(Sort locSort, Sort dataSort) except +
         Term getSeparationHeap() except +
         Term getSeparationNilTerm() except +
         void pop(uint32_t nscopes) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 16f454311..f945228dd 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1122,6 +1122,9 @@ cdef class Solver:
         term.cterm = self.csolver.getSeparationHeap()
         return term
 
+    def declareSeparationHeap(self, Sort locType, Sort dataType):
+        self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
+
     def getSeparationNilTerm(self):
         cdef Term term = Term(self)
         term.cterm = self.csolver.getSeparationNilTerm()
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index fe051f036..40c66eaa5 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -895,7 +895,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::vector<api::DatatypeDecl> dts;
   CVC4::api::Term e, e2;
-  CVC4::api::Sort t;
+  CVC4::api::Sort t, s;
   std::string name;
   std::vector<std::string> names;
   std::vector<CVC4::api::Term> terms;
@@ -1073,9 +1073,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
-    sortSymbol[t, CHECK_DECLARED]
-    // We currently do nothing with the type information declared for the heap.
-    { cmd->reset(new EmptyCommand()); }
+    sortSymbol[s, CHECK_DECLARED]
+    { cmd->reset(new DeclareHeapCommand(t, s)); }
     RPAREN_TOK
   | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd->reset(new BlockModelCommand()); }
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 195247df7..21eb88c8c 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -415,6 +415,13 @@ void Printer::toStreamCmdComment(std::ostream& out,
   printUnknownCommand(out, "comment");
 }
 
+void Printer::toStreamCmdDeclareHeap(std::ostream& out,
+                                     TypeNode locType,
+                                     TypeNode dataType) const
+{
+  printUnknownCommand(out, "declare-heap");
+}
+
 void Printer::toStreamCmdCommandSequence(
     std::ostream& out, const std::vector<Command*>& sequence) const
 {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 84262d992..ffacaa5d8 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -256,6 +256,10 @@ class Printer
   /** Print comment command */
   virtual void toStreamCmdComment(std::ostream& out,
                                   const std::string& comment) const;
+  /** Declare heap command */
+  virtual void toStreamCmdDeclareHeap(std::ostream& out,
+                                      TypeNode locType,
+                                      TypeNode dataType) const;
 
   /** Print command sequence command */
   virtual void toStreamCmdCommandSequence(
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bc6902305..032d26511 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1938,6 +1938,13 @@ void Smt2Printer::toStreamCmdComment(std::ostream& out,
   out << "(set-info :notes \"" << s << "\")" << std::endl;
 }
 
+void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out,
+                                         TypeNode locType,
+                                         TypeNode dataType) const
+{
+  out << "(declare-heap (" << locType << " " << dataType << "))" << std::endl;
+}
+
 void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
                                    const std::string& name) const
 {
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index f4783c955..3fc144d46 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -217,6 +217,11 @@ class Smt2Printer : public CVC4::Printer
   void toStreamCmdComment(std::ostream& out,
                           const std::string& comment) const override;
 
+  /** Print declare-heap command */
+  void toStreamCmdDeclareHeap(std::ostream& out,
+                              TypeNode locType,
+                              TypeNode dataType) const override;
+
   /** Print command sequence command */
   void toStreamCmdCommandSequence(
       std::ostream& out, const std::vector<Command*>& sequence) const override;
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 58ac57cc9..b33fe5ad9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1425,9 +1425,43 @@ void DefineFunctionRecCommand::toStream(std::ostream& out,
       formals,
       api::termVectorToNodes(d_formulas));
 }
+/* -------------------------------------------------------------------------- */
+/* class DeclareHeapCommand                                                   */
+/* -------------------------------------------------------------------------- */
+DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort)
+    : d_locSort(locSort), d_dataSort(dataSort)
+{
+}
+
+api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
+api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
+
+void DeclareHeapCommand::invoke(api::Solver* solver)
+{
+  solver->declareSeparationHeap(d_locSort, d_dataSort);
+}
+
+Command* DeclareHeapCommand::clone() const
+{
+  return new DeclareHeapCommand(d_locSort, d_dataSort);
+}
+
+std::string DeclareHeapCommand::getCommandName() const
+{
+  return "declare-heap";
+}
+
+void DeclareHeapCommand::toStream(std::ostream& out,
+                                  int toDepth,
+                                  size_t dag,
+                                  OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclareHeap(
+      out, d_locSort.getTypeNode(), d_dataSort.getTypeNode());
+}
 
 /* -------------------------------------------------------------------------- */
-/* class SetUserAttribute                                                     */
+/* class SetUserAttributeCommand                                              */
 /* -------------------------------------------------------------------------- */
 
 SetUserAttributeCommand::SetUserAttributeCommand(
diff --git a/src/smt/command.h b/src/smt/command.h
index d2ce99f2f..438f9febb 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -511,7 +511,6 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DefineNamedFunctionCommand */
@@ -562,6 +561,34 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command
 }; /* class DefineFunctionRecCommand */
 
 /**
+ * In separation logic inputs, which is an extension of smt2 inputs, this
+ * corresponds to the command:
+ *   (declare-heap (T U))
+ * where T is the location sort and U is the data sort.
+ */
+class CVC4_PUBLIC DeclareHeapCommand : public Command
+{
+ public:
+  DeclareHeapCommand(api::Sort locSort, api::Sort dataSort);
+  api::Sort getLocationSort() const;
+  api::Sort getDataSort() const;
+  void invoke(api::Solver* solver) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+
+ protected:
+  /** The location sort */
+  api::Sort d_locSort;
+  /** The data sort */
+  api::Sort d_dataSort;
+};
+
+/**
  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
  *  via the syntax (! expr :attr)
  */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dc5338199..a5861c6b0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -65,6 +65,7 @@
 #include "theory/logic_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
 #include "util/hash.h"
 #include "util/random.h"
@@ -1448,6 +1449,28 @@ std::vector<Node> SmtEngine::getExpandedAssertions()
   return eassertsProc;
 }
 
+void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+  if (!d_logic.isTheoryEnabled(THEORY_SEP))
+  {
+    const char* msg =
+        "Cannot declare heap if not using the separation logic theory.";
+    throw RecoverableModalException(msg);
+  }
+  SmtScope smts(this);
+  finishInit();
+  TheoryEngine* te = getTheoryEngine();
+  te->declareSepHeap(locT, dataT);
+}
+
+bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
+{
+  SmtScope smts(this);
+  finishInit();
+  TheoryEngine* te = getTheoryEngine();
+  return te->getSepHeapTypes(locT, dataT);
+}
+
 Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
 Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
@@ -1483,21 +1506,28 @@ void SmtEngine::checkUnsatCore() {
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
   UnsatCore core = getUnsatCore();
 
-  SmtEngine coreChecker(d_exprManager, &d_options);
-  coreChecker.setIsInternalSubsolver();
-  coreChecker.setLogic(getLogicInfo());
-  coreChecker.getOptions().set(options::checkUnsatCores, false);
+  // initialize the core checker
+  std::unique_ptr<SmtEngine> coreChecker;
+  initializeSubsolver(coreChecker);
+  coreChecker->getOptions().set(options::checkUnsatCores, false);
+
+  // set up separation logic heap if necessary
+  TypeNode sepLocType, sepDataType;
+  if (getSepHeapTypes(sepLocType, sepDataType))
+  {
+    coreChecker->declareSepHeap(sepLocType, sepDataType);
+  }
 
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     Node assertionAfterExpansion = expandDefinitions(*i);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
              << ", expanded to " << assertionAfterExpansion << "\n";
-    coreChecker.assertFormula(assertionAfterExpansion);
+    coreChecker->assertFormula(assertionAfterExpansion);
   }
   Result r;
   try {
-    r = coreChecker.checkSat();
+    r = coreChecker->checkSat();
   } catch(...) {
     throw;
   }
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();
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 013c61e52..1b25bb0f4 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -69,6 +69,22 @@ TheorySep::~TheorySep() {
   }
 }
 
+void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+  if (!d_type_ref.isNull())
+  {
+    TypeNode te1 = d_loc_to_data_type.begin()->first;
+    std::stringstream ss;
+    ss << "ERROR: cannot declare heap types for separation logic more than "
+          "once.  We are declaring heap of type ";
+    ss << locT << " -> " << dataT << ", but we already have ";
+    ss << d_type_ref << " -> " << d_type_data;
+    throw LogicException(ss.str());
+  }
+  Node nullAtom;
+  registerRefDataTypes(locT, dataT, nullAtom);
+}
+
 TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
 
 bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
@@ -239,7 +255,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){
 
 void TheorySep::presolve() {
   Trace("sep-pp") << "Presolving" << std::endl;
-  //TODO: cleanup if incremental?
 }
 
 
@@ -1119,48 +1134,43 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
 }
 
 void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
-  //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input
-  if( options::incrementalSolving() ){
-    std::stringstream ss;
-    ss << "ERROR: cannot use separation logic in incremental mode." << std::endl;
-    throw LogicException(ss.str());
-  }
-  std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 );
-  if( itt==d_loc_to_data_type.end() ){
-    if( !d_loc_to_data_type.empty() ){
-      TypeNode te1 = d_loc_to_data_type.begin()->first;
+  if (!d_type_ref.isNull())
+  {
+    Assert(!atom.isNull());
+    // already declared, ensure compatible
+    if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
+        || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+    {
       std::stringstream ss;
-      ss << "ERROR: specifying heap constraints for two different types : " << tn1 << " -> " << tn2 << " and " << te1 << " -> " << d_loc_to_data_type[te1] << std::endl;
-      throw LogicException(ss.str());
-      Assert(false);
-    }
-    if( tn2.isNull() ){
-      Trace("sep-type") << "Sep: assume location type " << tn1 << " (from " << atom << ")" << std::endl;
-    }else{
-      Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
-    }
-    d_loc_to_data_type[tn1] = tn2;
-    //for now, we only allow heap constraints of one type
-    d_type_ref = tn1;
-    d_type_data = tn2;
-    d_bound_kind[tn1] = bound_default;
-  }else{
-    if( !tn2.isNull() ){
-      if( itt->second!=tn2 ){
-        if( itt->second.isNull() ){
-          Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
-          //now we know data type
-          d_loc_to_data_type[tn1] = tn2;
-          d_type_data = tn2;
-        }else{
-          std::stringstream ss;
-          ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
-          throw LogicException(ss.str());
-          Assert(false);
-        }
-      }
+      ss << "ERROR: the separation logic heap type has already been set to "
+         << d_type_ref << " -> " << d_type_data
+         << " but we have a constraint that uses different heap types, "
+            "offending atom is "
+         << atom << " with associated heap type " << tn1 << " -> " << tn2
+         << std::endl;
     }
+    return;
+  }
+  // if not declared yet, and we have a separation logic constraint, throw
+  // an error.
+  if (!atom.isNull())
+  {
+    std::stringstream ss;
+    // error, heap not declared
+    ss << "ERROR: the type of the separation logic heap has not been declared "
+          "(e.g. via a declare-heap command), and we have a separation logic "
+          "constraint "
+       << atom << std::endl;
+    throw LogicException(ss.str());
   }
+  // otherwise set it
+  Trace("sep-type") << "Sep: assume location type " << tn1
+                    << " is associated with data type " << tn2 << std::endl;
+  d_loc_to_data_type[tn1] = tn2;
+  // for now, we only allow heap constraints of one type
+  d_type_ref = tn1;
+  d_type_data = tn2;
+  d_bound_kind[tn1] = bound_default;
 }
 
 void TheorySep::initializeBounds() {
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index ac87ebe67..2cd7aba91 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -79,6 +79,15 @@ class TheorySep : public Theory {
             ProofNodeManager* pnm = nullptr);
   ~TheorySep();
 
+  /**
+   * 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 can be
+   * executed once only, and must be invoked before solving separation logic
+   * inputs.
+   */
+  void declareSepHeap(TypeNode locT, TypeNode dataT) override;
+
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
@@ -274,7 +283,14 @@ class TheorySep : public Theory {
   //get global reference/data type
   TypeNode getReferenceType( Node n );
   TypeNode getDataType( Node n );
-  void registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom );
+  /**
+   * This is called either when:
+   * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
+   * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.
+   * We set the heap type if we are are case (A), and check whether the
+   * heap type is consistent in the case of (B).
+   */
+  void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom);
   //get location/data type
   //get the base label for the spatial assertion
   Node getBaseLabel( TypeNode tn );
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index cedb838af..ed10e85ae 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -51,11 +51,11 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
   smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions()));
   smte->setIsInternalSubsolver();
   smte->setLogic(smtCurr->getLogicInfo());
+  // set the options
   if (needsTimeout)
   {
     smte->setTimeLimit(timeout);
   }
-  smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
 }
 
 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index d34729dec..f68900ccc 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -31,7 +31,16 @@ namespace theory {
 
 /**
  * This function initializes the smt engine smte to check the satisfiability
- * of the argument "query".
+ * of the argument "query". It takes the logic and options of the current
+ * SMT engine in scope.
+ *
+ * Notice this method intentionally does not fully initialize smte. This means
+ * that the options of smte can still be modified after it is returned by
+ * this method.
+ *
+ * Notice that some aspects of subsolvers are not incoporated by this call.
+ * For example, the type of separation logic heaps is not set on smte, even
+ * if the current SMT engine has declared a separation logic heap.
  *
  * @param smte The smt engine pointer to initialize
  * @param needsTimeout Whether we would like to set a timeout
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;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 706149d86..3a155b9ad 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1116,6 +1116,42 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
 const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
 
+bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
+{
+  if (d_sepLocType.isNull())
+  {
+    return false;
+  }
+  locType = d_sepLocType;
+  dataType = d_sepDataType;
+  return true;
+}
+
+void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+  Theory* tsep = theoryOf(THEORY_SEP);
+  if (tsep == nullptr)
+  {
+    Assert(false) << "TheoryEngine::declareSepHeap called without the "
+                     "separation logic theory enabled";
+    return;
+  }
+
+  // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+  theoryOf(THEORY)->declareSepHeap(locT, dataT);
+
+  // notify each theory using the statement above
+  CVC4_FOR_EACH_THEORY;
+
+  // remember the types we have set
+  d_sepLocType = locT;
+  d_sepDataType = dataT;
+}
+
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType().isComparableTo(b.getType()));
   return d_sharedSolver->getEqualityStatus(a, b);
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.