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                 :            :  * Proof logger utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/proof_logger.h"
      14                 :            : 
      15                 :            : #include "proof/proof.h"
      16                 :            : #include "proof/proof_node_manager.h"
      17                 :            : #include "smt/proof_manager.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : 
      21                 :          0 : ProofLoggerCpc::ProofLoggerCpc(Env& env,
      22                 :            :                                std::ostream& out,
      23                 :            :                                smt::PfManager* pm,
      24                 :          0 :                                smt::Assertions& as)
      25                 :            :     : ProofLogger(env),
      26                 :          0 :       d_pm(pm),
      27                 :          0 :       d_pnm(pm->getProofNodeManager()),
      28                 :          0 :       d_as(as),
      29                 :          0 :       d_atp(nodeManager()),
      30                 :            :       // we use thresh 1 since terms may come incrementally and would benefit
      31                 :            :       // from previous eager letification
      32                 :          0 :       d_alfp(env, d_atp, pm->getRewriteDatabase(), 1),
      33                 :          0 :       d_aout(out, d_alfp.getLetBinding(), "@t", false)
      34                 :            : {
      35         [ -  - ]:          0 :   Trace("pf-log-debug") << "Make proof logger" << std::endl;
      36                 :            :   // global options on out
      37                 :          0 :   options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
      38                 :          0 :   options::ioutils::applyPrintArithLitToken(out, true);
      39                 :          0 :   options::ioutils::applyPrintSkolemDefinitions(out, true);
      40                 :          0 : }
      41                 :            : 
      42                 :          0 : ProofLoggerCpc::~ProofLoggerCpc() {}
      43                 :            : 
      44                 :          0 : void ProofLoggerCpc::logCnfPreprocessInputs(const std::vector<Node>& inputs)
      45                 :            : {
      46                 :          0 :   d_aout.getOStream() << "; log start" << std::endl;
      47         [ -  - ]:          0 :   Trace("pf-log") << "; log: cnf preprocess input proof start" << std::endl;
      48                 :          0 :   CDProof cdp(d_env);
      49                 :          0 :   Node conc = nodeManager()->mkAnd(inputs);
      50                 :          0 :   cdp.addTrustedStep(conc, TrustId::PREPROCESSED_INPUT, inputs, {});
      51                 :          0 :   std::shared_ptr<ProofNode> pfn = cdp.getProofFor(conc);
      52                 :          0 :   ProofScopeMode m = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS;
      53                 :          0 :   d_ppProof = d_pm->connectProofToAssertions(pfn, d_as, m);
      54                 :          0 :   d_alfp.print(d_aout, d_ppProof, m);
      55         [ -  - ]:          0 :   Trace("pf-log") << "; log: cnf preprocess input proof end" << std::endl;
      56                 :          0 : }
      57                 :            : 
      58                 :          0 : void ProofLoggerCpc::logCnfPreprocessInputProofs(
      59                 :            :     std::vector<std::shared_ptr<ProofNode>>& pfns)
      60                 :            : {
      61         [ -  - ]:          0 :   Trace("pf-log") << "; log: cnf preprocess input proof start" << std::endl;
      62                 :            :   // if the assertions are empty, we do nothing. We will answer sat.
      63                 :          0 :   std::shared_ptr<ProofNode> pfn;
      64         [ -  - ]:          0 :   if (!pfns.empty())
      65                 :            :   {
      66         [ -  - ]:          0 :     if (pfns.size() == 1)
      67                 :            :     {
      68                 :          0 :       pfn = pfns[0];
      69                 :            :     }
      70                 :            :     else
      71                 :            :     {
      72                 :          0 :       pfn = d_pnm->mkNode(ProofRule::AND_INTRO, pfns, {});
      73                 :            :     }
      74                 :          0 :     ProofScopeMode m = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS;
      75                 :          0 :     d_ppProof = d_pm->connectProofToAssertions(pfn, d_as, m);
      76                 :          0 :     d_alfp.print(d_aout, d_ppProof, m);
      77                 :            :   }
      78         [ -  - ]:          0 :   Trace("pf-log") << "; log: cnf preprocess input proof end" << std::endl;
      79                 :          0 : }
      80                 :            : 
      81                 :          0 : void ProofLoggerCpc::logTheoryLemmaProof(std::shared_ptr<ProofNode>& pfn)
      82                 :            : {
      83                 :          0 :   Trace("pf-log") << "; log theory lemma proof start " << pfn->getResult()
      84                 :          0 :                   << std::endl;
      85                 :          0 :   d_lemmaPfs.emplace_back(pfn);
      86                 :          0 :   d_alfp.printNext(d_aout, pfn);
      87         [ -  - ]:          0 :   Trace("pf-log") << "; log theory lemma proof end" << std::endl;
      88                 :          0 : }
      89                 :            : 
      90                 :          0 : void ProofLoggerCpc::logTheoryLemma(const Node& n)
      91                 :            : {
      92         [ -  - ]:          0 :   Trace("pf-log") << "; log theory lemma start " << n << std::endl;
      93                 :            :   std::shared_ptr<ProofNode> ptl =
      94                 :          0 :       d_pnm->mkTrustedNode(TrustId::THEORY_LEMMA, {}, {}, n);
      95                 :          0 :   d_lemmaPfs.emplace_back(ptl);
      96                 :          0 :   d_alfp.printNext(d_aout, ptl);
      97         [ -  - ]:          0 :   Trace("pf-log") << "; log theory lemma end" << std::endl;
      98                 :          0 : }
      99                 :            : 
     100                 :          0 : void ProofLoggerCpc::logSatRefutation()
     101                 :            : {
     102         [ -  - ]:          0 :   Trace("pf-log") << "; log SAT refutation start" << std::endl;
     103                 :          0 :   std::vector<std::shared_ptr<ProofNode>> premises;
     104                 :          0 :   Assert(d_ppProof->getRule() == ProofRule::SCOPE);
     105                 :          0 :   Assert(d_ppProof->getChildren()[0]->getRule() == ProofRule::SCOPE);
     106                 :            :   std::shared_ptr<ProofNode> ppBody =
     107                 :          0 :       d_ppProof->getChildren()[0]->getChildren()[0];
     108                 :          0 :   premises.emplace_back(ppBody);
     109                 :          0 :   premises.insert(premises.end(), d_lemmaPfs.begin(), d_lemmaPfs.end());
     110                 :          0 :   Node f = nodeManager()->mkConst(false);
     111                 :            :   std::shared_ptr<ProofNode> psr =
     112                 :          0 :       d_pnm->mkNode(ProofRule::SAT_REFUTATION, premises, {}, f);
     113                 :          0 :   d_alfp.printNext(d_aout, psr);
     114         [ -  - ]:          0 :   Trace("pf-log") << "; log SAT refutation end" << std::endl;
     115                 :            :   // for now, to avoid checking failure
     116                 :          0 :   d_aout.getOStream() << "(exit)" << std::endl;
     117                 :          0 : }
     118                 :            : 
     119                 :          0 : void ProofLoggerCpc::logSatRefutationProof(std::shared_ptr<ProofNode>& pfn)
     120                 :            : {
     121         [ -  - ]:          0 :   Trace("pf-log") << "; log SAT refutation proof start" << std::endl;
     122                 :            :   // connect to preprocessed
     123                 :            :   std::shared_ptr<ProofNode> spf =
     124                 :          0 :       d_pm->connectProofToAssertions(pfn, d_as, ProofScopeMode::NONE);
     125                 :          0 :   d_alfp.printNext(d_aout, spf);
     126         [ -  - ]:          0 :   Trace("pf-log") << "; log SAT refutation proof end" << std::endl;
     127                 :            :   // for now, to avoid checking failure
     128                 :          0 :   d_aout.getOStream() << "(exit)" << std::endl;
     129                 :          0 : }
     130                 :            : 
     131                 :            : }  // namespace cvc5::internal