From 59d8647b04f86421949390a3e958ffdf0df07665 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Nov 2020 20:27:38 -0600
Subject: Fix preregistration in TheorySep before declare-heap (#5411)

Followup to fix for #5343. This catches cases where separation logic constraints are preregistered to TheorySep before the heap has been declared, which should also result in an error.
---
 src/theory/sep/theory_sep.cpp | 38 +++++++++++++++++++++++++++++++-------
 src/theory/sep/theory_sep.h   |  7 +++++++
 2 files changed, 38 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 1b25bb0f4..4a7f4367e 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -102,6 +102,15 @@ void TheorySep::finishInit()
   // we could but don't do congruence on SEP_STAR here.
 }
 
+void TheorySep::preRegisterTerm(TNode n)
+{
+  Kind k = n.getKind();
+  if (k == SEP_PTO || k == SEP_EMP || k == SEP_STAR || k == SEP_WAND)
+  {
+    registerRefDataTypesAtom(n);
+  }
+}
+
 Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
   if( assumptions.empty() ){
     return d_true;
@@ -1009,9 +1018,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
   if( it==visited[index].end() ){
     Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl;
     if( n.getKind()==kind::SEP_EMP ){
-      TypeNode tn = n[0].getType();
-      TypeNode tnd = n[1].getType();
-      registerRefDataTypes( tn, tnd, n );
+      registerRefDataTypesAtom(n);
       if( hasPol && pol ){
         references[index][n].clear();
         references_strict[index][n] = true; 
@@ -1019,10 +1026,9 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
         card = 1;
       }
     }else if( n.getKind()==kind::SEP_PTO ){
-      TypeNode tn1 = n[0].getType();
-      TypeNode tn2 = n[1].getType();
-      registerRefDataTypes( tn1, tn2, n );
+      registerRefDataTypesAtom(n);
       if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){
+        TypeNode tn1 = n[0].getType();
         if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){
           if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){
             // still valid : bound on heap models will include Herbrand universe of n[0].getType()
@@ -1133,7 +1139,25 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
   return card;
 }
 
-void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
+void TheorySep::registerRefDataTypesAtom(Node atom)
+{
+  TypeNode tn1;
+  TypeNode tn2;
+  Kind k = atom.getKind();
+  if (k == SEP_PTO || k == SEP_EMP)
+  {
+    tn1 = atom[0].getType();
+    tn2 = atom[1].getType();
+  }
+  else
+  {
+    Assert(k == SEP_STAR || k == SEP_WAND);
+  }
+  registerRefDataTypes(tn1, tn2, atom);
+}
+
+void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom)
+{
   if (!d_type_ref.isNull())
   {
     Assert(!atom.isNull());
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 2cd7aba91..9e96dccc3 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -100,6 +100,8 @@ class TheorySep : public Theory {
   /** finish initialization */
   void finishInit() override;
   //--------------------------------- end initialization
+  /** preregister term */
+  void preRegisterTerm(TNode n) override;
 
   std::string identify() const override { return std::string("TheorySep"); }
 
@@ -283,6 +285,11 @@ class TheorySep : public Theory {
   //get global reference/data type
   TypeNode getReferenceType( Node n );
   TypeNode getDataType( Node n );
+  /**
+   * Register reference data types for atom. Calls the method below for
+   * the appropriate types.
+   */
+  void registerRefDataTypesAtom(Node atom);
   /**
    * This is called either when:
    * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
-- 
cgit v1.2.3