From fb5e3113312322c21a00062b22c358c30fa27101 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 17 Feb 2021 15:39:42 +0100
Subject: Add InferenceIds for theory of arrays (#5910)

This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
---
 src/theory/arrays/inference_manager.cpp | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'src/theory/arrays/inference_manager.cpp')

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index be2972444..afcc9a719 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -37,8 +37,9 @@ InferenceManager::InferenceManager(Theory& t,
 
 bool InferenceManager::assertInference(TNode atom,
                                        bool polarity,
+                                       InferenceId id,
                                        TNode reason,
-                                       PfRule id)
+                                       PfRule pfr)
 {
   Trace("arrays-infer") << "TheoryArrays::assertInference: "
                         << (polarity ? Node(atom) : atom.notNode()) << " by "
@@ -52,14 +53,14 @@ bool InferenceManager::assertInference(TNode atom,
     std::vector<Node> children;
     std::vector<Node> args;
     // convert to proof rule application
-    convert(id, fact, reason, children, args);
-    return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args);
+    convert(pfr, fact, reason, children, args);
+    return assertInternalFact(atom, polarity, id, pfr, children, args);
   }
-  return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason);
+  return assertInternalFact(atom, polarity, id, reason);
 }
 
 bool InferenceManager::arrayLemma(
-    Node conc, Node exp, PfRule id, LemmaProperty p, bool doCache)
+    Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p, bool doCache)
 {
   Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp
                         << "; " << id << std::endl;
@@ -69,14 +70,14 @@ bool InferenceManager::arrayLemma(
     std::vector<Node> children;
     std::vector<Node> args;
     // convert to proof rule application
-    convert(id, conc, exp, children, args);
+    convert(pfr, conc, exp, children, args);
     // make the trusted lemma based on the eager proof generator and send
-    TrustNode tlem = d_lemmaPg->mkTrustNode(conc, id, children, args);
-    return trustedLemma(tlem, InferenceId::UNKNOWN, p, doCache);
+    TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args);
+    return trustedLemma(tlem, id, p, doCache);
   }
   // send lemma without proofs
   Node lem = nm->mkNode(IMPLIES, exp, conc);
-  return lemma(lem, InferenceId::UNKNOWN, p, doCache);
+  return lemma(lem, id, p, doCache);
 }
 
 void InferenceManager::convert(PfRule& id,
-- 
cgit v1.2.3