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                 :            :  * Utility for managing the contexts
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/context_manager.h"
      14                 :            : 
      15                 :            : #include "base/modal_exception.h"
      16                 :            : #include "options/base_options.h"
      17                 :            : #include "options/main_options.h"
      18                 :            : #include "options/option_exception.h"
      19                 :            : #include "options/smt_options.h"
      20                 :            : #include "smt/env.h"
      21                 :            : #include "smt/smt_driver.h"
      22                 :            : #include "smt/solver_engine_state.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace smt {
      26                 :            : 
      27                 :      74598 : ContextManager::ContextManager(Env& env, SolverEngineState& state)
      28                 :            :     : EnvObj(env),
      29                 :      74598 :       d_state(state),
      30                 :      74598 :       d_smt(nullptr),
      31                 :      74598 :       d_pendingPops(0),
      32                 :      74598 :       d_needPostsolve(false)
      33                 :            : {
      34                 :      74598 : }
      35                 :            : 
      36                 :        687 : void ContextManager::notifyResetAssertions()
      37                 :            : {
      38                 :        687 :   doPendingPops();
      39         [ +  + ]:       1247 :   while (!d_userLevels.empty())
      40                 :            :   {
      41                 :        560 :     userPop();
      42                 :            :   }
      43                 :            :   // Remember the global push/pop around everything when beyond Start mode
      44                 :            :   // (see solver execution modes in the SMT-LIB standard)
      45 [ +  - ][ +  - ]:        687 :   Assert(d_userLevels.size() == 0 && userContext()->getLevel() == 1);
         [ -  + ][ -  + ]
                 [ -  - ]
      46                 :        687 :   popto(0);
      47                 :            :   // push the state to maintain global context around everything
      48                 :        687 :   push();
      49                 :        687 : }
      50                 :            : 
      51                 :      48694 : void ContextManager::notifyCheckSat(bool hasAssumptions)
      52                 :            : {
      53                 :            :   // push if there are assumptions
      54         [ +  + ]:      48694 :   if (hasAssumptions)
      55                 :            :   {
      56                 :       6416 :     internalPush();
      57                 :            :   }
      58                 :      48694 : }
      59                 :            : 
      60                 :      48635 : void ContextManager::notifyCheckSatResult(bool hasAssumptions)
      61                 :            : {
      62                 :      48635 :   d_needPostsolve = true;
      63                 :            :   // Pop the context
      64         [ +  + ]:      48635 :   if (hasAssumptions)
      65                 :            :   {
      66                 :       6408 :     internalPop();
      67                 :            :   }
      68                 :      48635 : }
      69                 :            : 
      70                 :      49974 : void ContextManager::setup(SmtDriver* smt)
      71                 :            : {
      72                 :      49974 :   d_smt = smt;
      73                 :            :   // push the state to maintain global context around everything
      74                 :      49974 :   push();
      75                 :      49974 : }
      76                 :            : 
      77                 :      69611 : void ContextManager::shutdown()
      78                 :            : {
      79                 :      69611 :   doPendingPops();
      80                 :            : 
      81 [ +  + ][ +  + ]:      70379 :   while (options().base.incrementalSolving && userContext()->getLevel() > 1)
                 [ +  + ]
      82                 :            :   {
      83                 :        768 :     internalPop(true);
      84                 :            :   }
      85                 :      69611 : }
      86                 :            : 
      87                 :      69611 : void ContextManager::cleanup()
      88                 :            : {
      89                 :            :   // pop to level zero
      90                 :      69611 :   popto(0);
      91                 :      69611 : }
      92                 :            : 
      93                 :       5079 : void ContextManager::userPush()
      94                 :            : {
      95                 :            :   // notify the state
      96                 :       5079 :   d_state.notifyUserPop();
      97                 :            : 
      98                 :       5079 :   d_userLevels.push_back(userContext()->getLevel());
      99                 :       5079 :   internalPush();
     100         [ +  - ]:      10158 :   Trace("userpushpop") << "ContextManager: pushed to level "
     101                 :       5079 :                        << userContext()->getLevel() << std::endl;
     102                 :       5079 : }
     103                 :            : 
     104                 :       4310 : void ContextManager::userPop()
     105                 :            : {
     106                 :            :   // notify the state
     107                 :       4310 :   d_state.notifyUserPush();
     108                 :            : 
     109         [ -  + ]:       4310 :   if (d_userLevels.size() == 0)
     110                 :            :   {
     111                 :          0 :     throw ModalException("Cannot pop beyond the first user frame");
     112                 :            :   }
     113                 :            : 
     114 [ -  + ][ -  + ]:       4310 :   AlwaysAssert(userContext()->getLevel() > 0);
                 [ -  - ]
     115 [ -  + ][ -  + ]:       4310 :   AlwaysAssert(d_userLevels.back() < userContext()->getLevel());
                 [ -  - ]
     116         [ +  + ]:       8620 :   while (d_userLevels.back() < userContext()->getLevel())
     117                 :            :   {
     118                 :       4310 :     internalPop(true);
     119                 :            :   }
     120                 :       4310 :   d_userLevels.pop_back();
     121                 :       4310 : }
     122                 :      50661 : void ContextManager::push()
     123                 :            : {
     124                 :      50661 :   userContext()->push();
     125                 :      50661 :   context()->push();
     126                 :      50661 : }
     127                 :            : 
     128                 :          0 : void ContextManager::pop()
     129                 :            : {
     130                 :          0 :   userContext()->pop();
     131                 :          0 :   context()->pop();
     132                 :          0 : }
     133                 :            : 
     134                 :      70298 : void ContextManager::popto(uint32_t toLevel)
     135                 :            : {
     136                 :      70298 :   context()->popto(toLevel);
     137                 :      70298 :   userContext()->popto(toLevel);
     138                 :      70298 : }
     139                 :            : 
     140                 :       3657 : size_t ContextManager::getNumUserLevels() const { return d_userLevels.size(); }
     141                 :            : 
     142                 :      11495 : void ContextManager::internalPush()
     143                 :            : {
     144         [ +  - ]:      11495 :   Trace("smt") << "ContextManager::internalPush()" << std::endl;
     145                 :      11495 :   doPendingPops();
     146         [ +  + ]:      11495 :   if (options().base.incrementalSolving)
     147                 :            :   {
     148                 :            :     // notifies the SolverEngine to process the assertions immediately
     149                 :       8216 :     d_smt->notifyPushPre();
     150                 :       8216 :     userContext()->push();
     151                 :            :     // the context push is done inside of the SAT solver
     152                 :       8216 :     d_smt->notifyPushPost();
     153                 :            :   }
     154                 :      11495 : }
     155                 :            : 
     156                 :      11486 : void ContextManager::internalPop(bool immediate)
     157                 :            : {
     158         [ +  - ]:      11486 :   Trace("smt") << "ContextManager::internalPop()" << std::endl;
     159         [ +  + ]:      11486 :   if (options().base.incrementalSolving)
     160                 :            :   {
     161                 :       8212 :     ++d_pendingPops;
     162                 :            :   }
     163         [ +  + ]:      11486 :   if (immediate)
     164                 :            :   {
     165                 :       5078 :     doPendingPops();
     166                 :            :   }
     167                 :      11486 : }
     168                 :            : 
     169                 :     360024 : void ContextManager::doPendingPops()
     170                 :            : {
     171         [ +  - ]:     360024 :   Trace("smt") << "ContextManager::doPendingPops()" << std::endl;
     172 [ +  + ][ +  - ]:     360024 :   Assert(d_pendingPops == 0 || options().base.incrementalSolving);
         [ -  + ][ -  + ]
                 [ -  - ]
     173                 :            :   // check to see if a postsolve() is pending
     174         [ +  + ]:     360024 :   if (d_needPostsolve)
     175                 :            :   {
     176                 :      48512 :     d_smt->notifyPostSolve();
     177                 :      48512 :     d_needPostsolve = false;
     178                 :            :   }
     179         [ +  + ]:     368233 :   while (d_pendingPops > 0)
     180                 :            :   {
     181                 :            :     // the context pop is done inside of the SAT solver
     182                 :       8209 :     d_smt->notifyPopPre();
     183                 :            :     // pop the context
     184                 :       8209 :     userContext()->pop();
     185                 :       8209 :     --d_pendingPops;
     186                 :            :     // no need for pop post (for now)
     187                 :            :   }
     188                 :     360024 : }
     189                 :            : 
     190                 :            : }  // namespace smt
     191                 :            : }  // namespace cvc5::internal