Branch data     Line data    Source code

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