Minor cleanup of proof messages (#7494)

Also deletes unused code encountered in TheoryArrays while investigating cyclic proofs.

diff --git a/src/proof/proof_ensure_closed.h b/src/proof/proof_ensure_closed.h
index cacfeeeedea9466b9ac0b9e1caaf73e295e2376f..14850de9b920ded26b6db335d79f3717bb545320 100644 (file)
--- 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 ce8ca55c3669e5e6bf4ab6035c0b220e1bf0f088..069bd1ba2a9222179e188c38f71aa4c08734c35f 100644 (file)
--- 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 67a43fedc7017f72dc816665cca2b0cabec194f4..e8871af340b5d9fb8635da32511ff2a48d6c34b8 100644 (file)
--- 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 561d4a761969584497be7f356bfeded14fffcf84..47f30f9bb6f8880f8aefc79b064e5e1e6b1bdf97 100644 (file)
--- 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 97cbec1d5baee0647a931d793ae0d06645f09459..7362e1fbab28abfdc77779a8732ecdfb011b382f 100644 (file)
--- 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 c8cff93f88f5a1856e8d2440b444b28ee78c9c38..2ce2344b93315f1f562d9601c1b4d87137e66fde 100644 (file)
--- 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;