Branch data     Line data    Source code

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