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                 :            :  * Term conversion sequence proof generator utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "proof/conv_seq_proof_generator.h"
      14                 :            : 
      15                 :            : #include <sstream>
      16                 :            : 
      17                 :            : #include "proof/proof_node_manager.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : 
      21                 :      20141 : TConvSeqProofGenerator::TConvSeqProofGenerator(
      22                 :            :     ProofNodeManager* pnm,
      23                 :            :     const std::vector<ProofGenerator*>& ts,
      24                 :            :     context::Context* c,
      25                 :      20141 :     std::string name)
      26                 :      20141 :     : d_pnm(pnm), d_converted(c), d_name(name)
      27                 :            : {
      28                 :      20141 :   d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end());
      29 [ -  + ][ -  + ]:      20141 :   AlwaysAssert(!d_tconvs.empty())
                 [ -  - ]
      30                 :            :       << "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty "
      31                 :          0 :          "sequence";
      32                 :      20141 : }
      33                 :            : 
      34                 :      40248 : TConvSeqProofGenerator::~TConvSeqProofGenerator() {}
      35                 :            : 
      36                 :      38570 : void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index)
      37                 :            : {
      38         [ -  + ]:      38570 :   if (t == s)
      39                 :            :   {
      40                 :            :     // no need
      41                 :          0 :     return;
      42                 :            :   }
      43                 :      38570 :   std::pair<Node, size_t> key = std::pair<Node, size_t>(t, index);
      44                 :      38570 :   d_converted[key] = s;
      45                 :      38570 : }
      46                 :            : 
      47                 :       2698 : std::shared_ptr<ProofNode> TConvSeqProofGenerator::getProofFor(Node f)
      48                 :            : {
      49         [ +  - ]:       5396 :   Trace("tconv-seq-pf-gen")
      50 [ -  + ][ -  - ]:       2698 :       << "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f
      51                 :       2698 :       << std::endl;
      52                 :       2698 :   return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1);
      53                 :            : }
      54                 :            : 
      55                 :       2698 : std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor(
      56                 :            :     Node f, size_t start, size_t end)
      57                 :            : {
      58 [ -  + ][ -  + ]:       2698 :   Assert(end < d_tconvs.size());
                 [ -  - ]
      59         [ -  + ]:       2698 :   if (f.getKind() != Kind::EQUAL)
      60                 :            :   {
      61                 :          0 :     std::stringstream serr;
      62                 :          0 :     serr << "TConvSeqProofGenerator::getProofFor: " << identify()
      63                 :          0 :          << ": fail, non-equality " << f;
      64                 :          0 :     Unhandled() << serr.str();
      65                 :            :     Trace("tconv-seq-pf-gen") << serr.str() << std::endl;
      66                 :            :     return nullptr;
      67                 :          0 :   }
      68                 :            :   // start with the left hand side of the equality
      69                 :       2698 :   Node curr = f[0];
      70                 :            :   // proofs forming transitivity chain
      71                 :       2698 :   std::vector<std::shared_ptr<ProofNode>> transChildren;
      72                 :       2698 :   std::pair<Node, size_t> currKey;
      73                 :       2698 :   NodeIndexNodeMap::iterator itc;
      74                 :            :   // convert the term in sequence
      75         [ +  + ]:       8094 :   for (size_t i = start; i <= end; i++)
      76                 :            :   {
      77                 :       5396 :     currKey = std::pair<Node, size_t>(curr, i);
      78                 :       5396 :     itc = d_converted.find(currKey);
      79                 :            :     // if we provided a conversion at this index via registerConvertedTerm
      80         [ +  - ]:       5396 :     if (itc != d_converted.end())
      81                 :            :     {
      82                 :       5396 :       Node next = (*itc).second;
      83         [ +  - ]:       5396 :       Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl;
      84                 :       5396 :       Node eq = curr.eqNode(next);
      85                 :       5396 :       std::shared_ptr<ProofNode> pf = d_tconvs[i]->getProofFor(eq);
      86                 :       5396 :       transChildren.push_back(pf);
      87                 :       5396 :       curr = next;
      88                 :       5396 :     }
      89                 :            :   }
      90                 :            :   // should end up with the right hand side of the equality
      91         [ -  + ]:       2698 :   if (curr != f[1])
      92                 :            :   {
      93                 :            :     // unexpected
      94                 :          0 :     std::stringstream serr;
      95                 :          0 :     serr << "TConvSeqProofGenerator::getProofFor: " << identify()
      96                 :          0 :          << ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)"
      97                 :          0 :          << std::endl;
      98                 :          0 :     serr << "                    source: " << f[0] << std::endl;
      99                 :          0 :     serr << "expected after conversions: " << f[1] << std::endl;
     100                 :          0 :     serr << "  actual after conversions: " << curr << std::endl;
     101                 :            : 
     102         [ -  - ]:          0 :     if (TraceIsOn("tconv-seq-pf-gen-debug"))
     103                 :            :     {
     104         [ -  - ]:          0 :       Trace("tconv-pf-gen-debug")
     105                 :          0 :           << "Printing conversion steps..." << std::endl;
     106                 :          0 :       serr << "Conversions: " << std::endl;
     107                 :          0 :       for (NodeIndexNodeMap::const_iterator it = d_converted.begin();
     108         [ -  - ]:          0 :            it != d_converted.end();
     109                 :          0 :            ++it)
     110                 :            :       {
     111                 :          0 :         serr << "(" << (*it).first.first << ", " << (*it).first.second
     112                 :          0 :              << ") -> " << (*it).second << std::endl;
     113                 :            :       }
     114                 :            :     }
     115                 :          0 :     Unhandled() << serr.str();
     116                 :            :     return nullptr;
     117                 :          0 :   }
     118                 :            :   // otherwise, make transitivity
     119                 :       2698 :   return d_pnm->mkTrans(transChildren, f);
     120                 :       2698 : }
     121                 :            : 
     122                 :     252412 : TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
     123                 :            :     const std::vector<Node>& cterms)
     124                 :            : {
     125 [ -  + ][ -  + ]:     252412 :   Assert(cterms.size() == d_tconvs.size() + 1);
                 [ -  - ]
     126         [ -  + ]:     252412 :   if (cterms[0] == cterms[cterms.size() - 1])
     127                 :            :   {
     128                 :          0 :     return TrustNode::null();
     129                 :            :   }
     130                 :     252412 :   bool useThis = false;
     131                 :     252412 :   ProofGenerator* pg = nullptr;
     132         [ +  + ]:     737951 :   for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
     133                 :            :   {
     134         [ +  + ]:     504824 :     if (cterms[i] == cterms[i + 1])
     135                 :            :     {
     136                 :     233127 :       continue;
     137                 :            :     }
     138         [ +  + ]:     271697 :     else if (pg == nullptr)
     139                 :            :     {
     140                 :            :       // Maybe the i^th generator can explain it alone, which must be the case
     141                 :            :       // if there is only one position in the sequence where the term changes.
     142                 :            :       // We may overwrite pg with this class if another step is encountered in
     143                 :            :       // this loop.
     144                 :     252412 :       pg = d_tconvs[i];
     145                 :            :     }
     146                 :            :     else
     147                 :            :     {
     148                 :            :       // need more than a single generator, use this class
     149                 :      19285 :       useThis = true;
     150                 :      19285 :       break;
     151                 :            :     }
     152                 :            :   }
     153         [ +  + ]:     252412 :   if (useThis)
     154                 :            :   {
     155                 :      19285 :     pg = this;
     156                 :            :     // if more than two steps, we must register each conversion step
     157         [ +  + ]:      57855 :     for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
     158                 :            :     {
     159                 :      38570 :       registerConvertedTerm(cterms[i], cterms[i + 1], i);
     160                 :            :     }
     161                 :            :   }
     162 [ -  + ][ -  + ]:     252412 :   Assert(pg != nullptr);
                 [ -  - ]
     163                 :     252412 :   return TrustNode::mkTrustRewrite(cterms[0], cterms[cterms.size() - 1], pg);
     164                 :            : }
     165                 :            : 
     166                 :         36 : std::string TConvSeqProofGenerator::identify() const { return d_name; }
     167                 :            : 
     168                 :            : }  // namespace cvc5::internal