From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Nov 2020 02:27:38 +0000 (-0600)
Subject: Fix preregistration in TheorySep before declare-heap (#5411)
X-Git-Tag: cvc5-1.0.0~2617
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59d8647b04f86421949390a3e958ffdf0df07665;p=cvc5.git

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.
---

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
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9a0565d8e..ac62452e5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -869,6 +869,7 @@ set(regress_0_tests
   regress0/sep/dispose-1.smt2
   regress0/sep/dup-nemp.smt2
   regress0/sep/issue3720-check-model.smt2
+  regress0/sep/issue5343-err.smt2
   regress0/sep/nemp.smt2
   regress0/sep/nil-no-elim.smt2
   regress0/sep/nspatial-simp.smt2
diff --git a/test/regress/regress0/sep/issue5343-err.smt2 b/test/regress/regress0/sep/issue5343-err.smt2
new file mode 100644
index 000000000..ea37815fa
--- /dev/null
+++ b/test/regress/regress0/sep/issue5343-err.smt2
@@ -0,0 +1,8 @@
+; REQUIRES: no-competition
+; COMMAND-LINE:
+; EXPECT: (error "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 (wand true true)
+; EXPECT: ")
+; EXIT: 1
+(set-logic QF_ALL_SUPPORTED)
+(assert (wand true true))
+(check-sat)