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                 :            :  * Decision engine.
      11                 :            :  */
      12                 :            : #include "decision/decision_engine.h"
      13                 :            : 
      14                 :            : #include "util/resource_manager.h"
      15                 :            : 
      16                 :            : namespace cvc5::internal {
      17                 :            : namespace decision {
      18                 :            : 
      19                 :      55853 : DecisionEngine::DecisionEngine(Env& env,
      20                 :            :                                prop::CDCLTSatSolver* ss,
      21                 :      55853 :                                prop::CnfStream* cs)
      22                 :      55853 :     : EnvObj(env), d_satSolver(ss), d_cnfStream(cs)
      23                 :            : {
      24                 :      55853 : }
      25                 :            : 
      26                 :    7064089 : prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
      27                 :            : {
      28                 :    7064089 :   resourceManager()->spendResource(Resource::DecisionStep);
      29                 :    7064089 :   return getNextInternal(stopSearch);
      30                 :            : }
      31                 :            : 
      32                 :      10322 : DecisionEngineEmpty::DecisionEngineEmpty(Env& env)
      33                 :      10322 :     : DecisionEngine(env, nullptr, nullptr)
      34                 :            : {
      35                 :      10322 : }
      36                 :      34565 : bool DecisionEngineEmpty::isDone() { return false; }
      37                 :     457834 : void DecisionEngineEmpty::addAssertions(
      38                 :            :     CVC5_UNUSED const std::vector<TNode>& lems)
      39                 :            : {
      40                 :     457834 : }
      41                 :    3791202 : prop::SatLiteral DecisionEngineEmpty::getNextInternal(
      42                 :            :     CVC5_UNUSED bool& stopSearch)
      43                 :            : {
      44                 :    3791202 :   return prop::undefSatLiteral;
      45                 :            : }
      46                 :            : 
      47                 :            : }  // namespace decision
      48                 :            : }  // namespace cvc5::internal