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 maintaining the state of the SMT engine.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__SMT__SMT_ENGINE_STATE_H
      16                 :            : #define CVC5__SMT__SMT_ENGINE_STATE_H
      17                 :            : 
      18                 :            : #include <string>
      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                 :            : 
      28                 :            : class SolverEngine;
      29                 :            : 
      30                 :            : namespace smt {
      31                 :            : 
      32                 :            : /**
      33                 :            :  * This utility is responsible for maintaining the basic state of the
      34                 :            :  * SolverEngine.
      35                 :            :  *
      36                 :            :  * It has no concept of anything related to the assertions of the SolverEngine,
      37                 :            :  * or more generally it does not depend on Node.
      38                 :            :  *
      39                 :            :  * This class has three sets of interfaces:
      40                 :            :  * (1) notification methods that are used by SolverEngine to notify when an
      41                 :            :  * event occurs (e.g. the beginning of a check-sat call), (2) general
      42                 :            :  * information queries, including the mode that the SolverEngine is in, based on
      43                 :            :  * the notifications it has received.
      44                 :            :  */
      45                 :            : class SolverEngineState : protected EnvObj
      46                 :            : {
      47                 :            :  public:
      48                 :            :   SolverEngineState(Env& env);
      49                 :     141462 :   ~SolverEngineState() {}
      50                 :            :   /**
      51                 :            :    * Notify that the expected status of the next check-sat is given by the
      52                 :            :    * string status, which should be one of "sat", "unsat" or "unknown".
      53                 :            :    */
      54                 :            :   void notifyExpectedStatus(const std::string& status);
      55                 :            :   /**
      56                 :            :    * Notify that the SolverEngine is fully initialized, which is called when
      57                 :            :    * options are finalized.
      58                 :            :    */
      59                 :            :   void notifyFullyInited();
      60                 :            :   /**
      61                 :            :    * Notify there was a declaration
      62                 :            :    */
      63                 :            :   void notifyDeclaration();
      64                 :            :   /**
      65                 :            :    * Notify that we are about to call check-sat. This call is made prior to
      66                 :            :    * initializing the assertions.
      67                 :            :    */
      68                 :            :   void notifyCheckSat();
      69                 :            :   /**
      70                 :            :    * Called when the user of SolverEngine issues a push. This corresponds to
      71                 :            :    * the SMT-LIB command push.
      72                 :            :    */
      73                 :            :   void notifyUserPush();
      74                 :            :   /**
      75                 :            :    * Called when the user of SolverEngine issues a pop. This corresponds to
      76                 :            :    * the SMT-LIB command pop.
      77                 :            :    */
      78                 :            :   void notifyUserPop();
      79                 :            :   /**
      80                 :            :    * Notify that the result of the last check-sat was r. This should be called
      81                 :            :    * once immediately following notifyCheckSat() if the check-sat call
      82                 :            :    * returned normal (i.e. it was not interupted).
      83                 :            :    *
      84                 :            :    * @param r The result of the check-sat call.
      85                 :            :    */
      86                 :            :   void notifyCheckSatResult(const Result& r);
      87                 :            :   /**
      88                 :            :    * Notify that the result of the last check-synth or check-synth-next was r.
      89                 :            :    * @param r The result of the check-synth or check-synth-next call.
      90                 :            :    */
      91                 :            :   void notifyCheckSynthResult(const SynthResult& r);
      92                 :            :   /**
      93                 :            :    * Notify that we finished an abduction query, where success is whether the
      94                 :            :    * command was successful. This is managed independently of the above
      95                 :            :    * calls for notifying check-sat. In other words, if a get-abduct command
      96                 :            :    * is issued to an SolverEngine, it may use a satisfiability call (if desired)
      97                 :            :    * to solve the abduction query. This method is called *in addition* to
      98                 :            :    * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
      99                 :            :    * In particular, it is called after these two methods are completed.
     100                 :            :    * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction
     101                 :            :    * was successful.
     102                 :            :    */
     103                 :            :   void notifyGetAbduct(bool success);
     104                 :            :   /**
     105                 :            :    * Notify that we finished an interpolation query, where success is whether
     106                 :            :    * the command was successful. This is managed independently of the above
     107                 :            :    * calls for notifying check-sat. In other words, if a get-interpolant command
     108                 :            :    * is issued to an SolverEngine, it may use a satisfiability call (if desired)
     109                 :            :    * to solve the interpolation query. This method is called *in addition* to
     110                 :            :    * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
     111                 :            :    * In particular, it is called after these two methods are completed.
     112                 :            :    * This overwrites the SMT mode to the "INTERPOL" mode if the call to
     113                 :            :    * interpolation was successful.
     114                 :            :    */
     115                 :            :   void notifyGetInterpol(bool success);
     116                 :            :   /**
     117                 :            :    * Notify that we finished a find-synth or find-synth-next query, where
     118                 :            :    * success is whether the command was successful.
     119                 :            :    */
     120                 :            :   void notifyFindSynth(bool success);
     121                 :            :   /**
     122                 :            :    * Set that we are in a fully initialized state.
     123                 :            :    */
     124                 :            :   void markFinishInit();
     125                 :            : 
     126                 :            :   //---------------------------- queries
     127                 :            :   /**
     128                 :            :    * Return true if the SolverEngine is fully initialized (post-construction).
     129                 :            :    * This post-construction initialization is automatically triggered by the
     130                 :            :    * use of the SolverEngine; e.g. when the first formula is asserted, a call
     131                 :            :    * to simplify() is issued, a scope is pushed, etc.
     132                 :            :    */
     133                 :            :   bool isFullyInited() const;
     134                 :            :   /**
     135                 :            :    * @return True if a call to check-sat or check-synth has been made and
     136                 :            :    * completed. Other calls (e.g., get-interpolant, get-abduct, get-qe) do not
     137                 :            :    * impact this, since they are handled independently via subsolvers.
     138                 :            :    */
     139                 :            :   bool isQueryMade() const;
     140                 :            :   /** Get the status of the last check-sat */
     141                 :            :   Result getStatus() const;
     142                 :            :   /** Get the SMT mode we are in */
     143                 :            :   SmtMode getMode() const;
     144                 :            :   //---------------------------- end queries
     145                 :            : 
     146                 :            :  private:
     147                 :            :   /**
     148                 :            :    * Whether or not the SolverEngine is fully initialized (post-construction).
     149                 :            :    * This post-construction initialization is automatically triggered by the
     150                 :            :    * use of the SolverEngine which calls the finishInit method above; e.g. when
     151                 :            :    * the first formula is asserted, a call to simplify() is issued, a scope is
     152                 :            :    * pushed, etc.
     153                 :            :    */
     154                 :            :   bool d_fullyInited;
     155                 :            : 
     156                 :            :   /**
     157                 :            :    * Whether or not a notifyCheckSat call has been made, which corresponds to
     158                 :            :    * when a checkSatisfiability() has already been
     159                 :            :    * made through the SolverEngine.  If true, and incrementalSolving is false,
     160                 :            :    * then attempting an additional checks for satisfiability will fail with
     161                 :            :    * a ModalException during notifyCheckSat.
     162                 :            :    */
     163                 :            :   bool d_queryMade;
     164                 :            :   /**
     165                 :            :    * Most recent result of last checkSatisfiability in the
     166                 :            :    * SolverEngine.
     167                 :            :    */
     168                 :            :   Result d_status;
     169                 :            : 
     170                 :            :   /**
     171                 :            :    * The expected status of the next satisfiability check.
     172                 :            :    */
     173                 :            :   Result d_expectedStatus;
     174                 :            : 
     175                 :            :   /** The SMT mode, for details see enumeration above. */
     176                 :            :   SmtMode d_smtMode;
     177                 :            : };
     178                 :            : 
     179                 :            : }  // namespace smt
     180                 :            : }  // namespace cvc5::internal
     181                 :            : 
     182                 :            : #endif