Branch data     Line data    Source code

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