From 1ef32585ddcf873805a7163bc266abaf10c7acd8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 29 Oct 2021 13:33:30 -0500
Subject: [PATCH] Minor cleanup of proof messages (#7494)

Also deletes unused code encountered in TheoryArrays while investigating cyclic proofs.
---
 src/proof/proof_ensure_closed.h     |  2 +-
 src/proof/proof_node_algorithm.cpp  |  2 +-
 src/proof/proof_node_to_sexpr.cpp   |  2 +-
 src/proof/proof_node_updater.cpp    |  2 +-
 src/theory/arrays/theory_arrays.cpp | 21 ---------------------
 src/theory/arrays/theory_arrays.h   |  3 ---
 6 files changed, 4 insertions(+), 28 deletions(-)

diff --git a/src/proof/proof_ensure_closed.h b/src/proof/proof_ensure_closed.h
index cacfeeeed..14850de9b 100644
--- a/src/proof/proof_ensure_closed.h
+++ b/src/proof/proof_ensure_closed.h
@@ -28,7 +28,7 @@ class ProofNode;
 /**
  * Debug check closed on Trace c. Context ctx is string for debugging.
  * This method throws an assertion failure if pg cannot provide a closed
- * proof for fact proven. This is checked only if --proof-eager-checking
+ * proof for fact proven. This is checked only if --proof-check=eager
  * is enabled or the Trace c is enabled.
  *
  * @param reqGen Whether we consider a null generator to be a failure.
diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp
index ce8ca55c3..069bd1ba2 100644
--- a/src/proof/proof_node_algorithm.cpp
+++ b/src/proof/proof_node_algorithm.cpp
@@ -106,7 +106,7 @@ void getFreeAssumptionsMap(
               != traversing.end())
           {
             Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
-                           "--proof-eager-checking)"
+                           "--proof-check=eager)"
                         << std::endl;
           }
           visit.push_back(cp);
diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp
index 67a43fedc..e8871af34 100644
--- a/src/proof/proof_node_to_sexpr.cpp
+++ b/src/proof/proof_node_to_sexpr.cpp
@@ -60,7 +60,7 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
             != traversing.end())
         {
           Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
-                         "--proof-eager-checking)"
+                         "--proof-check=eager)"
                       << std::endl;
           return Node::null();
         }
diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp
index 561d4a761..47f30f9bb 100644
--- a/src/proof/proof_node_updater.cpp
+++ b/src/proof/proof_node_updater.cpp
@@ -154,7 +154,7 @@ void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
         {
           Unhandled()
               << "ProofNodeUpdater::processInternal: cyclic proof! (use "
-                 "--proof-eager-checking)"
+                 "--proof-check=eager)"
               << std::endl;
         }
         visit.push_back(cp);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 97cbec1d5..7362e1fba 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -825,27 +825,6 @@ void TheoryArrays::preRegisterTerm(TNode node)
   }
 }
 
-void TheoryArrays::explain(TNode literal, Node& explanation)
-{
-  ++d_numExplain;
-  Debug("arrays") << spaces(context()->getLevel()) << "TheoryArrays::explain("
-                  << literal << ")" << std::endl;
-  std::vector<TNode> assumptions;
-  // Do the work
-  bool polarity = literal.getKind() != kind::NOT;
-  TNode atom = polarity ? literal : literal[0];
-  if (atom.getKind() == kind::EQUAL)
-  {
-    d_equalityEngine->explainEquality(
-        atom[0], atom[1], polarity, assumptions, nullptr);
-  }
-  else
-  {
-    d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
-  }
-  explanation = mkAnd(assumptions);
-}
-
 TrustNode TheoryArrays::explain(TNode literal)
 {
   return d_im.explainLit(literal);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index c8cff93f8..2ce2344b9 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -208,9 +208,6 @@ class TheoryArrays : public Theory {
   /** Should be called to propagate the literal.  */
   bool propagateLit(TNode literal);
 
-  /** Explain why this literal is true by building an explanation */
-  void explain(TNode literal, Node& exp);
-
   /** For debugging only- checks invariants about when things are preregistered*/
   context::CDHashSet<Node> d_isPreRegistered;
 
-- 
2.30.2