Branch data     Line data    Source code

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