Revert

ajreynol · Oct 21, 2024 · e346730 · e346730
1 parent 89024b9
commit e346730
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 53 deletions.
diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
@@ -48,10 +48,7 @@ ProofFinalCallback::ProofFinalCallback(Env& env)
           "finalProof::trustCount")),
       d_trustTheoryIdCount(
           statisticsRegistry().registerHistogram<theory::TheoryId>(
-              "finalProof::trustTheoryRewriteCount")),
-      d_trustTheoryLemmaCount(
-          statisticsRegistry().registerHistogram<theory::TheoryId>(
-              "finalProof::trustTheoryLemmaCount")),
+              "finalProof::trustTheoryIdCount")),
       d_totalRuleCount(
           statisticsRegistry().registerInt("finalProof::totalRuleCount")),
       d_minPedanticLevel(
@@ -140,16 +137,6 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
     {
       d_trustIds << id;
       Trace("final-pf-hole") << " " << id;
-      if (id == TrustId::THEORY_LEMMA)
-      {
-        const std::vector<Node>& args = pn->getArguments();
-        TheoryId tid = THEORY_BUILTIN;
-        if (args.size() >= 3)
-        {
-          builtin::BuiltinProofRuleChecker::getTheoryId(args[2], tid);
-        }
-        d_trustTheoryLemmaCount << tid;
-      }
     }
     Trace("final-pf-hole") << ": " << pn->getResult() << std::endl;
   }
@@ -191,44 +178,11 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
         premises.push_back(pncc->getResult());
       }
       NodeManager* nm = nodeManager();
-      Node query = conc;
-      if (!premises.empty())
-      {
-        query = nm->mkNode(Kind::IMPLIES, nm->mkAnd(premises), query);
-      }
-      // print the trusted step information
+      Node query = nm->mkNode(Kind::IMPLIES, nm->mkAnd(premises), conc);
       if (isOutputOn(OutputTag::TRUSTED_PROOF_STEPS))
       {
         output(OutputTag::TRUSTED_PROOF_STEPS)
-            << "(trusted-proof-step " << query;
-        output(OutputTag::TRUSTED_PROOF_STEPS) << " :rule " << r;
-        TheoryId tid = THEORY_LAST;
-        if (r == ProofRule::TRUST)
-        {
-          TrustId id;
-          if (getTrustId(pn->getArguments()[0], id))
-          {
-            output(OutputTag::TRUSTED_PROOF_STEPS) << " :trust-id " << id;
-            if (id == TrustId::THEORY_LEMMA)
-            {
-              const std::vector<Node>& args = pn->getArguments();
-              if (args.size() >= 3)
-              {
-                builtin::BuiltinProofRuleChecker::getTheoryId(args[2], tid);
-              }
-            }
-          }
-        }
-        else if (r == ProofRule::TRUST_THEORY_REWRITE)
-        {
-          const std::vector<Node>& args = pn->getArguments();
-          builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid);
-        }
-        if (tid != THEORY_LAST)
-        {
-          output(OutputTag::TRUSTED_PROOF_STEPS) << " :theory " << tid;
-        }
-        output(OutputTag::TRUSTED_PROOF_STEPS) << ")" << std::endl;
+            << "(trusted-proof-step " << query << ")" << std::endl;
       }
       if (options().proof.checkProofSteps)
       {

diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h
@@ -74,10 +74,6 @@ class ProofFinalCallback : protected EnvObj, public ProofNodeUpdaterCallback
    * Counts number of theory ids in TRUST_THEORY_REWRITE steps.
    */
   HistogramStat<theory::TheoryId> d_trustTheoryIdCount;
-  /**
-   * Counts number of theory ids in TRUST / THEORY_LEMMA steps.
-   */
-  HistogramStat<theory::TheoryId> d_trustTheoryLemmaCount;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
   /** The minimum pedantic level of any rule encountered */