From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 14 Oct 2020 00:50:19 +0000 (-0500)
Subject: (proof-new) Simplifications for proof rule checker interface (#5244)
X-Git-Tag: cvc5-1.0.0~2717
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53b3cf646549200e4986a47872abf6121fcbfe5b;p=cvc5.git

(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.
---

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 */
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 1a30f4449..8824859d4 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -201,6 +201,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
                                             const std::vector<Node>& children,
                                             const std::vector<Node>& args)
 {
+  NodeManager * nm = NodeManager::currentNM();
   // compute what was proven
   if (id == PfRule::ASSUME)
   {
@@ -217,7 +218,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
       // no antecedant
       return children[0];
     }
-    Node ant = mkAnd(args);
+    Node ant = nm->mkAnd(args);
     // if the conclusion is false, its the negated antencedant only
     if (children[0].isConst() && !children[0].getConst<bool>())
     {
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index ce2eb89ab..0b6cf6652 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -53,7 +53,7 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::STRING_CODE_INJ, this);
   pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
   // trusted rules
-  pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 1);
+  pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2);
 }
 
 Node StringProofRuleChecker::checkInternal(PfRule id,
@@ -318,7 +318,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       std::vector<Node> conj;
       ret = StringsPreprocess::reduce(t, conj, &skc);
       conj.push_back(t.eqNode(ret));
-      ret = mkAnd(conj);
+      ret = nm->mkAnd(conj);
     }
     else if (id == PfRule::STRING_EAGER_REDUCTION)
     {