Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * Utility for managing the contexts
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "smt/context_manager.h"
      17                 :            : 
      18                 :            : #include "base/modal_exception.h"
      19                 :            : #include "options/base_options.h"
      20                 :            : #include "options/main_options.h"
      21                 :            : #include "options/option_exception.h"
      22                 :            : #include "options/smt_options.h"
      23                 :            : #include "smt/env.h"
      24                 :            : #include "smt/smt_driver.h"
      25                 :            : #include "smt/solver_engine_state.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace smt {
      29                 :            : 
      30                 :      70104 : ContextManager::ContextManager(Env& env, SolverEngineState& state)
      31                 :            :     : EnvObj(env),
      32                 :            :       d_state(state),
      33                 :            :       d_smt(nullptr),
      34                 :            :       d_pendingPops(0),
      35                 :      70104 :       d_needPostsolve(false)
      36                 :            : {
      37                 :      70104 : }
      38                 :            : 
      39                 :        597 : void ContextManager::notifyResetAssertions()
      40                 :            : {
      41                 :        597 :   doPendingPops();
      42         [ +  + ]:       1065 :   while (!d_userLevels.empty())
      43                 :            :   {
      44                 :        468 :     userPop();
      45                 :            :   }
      46                 :            :   // Remember the global push/pop around everything when beyond Start mode
      47                 :            :   // (see solver execution modes in the SMT-LIB standard)
      48 [ +  - ][ +  - ]:       1194 :   Assert(d_userLevels.size() == 0 && userContext()->getLevel() == 1);
         [ -  + ][ -  - ]
      49                 :        597 :   popto(0);
      50                 :            :   // push the state to maintain global context around everything
      51                 :        597 :   push();
      52                 :        597 : }
      53                 :            : 
      54                 :      49047 : void ContextManager::notifyCheckSat(bool hasAssumptions)
      55                 :            : {
      56                 :            :   // push if there are assumptions
      57         [ +  + ]:      49047 :   if (hasAssumptions)
      58                 :            :   {
      59                 :       6853 :     internalPush();
      60                 :            :   }
      61                 :      49047 : }
      62                 :            : 
      63                 :      49004 : void ContextManager::notifyCheckSatResult(bool hasAssumptions)
      64                 :            : {
      65                 :      49004 :   d_needPostsolve = true;
      66                 :            :   // Pop the context
      67         [ +  + ]:      49004 :   if (hasAssumptions)
      68                 :            :   {
      69                 :       6846 :     internalPop();
      70                 :            :   }
      71                 :      49004 : }
      72                 :            : 
      73                 :      49695 : void ContextManager::setup(SmtDriver* smt)
      74                 :            : {
      75                 :      49695 :   d_smt = smt;
      76                 :            :   // push the state to maintain global context around everything
      77                 :      49695 :   push();
      78                 :      49695 : }
      79                 :            : 
      80                 :      65678 : void ContextManager::shutdown()
      81                 :            : {
      82                 :      65678 :   doPendingPops();
      83                 :            : 
      84 [ +  + ][ +  + ]:      66532 :   while (options().base.incrementalSolving && userContext()->getLevel() > 1)
                 [ +  + ]
      85                 :            :   {
      86                 :        854 :     internalPop(true);
      87                 :            :   }
      88                 :      65678 : }
      89                 :            : 
      90                 :      65678 : void ContextManager::cleanup()
      91                 :            : {
      92                 :            :   // pop to level zero
      93                 :      65678 :   popto(0);
      94                 :      65678 : }
      95                 :            : 
      96                 :       5664 : void ContextManager::userPush()
      97                 :            : {
      98                 :            :   // notify the state
      99                 :       5664 :   d_state.notifyUserPop();
     100                 :            : 
     101                 :       5664 :   d_userLevels.push_back(userContext()->getLevel());
     102                 :       5664 :   internalPush();
     103         [ +  - ]:      11328 :   Trace("userpushpop") << "ContextManager: pushed to level "
     104                 :       5664 :                        << userContext()->getLevel() << std::endl;
     105                 :       5664 : }
     106                 :            : 
     107                 :       4809 : void ContextManager::userPop()
     108                 :            : {
     109                 :            :   // notify the state
     110                 :       4809 :   d_state.notifyUserPush();
     111                 :            : 
     112         [ -  + ]:       4809 :   if (d_userLevels.size() == 0)
     113                 :            :   {
     114                 :          0 :     throw ModalException("Cannot pop beyond the first user frame");
     115                 :            :   }
     116                 :            : 
     117 [ -  + ][ -  + ]:       4809 :   AlwaysAssert(userContext()->getLevel() > 0);
                 [ -  - ]
     118 [ -  + ][ -  + ]:       4809 :   AlwaysAssert(d_userLevels.back() < userContext()->getLevel());
                 [ -  - ]
     119         [ +  + ]:       9618 :   while (d_userLevels.back() < userContext()->getLevel())
     120                 :            :   {
     121                 :       4809 :     internalPop(true);
     122                 :            :   }
     123                 :       4809 :   d_userLevels.pop_back();
     124                 :       4809 : }
     125                 :      50292 : void ContextManager::push()
     126                 :            : {
     127                 :      50292 :   userContext()->push();
     128                 :      50292 :   context()->push();
     129                 :      50292 : }
     130                 :            : 
     131                 :          0 : void ContextManager::pop()
     132                 :            : {
     133                 :          0 :   userContext()->pop();
     134                 :          0 :   context()->pop();
     135                 :          0 : }
     136                 :            : 
     137                 :      66275 : void ContextManager::popto(uint32_t toLevel)
     138                 :            : {
     139                 :      66275 :   context()->popto(toLevel);
     140                 :      66275 :   userContext()->popto(toLevel);
     141                 :      66275 : }
     142                 :            : 
     143                 :       4224 : size_t ContextManager::getNumUserLevels() const { return d_userLevels.size(); }
     144                 :            : 
     145                 :      12517 : void ContextManager::internalPush()
     146                 :            : {
     147         [ +  - ]:      12517 :   Trace("smt") << "ContextManager::internalPush()" << std::endl;
     148                 :      12517 :   doPendingPops();
     149         [ +  + ]:      12517 :   if (options().base.incrementalSolving)
     150                 :            :   {
     151                 :            :     // notifies the SolverEngine to process the assertions immediately
     152                 :       9045 :     d_smt->notifyPushPre();
     153                 :       9045 :     userContext()->push();
     154                 :            :     // the context push is done inside of the SAT solver
     155                 :       9045 :     d_smt->notifyPushPost();
     156                 :            :   }
     157                 :      12517 : }
     158                 :            : 
     159                 :      12509 : void ContextManager::internalPop(bool immediate)
     160                 :            : {
     161         [ +  - ]:      12509 :   Trace("smt") << "ContextManager::internalPop()" << std::endl;
     162         [ +  + ]:      12509 :   if (options().base.incrementalSolving)
     163                 :            :   {
     164                 :       9041 :     ++d_pendingPops;
     165                 :            :   }
     166         [ +  + ]:      12509 :   if (immediate)
     167                 :            :   {
     168                 :       5663 :     doPendingPops();
     169                 :            :   }
     170                 :      12509 : }
     171                 :            : 
     172                 :     381719 : void ContextManager::doPendingPops()
     173                 :            : {
     174         [ +  - ]:     381719 :   Trace("smt") << "ContextManager::doPendingPops()" << std::endl;
     175 [ +  + ][ -  + ]:     381719 :   Assert(d_pendingPops == 0 || options().base.incrementalSolving);
         [ -  + ][ -  - ]
     176                 :            :   // check to see if a postsolve() is pending
     177         [ +  + ]:     381719 :   if (d_needPostsolve)
     178                 :            :   {
     179                 :      48910 :     d_smt->notifyPostSolve();
     180                 :      48910 :     d_needPostsolve = false;
     181                 :            :   }
     182         [ +  + ]:     390759 :   while (d_pendingPops > 0)
     183                 :            :   {
     184                 :            :     // the context pop is done inside of the SAT solver
     185                 :       9040 :     d_smt->notifyPopPre();
     186                 :            :     // pop the context
     187                 :       9040 :     userContext()->pop();
     188                 :       9040 :     --d_pendingPops;
     189                 :            :     // no need for pop post (for now)
     190                 :            :   }
     191                 :     381719 : }
     192                 :            : 
     193                 :            : }  // namespace smt
     194                 :            : }  // namespace cvc5::internal