Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Haniel Barbosa, Gereon Kremer
       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 lazy proof utility.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "prop/minisat/opt_clauses_manager.h"
      17                 :            : 
      18                 :            : #include "proof/proof_node.h"
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace prop {
      22                 :            : 
      23                 :      41256 : OptimizedClausesManager::OptimizedClausesManager(
      24                 :            :     context::Context* context,
      25                 :            :     CDProof* parentProof,
      26                 :      41256 :     std::map<int, std::vector<std::shared_ptr<ProofNode>>>& optProofs)
      27                 :            :     : context::ContextNotifyObj(context),
      28                 :            :       d_context(context),
      29                 :            :       d_optProofs(optProofs),
      30                 :            :       d_parentProof(parentProof),
      31                 :            :       d_nodeHashSet(nullptr),
      32                 :      41256 :       d_nodeLevels(nullptr)
      33                 :            : {
      34                 :      41256 : }
      35                 :            : 
      36                 :      47584 : void OptimizedClausesManager::contextNotifyPop()
      37                 :            : {
      38                 :      47584 :   int newLvl = d_context->getLevel();
      39         [ +  - ]:      95168 :   Trace("sat-proof") << "contextNotifyPop: called with lvl " << newLvl << "\n"
      40                 :      47584 :                      << push;
      41                 :            :   // the increment is handled inside the loop, so that we can erase as we go
      42         [ +  + ]:      47842 :   for (auto it = d_optProofs.cbegin(); it != d_optProofs.cend();)
      43                 :            :   {
      44         [ +  + ]:        258 :     if (it->first <= newLvl)
      45                 :            :     {
      46         [ +  - ]:        195 :       Trace("sat-proof") << "Should re-add pfs of [" << it->first << "]:\n";
      47         [ +  + ]:       1504 :       for (const auto& pf : it->second)
      48                 :            :       {
      49                 :       2618 :         Node processedPropgation = pf->getResult();
      50         [ +  - ]:       1309 :         Trace("sat-proof") << "\t- " << processedPropgation << "\n";
      51         [ +  - ]:       1309 :         Trace("sat-proof-debug") << "\t\t{" << pf << "} " << *pf.get() << "\n";
      52                 :            :         // Note that this proof may have already been added in a previous
      53                 :            :         // pop. For example, if a proof associated with level 1 was added
      54                 :            :         // when going down from 2 to 1, but then we went up to 2 again, when
      55                 :            :         // we go back to 1 the proof will still be there. Note that if say
      56                 :            :         // we had a proof of level 1 that was added at level 2 when we were
      57                 :            :         // going down from 3, we'd still need to add it again when going to
      58                 :            :         // level 1, since it'd be popped in that case.
      59         [ +  + ]:       1309 :         if (!d_parentProof->hasStep(processedPropgation))
      60                 :            :         {
      61                 :        255 :           d_parentProof->addProof(pf);
      62                 :            :         }
      63                 :            :         else
      64                 :            :         {
      65         [ +  - ]:       2108 :           Trace("sat-proof")
      66                 :       1054 :               << "\t..skipped since its proof was already added\n";
      67                 :            :         }
      68                 :            :       }
      69                 :        195 :       ++it;
      70                 :        195 :       continue;
      71                 :            :     }
      72         [ -  + ]:         63 :     if (TraceIsOn("sat-proof"))
      73                 :            :     {
      74         [ -  - ]:          0 :       Trace("sat-proof") << "Should remove from map pfs of [" << it->first
      75                 :          0 :                          << "]:\n";
      76         [ -  - ]:          0 :       for (const auto& pf : it->second)
      77                 :            :       {
      78                 :          0 :         Trace("sat-proof") << "\t- " << pf->getResult() << "\n";
      79                 :            :       }
      80                 :            :     }
      81                 :         63 :     it = d_optProofs.erase(it);
      82                 :            :   }
      83         [ +  + ]:      47584 :   if (d_nodeHashSet)
      84                 :            :   {
      85 [ -  + ][ -  + ]:      23792 :     Assert(d_nodeLevels);
                 [ -  - ]
      86                 :            :     // traverse mapping from context levels to nodes so that we can reinsert the
      87                 :            :     // nodes that are below the current level being popped. The entries in the
      88                 :            :     // map at or above this level are deleted.
      89         [ +  + ]:      23992 :     for (auto it = d_nodeLevels->cbegin(); it != d_nodeLevels->cend();)
      90                 :            :     {
      91         [ +  + ]:        200 :       if (it->first <= newLvl)
      92                 :            :       {
      93         [ +  - ]:        372 :         Trace("sat-proof") << "Should re-add SAT assumptions of [" << it->first
      94                 :        186 :                            << "]:\n";
      95         [ +  + ]:       1528 :         for (const auto& assumption : it->second)
      96                 :            :         {
      97         [ +  - ]:       1342 :           Trace("sat-proof") << "\t- " << assumption << "\n";
      98                 :            :           // Note that since it's a hash set we do not care about repetitions
      99                 :       1342 :           d_nodeHashSet->insert(assumption);
     100                 :            :         }
     101                 :        186 :         ++it;
     102                 :        186 :         continue;
     103                 :            :       }
     104         [ +  - ]:         28 :       Trace("sat-proof") << "Should remove from map assumptions of ["
     105                 :         14 :                          << it->first << "]: " << it->second << "\n";
     106                 :         14 :       it = d_nodeLevels->erase(it);
     107                 :            :     }
     108                 :            :   }
     109         [ +  - ]:      47584 :   Trace("sat-proof") << pop;
     110                 :      47584 : }
     111                 :            : 
     112                 :      20628 : void OptimizedClausesManager::trackNodeHashSet(
     113                 :            :     context::CDHashSet<Node>* nodeHashSet,
     114                 :            :     std::map<int, std::vector<Node>>* nodeLevels)
     115                 :            : {
     116                 :      20628 :   d_nodeHashSet = nodeHashSet;
     117                 :      20628 :   d_nodeLevels = nodeLevels;
     118                 :      20628 : }
     119                 :            : 
     120                 :            : }  // namespace prop
     121                 :            : }  // namespace cvc5::internal