From bdc1b222fbc674ab1f8a48fad9f78759c3baea23 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 17 Feb 2021 16:50:15 +0100
Subject: [PATCH] Use InferenceId in sep theory. (#5912)

This PR uses the new InferenceIds in the separation logic theory.
---
 src/theory/inference_id.cpp   |  3 +++
 src/theory/inference_id.h     |  5 +++++
 src/theory/sep/theory_sep.cpp | 18 +++++++++---------
 src/theory/sep/theory_sep.h   |  2 +-
 4 files changed, 18 insertions(+), 10 deletions(-)

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 81c34cf3f..b80503fe9 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -75,6 +75,9 @@ const char* toString(InferenceId i)
     case InferenceId::DATATYPES_BISIMILAR: return "BISIMILAR";
     case InferenceId::DATATYPES_CYCLE: return "CYCLE";
 
+    case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
+    case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
+
     case InferenceId::STRINGS_I_NORM_S: return "I_NORM_S";
     case InferenceId::STRINGS_I_CONST_MERGE: return "I_CONST_MERGE";
     case InferenceId::STRINGS_I_CONST_CONFLICT: return "I_CONST_CONFLICT";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index a48a8c366..bb69f5d7f 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -135,6 +135,11 @@ enum class InferenceId
   // cycle conflict for datatypes
   DATATYPES_CYCLE,
 
+  // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
+  SEP_PTO_NEG_PROP,
+  // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w
+  SEP_PTO_PROP,
+
   //-------------------------------------- base solver
   // initial normalize singular
   //   x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 8782bfe34..db7fa2c6c 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1745,7 +1745,7 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity )
       Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) );
       Trace("sep-pto")  << "Conclusion is " << n_conc << std::endl;
       // propagation for (pto x y) ^ ~(pto z w) ^ x = z => y != w
-      sendLemma( exp, n_conc, "PTO_NEG_PROP" );
+      sendLemma( exp, n_conc, InferenceId::SEP_PTO_NEG_PROP);
     }
   }else{
     if( polarity ){
@@ -1770,30 +1770,30 @@ void TheorySep::mergePto( Node p1, Node p2 ) {
     exp.push_back( p1 );
     exp.push_back( p2 );
     //enforces injectiveness of pto : (pto x y) ^ (pto y w) ^ x = y => y = w
-    sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" );
+    sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), InferenceId::SEP_PTO_PROP);
   }
 }
 
-void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer ) {
+void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer ) {
   Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl;
   conc = Rewriter::rewrite( conc );
   Trace("sep-lemma-debug") << "Got : " << conc << std::endl;
   if( conc!=d_true ){
     if( infer && conc!=d_false ){
       Node ant_n = NodeManager::currentNM()->mkAnd(ant);
-      Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl;
-      d_im.addPendingFact(conc, InferenceId::UNKNOWN, ant_n);
+      Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << id << std::endl;
+      d_im.addPendingFact(conc, id, ant_n);
     }else{
       if( conc==d_false ){
-        Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << c
+        Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << id
                            << std::endl;
-        d_im.conflictExp(InferenceId::UNKNOWN, ant, nullptr);
+        d_im.conflictExp(id, ant, nullptr);
       }else{
         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant
-                           << " by " << c << std::endl;
+                           << " by " << id << std::endl;
         TrustNode trn = d_im.mkLemmaExp(conc, ant, {});
         d_im.addPendingLemma(
-            trn.getNode(), InferenceId::UNKNOWN, LemmaProperty::NONE, trn.getGenerator());
+            trn.getNode(), id, LemmaProperty::NONE, trn.getGenerator());
       }
     }
   }
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 9396200c9..b2cd6bf45 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -339,7 +339,7 @@ class TheorySep : public Theory {
   bool areDisequal( Node a, Node b );
   void eqNotifyMerge(TNode t1, TNode t2);
 
-  void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
+  void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false );
   void doPending();
 
  public:
-- 
2.30.2