Branch data     Line data    Source code

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