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