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 proof node utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "proof/proof_node.h"
      14                 :            : 
      15                 :            : #include "proof/proof_node_algorithm.h"
      16                 :            : #include "proof/proof_node_to_sexpr.h"
      17                 :            : 
      18                 :            : namespace cvc5::internal {
      19                 :            : 
      20                 :   77116976 : ProofNode::ProofNode(ProofRule id,
      21                 :            :                      const std::vector<std::shared_ptr<ProofNode>>& children,
      22                 :   77116976 :                      const std::vector<Node>& args)
      23                 :   77116976 :     : d_provenChecked(false)
      24                 :            : {
      25                 :   77116976 :   setValue(id, children, args);
      26                 :   77116976 : }
      27                 :            : 
      28                 :  573126032 : ProofRule ProofNode::getRule() const { return d_rule; }
      29                 :            : 
      30                 :  242172516 : const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const
      31                 :            : {
      32                 :  242172516 :   return d_children;
      33                 :            : }
      34                 :            : 
      35                 :  303148363 : const std::vector<Node>& ProofNode::getArguments() const { return d_args; }
      36                 :            : 
      37                 :  295267134 : Node ProofNode::getResult() const { return d_proven; }
      38                 :            : 
      39                 :     471293 : bool ProofNode::isClosed()
      40                 :            : {
      41                 :     471293 :   std::vector<Node> assumps;
      42                 :     471293 :   expr::getFreeAssumptions(this, assumps);
      43                 :     942586 :   return assumps.empty();
      44                 :     471293 : }
      45                 :            : 
      46                 :   88945426 : void ProofNode::setValue(
      47                 :            :     ProofRule id,
      48                 :            :     const std::vector<std::shared_ptr<ProofNode>>& children,
      49                 :            :     const std::vector<Node>& args)
      50                 :            : {
      51                 :   88945426 :   d_rule = id;
      52                 :   88945426 :   d_children = children;
      53                 :   88945426 :   d_args = args;
      54                 :   88945426 : }
      55                 :            : 
      56                 :        255 : void ProofNode::printDebug(std::ostream& os, bool printConclusion) const
      57                 :            : {
      58                 :            :   // convert to sexpr and print
      59                 :        255 :   ProofNodeToSExpr pnts(d_proven.getNodeManager());
      60                 :        255 :   Node ps = pnts.convertToSExpr(this, printConclusion);
      61                 :        255 :   os << ps;
      62                 :        255 : }
      63                 :            : 
      64                 :     375166 : std::shared_ptr<ProofNode> ProofNode::clone() const
      65                 :            : {
      66                 :     375166 :   std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited;
      67                 :     375166 :   std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it;
      68                 :     375166 :   std::vector<const ProofNode*> visit;
      69                 :     375166 :   std::shared_ptr<ProofNode> cloned;
      70                 :     375166 :   visit.push_back(this);
      71                 :            :   const ProofNode* cur;
      72         [ +  + ]:   28450197 :   while (!visit.empty())
      73                 :            :   {
      74                 :   28075031 :     cur = visit.back();
      75                 :   28075031 :     it = visited.find(cur);
      76         [ +  + ]:   28075031 :     if (it == visited.end())
      77                 :            :     {
      78                 :   10010314 :       visited[cur] = nullptr;
      79                 :            :       const std::vector<std::shared_ptr<ProofNode>>& children =
      80                 :   10010314 :           cur->getChildren();
      81         [ +  + ]:   27699865 :       for (const std::shared_ptr<ProofNode>& cp : children)
      82                 :            :       {
      83                 :   17689551 :         visit.push_back(cp.get());
      84                 :            :       }
      85                 :   10010314 :       continue;
      86                 :   10010314 :     }
      87                 :   18064717 :     visit.pop_back();
      88         [ +  + ]:   18064717 :     if (it->second.get() == nullptr)
      89                 :            :     {
      90                 :   10010314 :       std::vector<std::shared_ptr<ProofNode>> cchildren;
      91                 :            :       const std::vector<std::shared_ptr<ProofNode>>& children =
      92                 :   10010314 :           cur->getChildren();
      93         [ +  + ]:   27699865 :       for (const std::shared_ptr<ProofNode>& cp : children)
      94                 :            :       {
      95                 :   17689551 :         it = visited.find(cp.get());
      96 [ -  + ][ -  + ]:   17689551 :         Assert(it != visited.end());
                 [ -  - ]
      97                 :            :         // if we encounter nullptr here, then this child is currently being
      98                 :            :         // traversed at a higher level, hence this corresponds to a cyclic
      99                 :            :         // proof.
     100         [ -  + ]:   17689551 :         if (it->second == nullptr)
     101                 :            :         {
     102                 :          0 :           Unreachable() << "Cyclic proof encountered when cloning a proof node";
     103                 :            :         }
     104                 :   17689551 :         cchildren.push_back(it->second);
     105                 :            :       }
     106                 :   20020628 :       cloned = std::make_shared<ProofNode>(
     107                 :   10010314 :           cur->getRule(), cchildren, cur->getArguments());
     108                 :   10010314 :       visited[cur] = cloned;
     109                 :            :       // we trust the above cloning does not change what is proven
     110                 :   10010314 :       cloned->d_proven = cur->d_proven;
     111                 :   10010314 :       cloned->d_provenChecked = cur->d_provenChecked;
     112                 :   10010314 :     }
     113                 :            :   }
     114 [ -  + ][ -  + ]:     375166 :   Assert(visited.find(this) != visited.end());
                 [ -  - ]
     115                 :     750332 :   return visited[this];
     116                 :     375166 : }
     117                 :            : 
     118                 :          0 : std::ostream& operator<<(std::ostream& out, const ProofNode& pn)
     119                 :            : {
     120                 :          0 :   pn.printDebug(out);
     121                 :          0 :   return out;
     122                 :            : }
     123                 :            : 
     124                 :       1502 : size_t ProofNodeHashFunction::operator()(const ProofNode* pfn) const
     125                 :            : {
     126                 :       1502 :   uint64_t ret = fnv1a::offsetBasis;
     127                 :            : 
     128                 :       1502 :   ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(pfn->getResult()));
     129                 :       1502 :   ret = fnv1a::fnv1a_64(ret, static_cast<size_t>(pfn->getRule()));
     130                 :            : 
     131                 :       1502 :   const std::vector<std::shared_ptr<ProofNode>>& children = pfn->getChildren();
     132         [ +  + ]:       4354 :   for (const Pf& child : children)
     133                 :            :   {
     134                 :       2852 :     ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(child->getResult()));
     135                 :            :   }
     136                 :            : 
     137                 :       1502 :   const std::vector<Node>& args = pfn->getArguments();
     138         [ +  + ]:       3049 :   for (const Node& arg : args)
     139                 :            :   {
     140                 :       1547 :     ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(arg));
     141                 :            :   }
     142                 :            : 
     143                 :       1502 :   return static_cast<size_t>(ret);
     144                 :            : }
     145                 :            : }  // namespace cvc5::internal
     146                 :            : 
     147                 :            : namespace std {
     148                 :       1502 : size_t hash<cvc5::internal::ProofNode>::operator()(
     149                 :            :     const cvc5::internal::ProofNode& node) const
     150                 :            : {
     151                 :       1502 :   return cvc5::internal::ProofNodeHashFunction{}(&node);
     152                 :            : }
     153                 :            : }  // namespace std