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 a proof generator for buffered proof steps.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "proof/buffered_proof_generator.h"
      14                 :            : 
      15                 :            : #include "proof/proof.h"
      16                 :            : #include "proof/proof_node_manager.h"
      17                 :            : 
      18                 :            : namespace cvc5::internal {
      19                 :            : 
      20                 :     157444 : BufferedProofGenerator::BufferedProofGenerator(Env& env,
      21                 :            :                                                context::Context* c,
      22                 :            :                                                bool mkUniqueAssume,
      23                 :     157444 :                                                bool autoSymm)
      24                 :            :     : EnvObj(env),
      25                 :            :       ProofGenerator(),
      26                 :     157444 :       d_facts(c),
      27                 :     157444 :       d_mkUniqueAssume(mkUniqueAssume),
      28                 :     157444 :       d_autoSymm(autoSymm),
      29                 :     157444 :       d_assumptionsToPfNodes(c)
      30                 :            : {
      31                 :     157444 : }
      32                 :            : 
      33                 :     319803 : bool BufferedProofGenerator::addStep(Node fact,
      34                 :            :                                      ProofStep ps,
      35                 :            :                                      CDPOverwrite opolicy)
      36                 :            : {
      37                 :            :   // check duplicates if we are not always overwriting
      38         [ +  - ]:     319803 :   if (opolicy != CDPOverwrite::ALWAYS)
      39                 :            :   {
      40         [ +  + ]:     319803 :     if (d_facts.find(fact) != d_facts.end())
      41                 :            :     {
      42                 :            :       // duplicate
      43                 :       1351 :       return false;
      44                 :            :     }
      45                 :     318452 :     Node symFact = CDProof::getSymmFact(fact);
      46         [ +  + ]:     318452 :     if (!symFact.isNull())
      47                 :            :     {
      48         [ -  + ]:      64467 :       if (d_facts.find(symFact) != d_facts.end())
      49                 :            :       {
      50                 :            :         // duplicate due to symmetry
      51                 :          0 :         return false;
      52                 :            :       }
      53                 :            :     }
      54         [ +  - ]:     318452 :   }
      55                 :            :   // note that this replaces the value fact is mapped to if there is already one
      56                 :     318452 :   d_facts.insert(fact, std::make_shared<ProofStep>(ps));
      57                 :     318452 :   return true;
      58                 :            : }
      59                 :            : 
      60                 :     381095 : std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact)
      61                 :            : {
      62         [ +  - ]:     762190 :   Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact
      63                 :     381095 :                          << std::endl;
      64                 :     381095 :   NodeProofStepMap::iterator it = d_facts.find(fact);
      65         [ -  + ]:     381095 :   if (it == d_facts.end())
      66                 :            :   {
      67         [ -  - ]:          0 :     if (!d_autoSymm)
      68                 :            :     {
      69                 :          0 :       return nullptr;
      70                 :            :     }
      71                 :          0 :     Node symFact = CDProof::getSymmFact(fact);
      72         [ -  - ]:          0 :     if (symFact.isNull())
      73                 :            :     {
      74         [ -  - ]:          0 :       Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
      75                 :          0 :       DebugUnhandled();
      76                 :            :       return nullptr;
      77                 :            :     }
      78                 :          0 :     it = d_facts.find(symFact);
      79         [ -  - ]:          0 :     if (it == d_facts.end())
      80                 :            :     {
      81                 :          0 :       DebugUnhandled();
      82                 :            :       Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
      83                 :            :       return nullptr;
      84                 :            :     }
      85         [ -  - ]:          0 :   }
      86         [ +  - ]:     381095 :   Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
      87                 :     762190 :   CDProof cdp(d_env, nullptr, "CDProof", d_autoSymm);
      88         [ +  + ]:     381095 :   if (d_mkUniqueAssume)
      89                 :            :   {
      90                 :            :     // Add or create assumption proof nodes for children. If child has already
      91                 :            :     // been seen, retrieve its saved assumption proof node, otherwise create via
      92                 :            :     // cdp.
      93         [ +  + ]:    5556947 :     for (const Node& n : it->second->d_children)
      94                 :            :     {
      95                 :    5317591 :       NodeProofNodeMap::iterator itChild = d_assumptionsToPfNodes.find(n);
      96         [ +  + ]:    5317591 :       if (itChild != d_assumptionsToPfNodes.end())
      97                 :            :       {
      98                 :    4741158 :         cdp.addProof(itChild->second);
      99                 :    4741158 :         continue;
     100                 :            :       }
     101                 :            :       // this call both creates an assumption proof node and saves it in cdp. We
     102                 :            :       // use the resulting proof node to store in our cache.
     103                 :     576433 :       std::shared_ptr<ProofNode> pf = cdp.getProofFor(n);
     104                 :     576433 :       d_assumptionsToPfNodes.insert(n, pf);
     105                 :     576433 :     }
     106                 :            :   }
     107                 :            :   // If we are generating unique assumptions we require that we already have
     108                 :            :   // proof steps for the premises. This must be guaranteed by the above loop and
     109                 :            :   // is what prevents the duplication of assumption proof nodes (which will be
     110                 :            :   // automatically created by the command below when they don't yet exist).
     111                 :     381095 :   cdp.addStep(fact, *(*it).second, d_mkUniqueAssume);
     112                 :     381095 :   return cdp.getProofFor(fact);
     113                 :     381095 : }
     114                 :            : 
     115                 :     118769 : bool BufferedProofGenerator::hasProofFor(Node f)
     116                 :            : {
     117                 :     118769 :   NodeProofStepMap::iterator it = d_facts.find(f);
     118         [ +  + ]:     118769 :   if (it == d_facts.end())
     119                 :            :   {
     120         [ +  - ]:      74646 :     if (!d_autoSymm)
     121                 :            :     {
     122                 :      74646 :       return false;
     123                 :            :     }
     124                 :          0 :     Node symFact = CDProof::getSymmFact(f);
     125         [ -  - ]:          0 :     if (symFact.isNull())
     126                 :            :     {
     127                 :          0 :       return false;
     128                 :            :     }
     129                 :          0 :     it = d_facts.find(symFact);
     130         [ -  - ]:          0 :     if (it == d_facts.end())
     131                 :            :     {
     132                 :          0 :       return false;
     133                 :            :     }
     134         [ -  - ]:          0 :   }
     135                 :      44123 :   return true;
     136                 :            : }
     137                 :            : 
     138                 :            : }  // namespace cvc5::internal