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 "smt/smt_driver.h"
      14                 :            : 
      15                 :            : #include "options/base_options.h"
      16                 :            : #include "options/main_options.h"
      17                 :            : #include "options/smt_options.h"
      18                 :            : #include "prop/prop_engine.h"
      19                 :            : #include "smt/context_manager.h"
      20                 :            : #include "smt/env.h"
      21                 :            : #include "smt/logic_exception.h"
      22                 :            : #include "smt/smt_solver.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace smt {
      26                 :            : 
      27                 :      52215 : SmtDriver::SmtDriver(Env& env, SmtSolver& smt, ContextManager* ctx)
      28                 :      52215 :     : EnvObj(env), d_smt(smt), d_ctx(ctx), d_ap(env), d_illegalChecker(env)
      29                 :            : {
      30                 :            :   // set up proofs, this is done after options are finalized, so the
      31                 :            :   // preprocess proof has been setup
      32                 :            :   PreprocessProofGenerator* pppg =
      33                 :      52215 :       d_smt.getPreprocessor()->getPreprocessProofGenerator();
      34         [ +  + ]:      52215 :   if (pppg != nullptr)
      35                 :            :   {
      36                 :      19812 :     d_ap.enableProofs(pppg);
      37                 :            :   }
      38                 :      52215 : }
      39                 :            : 
      40                 :      50528 : Result SmtDriver::checkSat(const std::vector<Node>& assumptions)
      41                 :            : {
      42                 :      50528 :   bool hasAssumptions = !assumptions.empty();
      43         [ +  + ]:      50528 :   if (d_ctx)
      44                 :            :   {
      45                 :      49764 :     d_ctx->notifyCheckSat(hasAssumptions);
      46                 :            :   }
      47                 :      50528 :   Assertions& as = d_smt.getAssertions();
      48                 :      50528 :   Result result;
      49                 :            :   try
      50                 :            :   {
      51                 :            :     // then, initialize the assertions
      52                 :      50528 :     as.setAssumptions(assumptions);
      53                 :            : 
      54                 :            :     // the assertions are now finalized, we call the illegal checker to
      55                 :            :     // verify that any new assertions are legal
      56                 :      50528 :     d_illegalChecker.checkAssertions(as);
      57                 :            : 
      58                 :            :     // make the check, where notice smt engine should be fully inited by now
      59                 :            : 
      60         [ +  - ]:      50524 :     Trace("smt") << "SmtSolver::check()" << std::endl;
      61                 :            : 
      62                 :      50524 :     ResourceManager* rm = d_env.getResourceManager();
      63                 :            :     // if we are already out of (cumulative) resources
      64         [ -  + ]:      50524 :     if (rm->out())
      65                 :            :     {
      66                 :          0 :       UnknownExplanation why = rm->outOfResources()
      67         [ -  - ]:          0 :                                    ? UnknownExplanation::RESOURCEOUT
      68                 :          0 :                                    : UnknownExplanation::TIMEOUT;
      69                 :          0 :       result = Result(Result::UNKNOWN, why);
      70                 :            :     }
      71                 :            :     else
      72                 :            :     {
      73                 :      50524 :       bool checkAgain = true;
      74         [ +  + ]:      50480 :       do
      75                 :            :       {
      76                 :            :         // get the next assertions, store in d_ap
      77                 :      50531 :         getNextAssertionsInternal(d_ap);
      78                 :            :         // check sat based on the driver strategy
      79                 :      50531 :         result = checkSatNext(d_ap);
      80                 :            :         // if we were asked to check again
      81                 :      50480 :         if (result.getStatus() == Result::UNKNOWN
      82 [ +  + ][ +  + ]:      50480 :             && result.getUnknownExplanation()
                 [ +  + ]
      83                 :            :                    == UnknownExplanation::REQUIRES_CHECK_AGAIN)
      84                 :            :         {
      85                 :            :           // finish init to construct new theory/prop engine
      86                 :          7 :           d_smt.finishInit();
      87                 :            :         }
      88                 :            :         else
      89                 :            :         {
      90                 :      50473 :           checkAgain = false;
      91                 :            :         }
      92                 :            :       } while (checkAgain);
      93                 :            :     }
      94                 :            :   }
      95    [ -  + ][ + ]:         55 :   catch (const LogicException& e)
      96                 :            :   {
      97                 :            :     // The exception may have been throw during solving, backtrack to reset the
      98                 :            :     // decision level to the level expected after this method finishes
      99                 :         50 :     d_smt.getPropEngine()->resetTrail();
     100                 :         50 :     throw;
     101                 :         50 :   }
     102                 :          5 :   catch (const TypeCheckingExceptionPrivate& e)
     103                 :            :   {
     104                 :            :     // The exception has been throw during solving, backtrack to reset the
     105                 :            :     // decision level to the level expected after this method finishes. Note
     106                 :            :     // that we do not expect type checking exceptions to occur during solving.
     107                 :            :     // However, if they occur due to a bug, we don't want to additionally cause
     108                 :            :     // an assertion failure.
     109                 :          5 :     d_smt.getPropEngine()->resetTrail();
     110                 :          5 :     throw;
     111                 :          5 :   }
     112         [ +  + ]:      50473 :   if (d_ctx)
     113                 :            :   {
     114                 :      49713 :     d_ctx->notifyCheckSatResult(hasAssumptions);
     115                 :            :   }
     116                 :      50473 :   return result;
     117                 :         55 : }
     118                 :            : 
     119                 :      65662 : void SmtDriver::getNextAssertionsInternal(preprocessing::AssertionPipeline& ap)
     120                 :            : {
     121                 :      65662 :   ap.clear();
     122                 :            :   // must first refresh the assertions, in the case global declarations is true
     123                 :      65662 :   d_smt.getAssertions().refresh();
     124                 :            :   // get the next assertions based on the implementation of this driver
     125                 :      65662 :   getNextAssertions(ap);
     126                 :      65662 : }
     127                 :            : 
     128                 :      15131 : void SmtDriver::refreshAssertions()
     129                 :            : {
     130                 :            :   // get the next assertions, store in d_ap
     131                 :      15131 :   getNextAssertionsInternal(d_ap);
     132                 :            :   // preprocess
     133                 :      15131 :   d_smt.preprocess(d_ap);
     134                 :            :   // assert to internal
     135                 :      15131 :   d_smt.assertToInternal(d_ap);
     136                 :      15129 : }
     137                 :            : 
     138                 :       8224 : void SmtDriver::notifyPushPre()
     139                 :            : {
     140                 :            :   // must preprocess the assertions and push them to the SAT solver, to make
     141                 :            :   // the state accurate prior to pushing
     142                 :       8224 :   refreshAssertions();
     143                 :       8224 : }
     144                 :            : 
     145                 :       8224 : void SmtDriver::notifyPushPost() { d_smt.pushPropContext(); }
     146                 :            : 
     147                 :       8217 : void SmtDriver::notifyPopPre() { d_smt.popPropContext(); }
     148                 :            : 
     149                 :      49590 : void SmtDriver::notifyPostSolve() { d_smt.resetTrail(); }
     150                 :            : 
     151                 :      52207 : SmtDriverSingleCall::SmtDriverSingleCall(Env& env,
     152                 :            :                                          SmtSolver& smt,
     153                 :      52207 :                                          ContextManager* ctx)
     154                 :      52207 :     : SmtDriver(env, smt, ctx), d_assertionListIndex(userContext(), 0)
     155                 :            : {
     156                 :      52207 : }
     157                 :            : 
     158                 :      50516 : Result SmtDriverSingleCall::checkSatNext(preprocessing::AssertionPipeline& ap)
     159                 :            : {
     160                 :            :   // preprocess
     161                 :      50516 :   d_smt.preprocess(ap);
     162                 :            : 
     163         [ +  + ]:      50495 :   if (options().base.preprocessOnly)
     164                 :            :   {
     165                 :         10 :     return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK);
     166                 :            :   }
     167                 :            : 
     168                 :            :   // assert to internal
     169                 :      50485 :   d_smt.assertToInternal(ap);
     170                 :            :   // get result
     171                 :      50471 :   Result result = d_smt.checkSatInternal();
     172                 :            :   // handle preprocessing-specific modifications to result
     173         [ +  + ]:      50455 :   if (ap.isNegated())
     174                 :            :   {
     175         [ +  - ]:          2 :     Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
     176         [ +  - ]:          2 :     if (result.getStatus() == Result::UNSAT)
     177                 :            :     {
     178                 :          2 :       result = Result(Result::SAT);
     179                 :            :     }
     180         [ -  - ]:          0 :     else if (result.getStatus() == Result::SAT)
     181                 :            :     {
     182                 :            :       // Only can answer unsat if the theory is satisfaction complete. In
     183                 :            :       // other words, a "sat" result for a closed formula indicates that the
     184                 :            :       // formula is true in *all* models.
     185                 :            :       // This includes linear arithmetic and bitvectors, which are the primary
     186                 :            :       // targets for the global negate option. Other logics are possible
     187                 :            :       // here but not considered.
     188                 :          0 :       LogicInfo logic = logicInfo();
     189         [ -  - ]:          0 :       if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear())
     190                 :          0 :           || logic.isPure(theory::THEORY_BV))
     191                 :            :       {
     192                 :          0 :         result = Result(Result::UNSAT);
     193                 :            :       }
     194                 :            :       else
     195                 :            :       {
     196                 :          0 :         result = Result(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
     197                 :            :       }
     198                 :          0 :     }
     199         [ +  - ]:          2 :     Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
     200                 :            :   }
     201                 :      50455 :   return result;
     202                 :      50455 : }
     203                 :            : 
     204                 :      65647 : void SmtDriverSingleCall::getNextAssertions(
     205                 :            :     preprocessing::AssertionPipeline& ap)
     206                 :            : {
     207                 :      65647 :   Assertions& as = d_smt.getAssertions();
     208                 :      65647 :   const context::CDList<Node>& al = as.getAssertionList();
     209                 :      65647 :   size_t alsize = al.size();
     210         [ +  + ]:     261864 :   for (size_t i = d_assertionListIndex.get(); i < alsize; ++i)
     211                 :            :   {
     212                 :     196217 :     ap.push_back(al[i], true);
     213                 :            :   }
     214                 :      65647 :   d_assertionListIndex = alsize;
     215                 :      65647 : }
     216                 :            : 
     217                 :            : }  // namespace smt
     218                 :            : }  // namespace cvc5::internal