(proof-new) Simplifications for proof rule checker interface (#5244)

Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.

This also updates STRING_TRUST to have pedantic level 2.

2 files changed, 14 insertions, 54 deletions

diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index 7accd08dc..e839c0830 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -30,39 +30,6 @@ Node ProofRuleChecker::check(PfRule id,
   return checkInternal(id, children, args);
 }
 
-Node ProofRuleChecker::checkChildrenArg(PfRule id,
-                                        const std::vector<Node>& children,
-                                        Node arg)
-{
-  return check(id, children, {arg});
-}
-Node ProofRuleChecker::checkChildren(PfRule id,
-                                     const std::vector<Node>& children)
-{
-  return check(id, children, {});
-}
-Node ProofRuleChecker::checkChild(PfRule id, Node child)
-{
-  return check(id, {child}, {});
-}
-Node ProofRuleChecker::checkArg(PfRule id, Node arg)
-{
-  return check(id, {}, {arg});
-}
-
-Node ProofRuleChecker::mkAnd(const std::vector<Node>& a)
-{
-  if (a.empty())
-  {
-    return NodeManager::currentNM()->mkConst(true);
-  }
-  else if (a.size() == 1)
-  {
-    return a[0];
-  }
-  return NodeManager::currentNM()->mkNode(AND, a);
-}
-
 bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
 {
   // must be a non-negative integer constant that fits an unsigned int
@@ -194,17 +161,20 @@ Node ProofChecker::checkDebug(PfRule id,
   // since we are debugging, we want to treat trusted (null) checkers as
   // a failure.
   Node res = checkInternal(id, cchildren, args, expected, out, false);
-  Trace(traceTag) << "ProofChecker::checkDebug: " << id;
-  if (res.isNull())
-  {
-    Trace(traceTag) << " failed, " << out.str() << std::endl;
-  }
-  else
+  if (Trace.isOn(traceTag))
   {
-    Trace(traceTag) << " success" << std::endl;
+    Trace(traceTag) << "ProofChecker::checkDebug: " << id;
+    if (res.isNull())
+    {
+      Trace(traceTag) << " failed, " << out.str() << std::endl;
+    }
+    else
+    {
+      Trace(traceTag) << " success" << std::endl;
+    }
+    Trace(traceTag) << "cchildren: " << cchildren << std::endl;
+    Trace(traceTag) << "     args: " << args << std::endl;
   }
-  Trace(traceTag) << "cchildren: " << cchildren << std::endl;
-  Trace(traceTag) << "     args: " << args << std::endl;
   return res;
 }
 
@@ -335,7 +305,7 @@ bool ProofChecker::isPedanticFailure(PfRule id, std::ostream& out) const
     if (itp->second <= d_pclevel)
     {
       out << "pedantic level for " << id << " not met (rule level is "
-          << itp->second << " which is strictly below the required level "
+          << itp->second << " which is at or below the pedantic level "
           << d_pclevel << ")";
       return true;
     }
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index b12b10ad8..93e16e63c 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -54,17 +54,7 @@ class ProofRuleChecker
   Node check(PfRule id,
              const std::vector<Node>& children,
              const std::vector<Node>& args);
-  /** Single arg version */
-  Node checkChildrenArg(PfRule id, const std::vector<Node>& children, Node arg);
-  /** No arg version */
-  Node checkChildren(PfRule id, const std::vector<Node>& children);
-  /** Single child only version */
-  Node checkChild(PfRule id, Node child);
-  /** Single argument only version */
-  Node checkArg(PfRule id, Node arg);
-
-  /** Make AND-kinded node with children a */
-  static Node mkAnd(const std::vector<Node>& a);
+
   /** get an index from a node, return false if we fail */
   static bool getUInt32(TNode n, uint32_t& i);
   /** get a Boolean from a node, return false if we fail */