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                 :            :  * The solver for SMT queries in an SolverEngine.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__SMT__SMT_DRIVER_H
      16                 :            : #define CVC5__SMT__SMT_DRIVER_H
      17                 :            : 
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #include "expr/node.h"
      21                 :            : #include "preprocessing/assertion_pipeline.h"
      22                 :            : #include "smt/assertions.h"
      23                 :            : #include "smt/env_obj.h"
      24                 :            : #include "smt/illegal_checker.h"
      25                 :            : #include "util/result.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace smt {
      29                 :            : 
      30                 :            : class SmtSolver;
      31                 :            : class ContextManager;
      32                 :            : 
      33                 :            : /**
      34                 :            :  * SMT driver class.
      35                 :            :  *
      36                 :            :  * The purpose of this class is to define algorithms for checking
      37                 :            :  * satisfiability beyond a single call to the underlying SMT solver. The
      38                 :            :  * default implementation, SmtDriverSingleCall, is used for invoking a
      39                 :            :  * single call to the SMT solver only.
      40                 :            :  */
      41                 :            : class SmtDriver : protected EnvObj
      42                 :            : {
      43                 :            :  public:
      44                 :            :   SmtDriver(Env& env, SmtSolver& smt, ContextManager* ctx);
      45                 :      51738 :   virtual ~SmtDriver() {}
      46                 :            :   /**
      47                 :            :    * Check satisfiability. This invokes the algorithm given by this driver
      48                 :            :    * for checking satisfiability.
      49                 :            :    *
      50                 :            :    * @param assumptions The assumptions for this check-sat call, which are
      51                 :            :    * temporary assertions.
      52                 :            :    */
      53                 :            :   Result checkSat(const std::vector<Node>& assumptions);
      54                 :            : 
      55                 :            :   /**
      56                 :            :    * Refresh the assertions that have been asserted to the underlying SMT
      57                 :            :    * solver. This gets the set of unprocessed assertions of the underlying
      58                 :            :    * SMT solver, preprocesses them, pushes them into the SMT solver.
      59                 :            :    *
      60                 :            :    * We ensure that assertions are refreshed eagerly during user pushes to
      61                 :            :    * ensure that assertions are only preprocessed in one context.
      62                 :            :    */
      63                 :            :   void refreshAssertions();
      64                 :            :   // --------------------------------------- callbacks from the context manager
      65                 :            :   /**
      66                 :            :    * Notify push pre, which is called just before the user context of the state
      67                 :            :    * pushes. This processes all pending assertions.
      68                 :            :    */
      69                 :            :   void notifyPushPre();
      70                 :            :   /**
      71                 :            :    * Notify push post, which is called just after the user context of the state
      72                 :            :    * pushes. This performs a push on the underlying prop engine.
      73                 :            :    */
      74                 :            :   void notifyPushPost();
      75                 :            :   /**
      76                 :            :    * Notify pop pre, which is called just before the user context of the state
      77                 :            :    * pops. This performs a pop on the underlying prop engine.
      78                 :            :    */
      79                 :            :   void notifyPopPre();
      80                 :            :   /**
      81                 :            :    * Notify post solve, which is called once per check-sat query. It is
      82                 :            :    * triggered when the first d_state.doPendingPops() is issued after the
      83                 :            :    * check-sat. This calls the postsolve method of the underlying TheoryEngine.
      84                 :            :    */
      85                 :            :   void notifyPostSolve();
      86                 :            :   // ----------------------------------- end callbacks from the context manager
      87                 :            :  protected:
      88                 :            :   /**
      89                 :            :    * Get the next assertions, store in ap. Refreshes the SMT solver's
      90                 :            :    * assertions and calls the driver-specific getNextAssertions method.
      91                 :            :    */
      92                 :            :   void getNextAssertionsInternal(preprocessing::AssertionPipeline& ap);
      93                 :            :   /**
      94                 :            :    * Check satisfiability next, return the result.
      95                 :            :    *
      96                 :            :    * If the result is unknown with UnknownExplanation REQUIRES_CHECK_AGAIN,
      97                 :            :    * then this driver will be called to getNextAssertions as described below
      98                 :            :    * and another call to checkSatNext will be made.
      99                 :            :    *
     100                 :            :    * Otherwise, the returned result is the final one returned by the
     101                 :            :    * checkSatisfiability method above.
     102                 :            :    */
     103                 :            :   virtual Result checkSatNext(preprocessing::AssertionPipeline& ap) = 0;
     104                 :            :   /**
     105                 :            :    * Get the next assertions. This is called:
     106                 :            :    * (1) immediately before calls to checkSatNext, where we populate ap with
     107                 :            :    * those that will be checked on the next call to checkSatNext.
     108                 :            :    * (2) in calls to refreshAssertions, where we populate ap with all
     109                 :            :    * assertions that require being pushed to the SAT solver.
     110                 :            :    */
     111                 :            :   virtual void getNextAssertions(preprocessing::AssertionPipeline& ap) = 0;
     112                 :            :   /** The underlying SMT solver */
     113                 :            :   SmtSolver& d_smt;
     114                 :            :   /**
     115                 :            :    * The underlying context manager. This is only required to be provided
     116                 :            :    * if the checkSatNext method ever sets checkAgain to true.
     117                 :            :    */
     118                 :            :   ContextManager* d_ctx;
     119                 :            :   /** assertions pipeline */
     120                 :            :   preprocessing::AssertionPipeline d_ap;
     121                 :            :   /**
     122                 :            :    * The utility used for checking for illegal inputs
     123                 :            :    */
     124                 :            :   IllegalChecker d_illegalChecker;
     125                 :            : };
     126                 :            : 
     127                 :            : /**
     128                 :            :  * The default SMT driver, which makes a single call to the underlying
     129                 :            :  * SMT solver.
     130                 :            :  *
     131                 :            :  * Notice this class does not require ContextManager if we are not doing
     132                 :            :  * incremental solving with this driver.
     133                 :            :  */
     134                 :            : class SmtDriverSingleCall : public SmtDriver
     135                 :            : {
     136                 :            :  public:
     137                 :            :   SmtDriverSingleCall(Env& env, SmtSolver& smt, ContextManager* ctx = nullptr);
     138                 :     102285 :   virtual ~SmtDriverSingleCall() {}
     139                 :            : 
     140                 :            :  protected:
     141                 :            :   /** Check sat next, takes result of underlying SMT solver only */
     142                 :            :   Result checkSatNext(preprocessing::AssertionPipeline& ap) override;
     143                 :            :   /** Gets all the assertions we have yet to process */
     144                 :            :   void getNextAssertions(preprocessing::AssertionPipeline& ap) override;
     145                 :            :   /**
     146                 :            :    * The first index in the assertion list of the underlying SMT solver that we
     147                 :            :    * have not processed yet. The call to getNextAssertions gets all assertions
     148                 :            :    * starting from this index onward.
     149                 :            :    */
     150                 :            :   context::CDO<size_t> d_assertionListIndex;
     151                 :            : };
     152                 :            : 
     153                 :            : }  // namespace smt
     154                 :            : }  // namespace cvc5::internal
     155                 :            : 
     156                 :            : #endif