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 "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__SMT__CONTEXT_MANAGER_H
      16                 :            : #define CVC5__SMT__CONTEXT_MANAGER_H
      17                 :            : 
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #include "context/context.h"
      21                 :            : #include "smt/env_obj.h"
      22                 :            : #include "smt/smt_mode.h"
      23                 :            : #include "util/result.h"
      24                 :            : #include "util/synth_result.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace smt {
      28                 :            : 
      29                 :            : class SmtDriver;
      30                 :            : class SolverEngineState;
      31                 :            : 
      32                 :            : /**
      33                 :            :  * This class manages how the SAT and user contexts should be used in
      34                 :            :  * cooperation with the SmtSolver.
      35                 :            :  */
      36                 :            : class ContextManager : protected EnvObj
      37                 :            : {
      38                 :            :  public:
      39                 :            :   ContextManager(Env& env, SolverEngineState& state);
      40                 :     141272 :   ~ContextManager() {}
      41                 :            :   /**
      42                 :            :    * Notify that we are resetting the assertions, called when a reset-assertions
      43                 :            :    * command is issued by the user.
      44                 :            :    */
      45                 :            :   void notifyResetAssertions();
      46                 :            :   /**
      47                 :            :    * Notify that we are about to call check-sat. This call is made prior to
      48                 :            :    * initializing the assertions. It processes pending pops and pushes a
      49                 :            :    * (user) context if necessary.
      50                 :            :    *
      51                 :            :    * @param hasAssumptions Whether the call to check-sat has assumptions. If
      52                 :            :    * so, we push a context.
      53                 :            :    */
      54                 :            :   void notifyCheckSat(bool hasAssumptions);
      55                 :            :   /**
      56                 :            :    * Notify that the result of the last check-sat was r. This should be called
      57                 :            :    * once immediately following notifyCheckSat() if the check-sat call
      58                 :            :    * returned normal (i.e. it was not interrupted).
      59                 :            :    *
      60                 :            :    * @param hasAssumptions Whether the prior call to check-sat had assumptions.
      61                 :            :    * If so, we pop a context.
      62                 :            :    */
      63                 :            :   void notifyCheckSatResult(bool hasAssumptions);
      64                 :            :   /**
      65                 :            :    * Setup the context, which makes a single push to maintain a global
      66                 :            :    * context around everything.
      67                 :            :    *
      68                 :            :    * @param smt The driver that handles notifications from this context
      69                 :            :    * manager
      70                 :            :    */
      71                 :            :   void setup(SmtDriver* smt);
      72                 :            :   /**
      73                 :            :    * Prepare for a shutdown of the SolverEngine, which does pending pops and
      74                 :            :    * pops the user context to zero.
      75                 :            :    */
      76                 :            :   void shutdown();
      77                 :            :   /**
      78                 :            :    * Cleanup, which pops all contexts to level zero.
      79                 :            :    */
      80                 :            :   void cleanup();
      81                 :            : 
      82                 :            :   //---------------------------- context management
      83                 :            :   /**
      84                 :            :    * Do all pending pops, which ensures that the context levels are up-to-date.
      85                 :            :    * This method should be called by the SolverEngine before using any of its
      86                 :            :    * members that rely on the context (e.g. PropEngine or TheoryEngine).
      87                 :            :    */
      88                 :            :   void doPendingPops();
      89                 :            :   /**
      90                 :            :    * Called when the user of SolverEngine issues a push. This corresponds to
      91                 :            :    * the SMT-LIB command push.
      92                 :            :    */
      93                 :            :   void userPush();
      94                 :            :   /**
      95                 :            :    * Called when the user of SolverEngine issues a pop. This corresponds to
      96                 :            :    * the SMT-LIB command pop.
      97                 :            :    */
      98                 :            :   void userPop();
      99                 :            :   //---------------------------- end context management
     100                 :            : 
     101                 :            :   //---------------------------- queries
     102                 :            :   /** Return the user context level.  */
     103                 :            :   size_t getNumUserLevels() const;
     104                 :            :   //---------------------------- end queries
     105                 :            : 
     106                 :            :  private:
     107                 :            :   /** Pushes the user and SAT contexts */
     108                 :            :   void push();
     109                 :            :   /** Pops the user and SAT contexts */
     110                 :            :   void pop();
     111                 :            :   /** Pops the user and SAT contexts to the given level */
     112                 :            :   void popto(uint32_t toLevel);
     113                 :            :   /**
     114                 :            :    * Internal push, which processes any pending pops, and pushes (if in
     115                 :            :    * incremental mode).
     116                 :            :    */
     117                 :            :   void internalPush();
     118                 :            :   /**
     119                 :            :    * Internal pop. If immediate is true, this processes any pending pops, and
     120                 :            :    * pops (if in incremental mode). Otherwise, it increments the pending pop
     121                 :            :    * counter and does nothing.
     122                 :            :    */
     123                 :            :   void internalPop(bool immediate = false);
     124                 :            :   /** Reference to the SolverEngineState */
     125                 :            :   SolverEngineState& d_state;
     126                 :            :   /** Pointer to the SmtDriver */
     127                 :            :   SmtDriver* d_smt;
     128                 :            :   /** The context levels of user pushes */
     129                 :            :   std::vector<uint32_t> d_userLevels;
     130                 :            :   /** Number of internal pops that have been deferred. */
     131                 :            :   unsigned d_pendingPops;
     132                 :            :   /**
     133                 :            :    * Internal status flag to indicate whether we have been issued a
     134                 :            :    * notifyCheckSat call and have yet to process the "postsolve" methods of
     135                 :            :    * SolverEngine via SolverEngine::notifyPostSolve().
     136                 :            :    */
     137                 :            :   bool d_needPostsolve;
     138                 :            : };
     139                 :            : 
     140                 :            : }  // namespace smt
     141                 :            : }  // namespace cvc5::internal
     142                 :            : 
     143                 :            : #endif