Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of module for final processing proof nodes.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/proof_final_callback.h"
      14                 :            : 
      15                 :            : #include "expr/skolem_manager.h"
      16                 :            : #include "options/base_options.h"
      17                 :            : #include "options/proof_options.h"
      18                 :            : #include "proof/alf/alf_printer.h"
      19                 :            : #include "proof/proof_checker.h"
      20                 :            : #include "proof/proof_node_manager.h"
      21                 :            : #include "rewriter/rewrite_proof_rule.h"
      22                 :            : #include "smt/env.h"
      23                 :            : #include "smt/set_defaults.h"
      24                 :            : #include "theory/builtin/proof_checker.h"
      25                 :            : #include "theory/smt_engine_subsolver.h"
      26                 :            : #include "theory/theory_id.h"
      27                 :            : 
      28                 :            : using namespace cvc5::internal::kind;
      29                 :            : using namespace cvc5::internal::theory;
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : namespace smt {
      33                 :            : 
      34                 :      19128 : ProofFinalCallback::ProofFinalCallback(Env& env)
      35                 :            :     : EnvObj(env),
      36                 :      19128 :       d_ruleCount(statisticsRegistry().registerHistogram<ProofRule>(
      37                 :            :           "finalProof::ruleCount")),
      38                 :      19128 :       d_ruleEouCount(statisticsRegistry().registerHistogram<ProofRule>(
      39                 :            :           "finalProof::ruleUnhandledEoCount")),
      40                 :      19128 :       d_instRuleIds(statisticsRegistry().registerHistogram<theory::InferenceId>(
      41                 :            :           "finalProof::instRuleId")),
      42                 :      19128 :       d_dslRuleCount(statisticsRegistry().registerHistogram<ProofRewriteRule>(
      43                 :            :           "finalProof::dslRuleCount")),
      44                 :            :       d_theoryRewriteRuleCount(
      45                 :      19128 :           statisticsRegistry().registerHistogram<ProofRewriteRule>(
      46                 :            :               "finalProof::theoryRewriteRuleCount")),
      47                 :            :       d_theoryRewriteEouCount(
      48                 :      19128 :           statisticsRegistry().registerHistogram<ProofRewriteRule>(
      49                 :            :               "finalProof::theoryRewriteRuleUnhandledEoCount")),
      50                 :      19128 :       d_trustIds(statisticsRegistry().registerHistogram<TrustId>(
      51                 :            :           "finalProof::trustCount")),
      52                 :            :       d_trustTheoryRewriteCount(
      53                 :      19128 :           statisticsRegistry().registerHistogram<theory::TheoryId>(
      54                 :            :               "finalProof::trustTheoryRewriteCount")),
      55                 :            :       d_trustTheoryLemmaCount(
      56                 :      19128 :           statisticsRegistry().registerHistogram<theory::TheoryId>(
      57                 :            :               "finalProof::trustTheoryLemmaCount")),
      58                 :            :       d_totalRuleCount(
      59                 :      19128 :           statisticsRegistry().registerInt("finalProof::totalRuleCount")),
      60                 :            :       d_minPedanticLevel(
      61                 :      19128 :           statisticsRegistry().registerInt("finalProof::minPedanticLevel")),
      62                 :            :       d_numFinalProofs(
      63                 :      19128 :           statisticsRegistry().registerInt("finalProofs::numFinalProofs")),
      64                 :      19128 :       d_pedanticFailure(false),
      65                 :      38256 :       d_checkProofHoles(false)
      66                 :            : {
      67                 :      19128 :   d_minPedanticLevel += 10;
      68                 :      19128 : }
      69                 :            : 
      70                 :       2418 : void ProofFinalCallback::initializeUpdate()
      71                 :            : {
      72                 :       2418 :   d_pedanticFailure = false;
      73                 :       2418 :   d_pedanticFailureOut.str("");
      74                 :       2418 :   ++d_numFinalProofs;
      75                 :       2418 :   d_checkProofHoles =
      76 [ +  - ][ -  + ]:       2418 :       options().base.statisticsInternal || options().proof.checkProofsComplete;
      77                 :       2418 : }
      78                 :            : 
      79                 :    2219872 : void ProofFinalCallback::finalize(std::shared_ptr<ProofNode> pn)
      80                 :            : {
      81                 :    2219872 :   ProofRule r = pn->getRule();
      82                 :    2219872 :   ProofNodeManager* pnm = d_env.getProofNodeManager();
      83 [ -  + ][ -  + ]:    2219872 :   Assert(pnm != nullptr);
                 [ -  - ]
      84                 :            :   // if not doing eager pedantic checking, fail if below threshold
      85         [ +  + ]:    2219872 :   if (options().proof.proofCheck != options::ProofCheckMode::EAGER)
      86                 :            :   {
      87         [ +  - ]:    2216577 :     if (!d_pedanticFailure)
      88                 :            :     {
      89 [ -  + ][ -  + ]:    2216577 :       Assert(d_pedanticFailureOut.str().empty());
                 [ -  - ]
      90         [ -  + ]:    2216577 :       if (pnm->getChecker()->isPedanticFailure(r, &d_pedanticFailureOut))
      91                 :            :       {
      92                 :          0 :         d_pedanticFailure = true;
      93                 :            :       }
      94                 :            :     }
      95                 :            :   }
      96         [ +  + ]:    2219872 :   if (options().proof.proofCheck != options::ProofCheckMode::NONE)
      97                 :            :   {
      98                 :    2205763 :     pnm->ensureChecked(pn.get());
      99                 :            :   }
     100                 :    2219872 :   uint32_t plevel = pnm->getChecker()->getPedanticLevel(r);
     101         [ +  + ]:    2219872 :   if (plevel != 0)
     102                 :            :   {
     103                 :       1906 :     d_minPedanticLevel.minAssign(plevel);
     104                 :            :   }
     105                 :            :   // if not taking statistics or checking completeness, don't bother computing
     106                 :            :   // the following
     107         [ -  + ]:    2219872 :   if (d_checkProofHoles)
     108                 :            :   {
     109                 :            :     // record stats for the rule
     110                 :          0 :     d_ruleCount << r;
     111                 :          0 :     bool isHandled = proof::AlfPrinter::isHandled(options(), pn.get());
     112         [ -  - ]:          0 :     if (!isHandled)
     113                 :            :     {
     114                 :          0 :       d_ruleEouCount << r;
     115                 :            :     }
     116                 :          0 :     ++d_totalRuleCount;
     117                 :          0 :     TheoryId trustTid = THEORY_BUILTIN;
     118                 :          0 :     TrustId trustId = TrustId::NONE;
     119                 :          0 :     ProofRewriteRule dslId = ProofRewriteRule::NONE;
     120                 :            :     // if a DSL rewrite, take DSL stat
     121 [ -  - ][ -  - ]:          0 :     if (r == ProofRule::DSL_REWRITE || r == ProofRule::THEORY_REWRITE)
     122                 :            :     {
     123                 :          0 :       const std::vector<Node>& args = pn->getArguments();
     124                 :          0 :       rewriter::getRewriteRule(args[0], dslId);
     125                 :          0 :       Assert(dslId != ProofRewriteRule::NONE);
     126         [ -  - ]:          0 :       if (r == ProofRule::DSL_REWRITE)
     127                 :            :       {
     128                 :          0 :         d_dslRuleCount << dslId;
     129                 :            :       }
     130                 :            :       else
     131                 :            :       {
     132         [ -  - ]:          0 :         if (!isHandled)
     133                 :            :         {
     134                 :          0 :           d_theoryRewriteEouCount << dslId;
     135                 :            :         }
     136                 :          0 :         d_theoryRewriteRuleCount << dslId;
     137                 :            :       }
     138                 :          0 :     }
     139                 :            :     // take stats on the instantiations in the proof
     140         [ -  - ]:          0 :     else if (r == ProofRule::INSTANTIATE)
     141                 :            :     {
     142                 :          0 :       Node q = pn->getChildren()[0]->getResult();
     143                 :          0 :       const std::vector<Node>& args = pn->getArguments();
     144         [ -  - ]:          0 :       if (args.size() > 1)
     145                 :            :       {
     146                 :            :         InferenceId id;
     147         [ -  - ]:          0 :         if (getInferenceId(args[1], id))
     148                 :            :         {
     149                 :          0 :           d_instRuleIds << id;
     150                 :            :         }
     151                 :            :       }
     152                 :          0 :     }
     153         [ -  - ]:          0 :     else if (r == ProofRule::TRUST)
     154                 :            :     {
     155         [ -  - ]:          0 :       if (getTrustId(pn->getArguments()[0], trustId))
     156                 :            :       {
     157                 :          0 :         d_trustIds << trustId;
     158         [ -  - ]:          0 :         if (trustId == TrustId::THEORY_LEMMA)
     159                 :            :         {
     160                 :          0 :           const std::vector<Node>& args = pn->getArguments();
     161         [ -  - ]:          0 :           if (args.size() >= 3)
     162                 :            :           {
     163                 :          0 :             builtin::BuiltinProofRuleChecker::getTheoryId(args[2], trustTid);
     164                 :            :           }
     165                 :          0 :           d_trustTheoryLemmaCount << trustTid;
     166                 :            :         }
     167                 :            :       }
     168                 :            :     }
     169         [ -  - ]:          0 :     else if (r == ProofRule::TRUST_THEORY_REWRITE)
     170                 :            :     {
     171                 :          0 :       const std::vector<Node>& args = pn->getArguments();
     172                 :          0 :       Node eq = args[0];
     173                 :          0 :       builtin::BuiltinProofRuleChecker::getTheoryId(args[1], trustTid);
     174                 :          0 :       d_trustTheoryRewriteCount << trustTid;
     175                 :          0 :     }
     176                 :            :     // If the rule is not handled, and we are checking for complete proofs
     177                 :          0 :     if (!isHandled && options().proof.checkProofsComplete)
     178                 :            :     {
     179                 :            :       // internal error if hardFailure is true
     180                 :          0 :       std::stringstream ss;
     181                 :          0 :       ss << "The proof was incomplete";
     182         [ -  - ]:          0 :       if (r == ProofRule::TRUST)
     183                 :            :       {
     184                 :          0 :         ss << " due to a trust step with id " << trustId;
     185         [ -  - ]:          0 :         if (trustId == TrustId::THEORY_LEMMA)
     186                 :            :         {
     187                 :          0 :           ss << ", from theory " << trustTid;
     188                 :            :         }
     189                 :            :       }
     190         [ -  - ]:          0 :       else if (r == ProofRule::TRUST_THEORY_REWRITE)
     191                 :            :       {
     192                 :          0 :         ss << " due to a trusted theory rewrite from theory " << trustTid;
     193                 :            :       }
     194         [ -  - ]:          0 :       else if (r == ProofRule::THEORY_REWRITE)
     195                 :            :       {
     196                 :          0 :         ss << " due to an unhandled instance of rewrite rule " << dslId;
     197                 :            :       }
     198                 :            :       else
     199                 :            :       {
     200                 :          0 :         ss << " due to an unhandled instance of proof rule " << r;
     201                 :            :       }
     202                 :          0 :       ss << ".";
     203                 :          0 :       InternalError() << ss.str();
     204                 :          0 :     }
     205                 :            :   }
     206                 :            : 
     207                 :    2219872 :   if (options().proof.checkProofSteps
     208 [ +  + ][ +  + ]:    2219872 :       || isOutputOn(OutputTag::TRUSTED_PROOF_STEPS))
                 [ +  + ]
     209                 :            :   {
     210                 :        153 :     Node conc = pn->getResult();
     211                 :        153 :     ProofChecker* pc = pnm->getChecker();
     212         [ +  + ]:        153 :     if (pc->getPedanticLevel(r) == 0)
     213                 :            :     {
     214                 :            :       // no need to check
     215                 :            :     }
     216                 :            :     else
     217                 :            :     {
     218                 :          6 :       std::vector<Node> premises;
     219                 :          6 :       const std::vector<std::shared_ptr<ProofNode>>& pnc = pn->getChildren();
     220         [ -  + ]:          6 :       for (const std::shared_ptr<ProofNode>& pncc : pnc)
     221                 :            :       {
     222                 :          0 :         premises.push_back(pncc->getResult());
     223                 :            :       }
     224                 :          6 :       NodeManager* nm = nodeManager();
     225                 :          6 :       Node query = conc;
     226         [ -  + ]:          6 :       if (!premises.empty())
     227                 :            :       {
     228                 :          0 :         query = nm->mkNode(Kind::IMPLIES, nm->mkAnd(premises), query);
     229                 :            :       }
     230                 :            :       // print the trusted step information
     231         [ +  + ]:          6 :       if (isOutputOn(OutputTag::TRUSTED_PROOF_STEPS))
     232                 :            :       {
     233                 :          1 :         output(OutputTag::TRUSTED_PROOF_STEPS)
     234                 :          1 :             << "(trusted-proof-step " << query;
     235                 :          1 :         output(OutputTag::TRUSTED_PROOF_STEPS) << " :rule " << r;
     236                 :          1 :         TheoryId tid = THEORY_LAST;
     237         [ -  + ]:          1 :         if (r == ProofRule::TRUST)
     238                 :            :         {
     239                 :            :           TrustId id;
     240         [ -  - ]:          0 :           if (getTrustId(pn->getArguments()[0], id))
     241                 :            :           {
     242                 :          0 :             output(OutputTag::TRUSTED_PROOF_STEPS) << " :trust-id " << id;
     243         [ -  - ]:          0 :             if (id == TrustId::THEORY_LEMMA)
     244                 :            :             {
     245                 :          0 :               const std::vector<Node>& args = pn->getArguments();
     246         [ -  - ]:          0 :               if (args.size() >= 3)
     247                 :            :               {
     248                 :          0 :                 builtin::BuiltinProofRuleChecker::getTheoryId(args[2], tid);
     249                 :            :               }
     250                 :            :             }
     251                 :            :           }
     252                 :            :         }
     253         [ +  - ]:          1 :         else if (r == ProofRule::TRUST_THEORY_REWRITE)
     254                 :            :         {
     255                 :          1 :           const std::vector<Node>& args = pn->getArguments();
     256                 :          1 :           builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid);
     257                 :            :         }
     258         [ +  - ]:          1 :         if (tid != THEORY_LAST)
     259                 :            :         {
     260                 :          1 :           output(OutputTag::TRUSTED_PROOF_STEPS) << " :theory " << tid;
     261                 :            :         }
     262                 :          1 :         output(OutputTag::TRUSTED_PROOF_STEPS) << ")" << std::endl;
     263                 :            :       }
     264         [ +  + ]:          6 :       if (options().proof.checkProofSteps)
     265                 :            :       {
     266                 :            :         // trust the rewriter here, since the subsolver will rewrite anyways
     267                 :          5 :         query = rewrite(query);
     268                 :            :         // We use the original form of the query, which is a logically
     269                 :            :         // stronger formula. This may make it possible or easier to prove.
     270                 :          5 :         query = SkolemManager::getOriginalForm(query);
     271                 :            :         // set up the subsolver
     272                 :          5 :         Options subOptions;
     273                 :          5 :         subOptions.copyValues(d_env.getOptions());
     274                 :          5 :         smt::SetDefaults::disableChecking(subOptions);
     275                 :          5 :         SubsolverSetupInfo ssi(d_env, subOptions);
     276         [ +  - ]:         10 :         Trace("check-proof-steps")
     277                 :          5 :             << "Check: " << r << " : " << query << std::endl;
     278                 :          5 :         Result res = checkWithSubsolver(query.notNode(), ssi, true, 5000);
     279         [ +  - ]:          5 :         Trace("check-proof-steps") << "...got " << res << std::endl;
     280         [ -  + ]:          5 :         if (res != Result::UNSAT)
     281                 :            :         {
     282         [ -  - ]:          0 :           Warning() << "A proof step may not hold: " << r << " proving "
     283                 :          0 :                     << query;
     284         [ -  - ]:          0 :           Warning() << ", result from check-sat was: " << res << std::endl;
     285         [ -  - ]:          0 :           Trace("check-proof-steps")
     286                 :          0 :               << "Original conclusion: " << conc << std::endl;
     287                 :            :         }
     288                 :          5 :       }
     289                 :          6 :     }
     290                 :        153 :   }
     291                 :    2219872 : }
     292                 :            : 
     293                 :       2418 : bool ProofFinalCallback::wasPedanticFailure(std::ostream& out) const
     294                 :            : {
     295         [ -  + ]:       2418 :   if (d_pedanticFailure)
     296                 :            :   {
     297                 :          0 :     out << d_pedanticFailureOut.str();
     298                 :          0 :     return true;
     299                 :            :   }
     300                 :       2418 :   return false;
     301                 :            : }
     302                 :            : 
     303                 :            : }  // namespace smt
     304                 :            : }  // namespace cvc5::internal