src/decision/decision_engine_old.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Kshitij Bansal, Aina Niemetz, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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  * Old implementation of the decision engine
  14  */
  15 #include "decision/decision_engine_old.h"
  16
  17 #include "decision/decision_attributes.h"
  18 #include "decision/justification_heuristic.h"
  19 #include "expr/node.h"
  20 #include "options/decision_options.h"
  21 #include "options/smt_options.h"
  22 #include "util/resource_manager.h"
  23
  24 using namespace std;
  25
  26 namespace cvc5 {
  27
  28 DecisionEngineOld::DecisionEngineOld(Env& env)
  29     : DecisionEngine(env),
  30       d_result(context(), SAT_VALUE_UNKNOWN),
  31       d_engineState(0),
  32       d_enabledITEStrategy(nullptr),
  33       d_decisionStopOnly(options::decisionMode()
  34                          == options::DecisionMode::STOPONLY_OLD)
  35 {
  36   Trace("decision") << "Creating decision engine" << std::endl;
  37   Assert(d_engineState == 0);
  38   d_engineState = 1;
  39
  40   Trace("decision-init") << "DecisionEngineOld::init()" << std::endl;
  41   Trace("decision-init") << " * options->decisionMode: "
  42                          << options::decisionMode() << std::endl;
  43   Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly
  44                          << std::endl;
  45
  46   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
  47   {
  48     d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this));
  49   }
  50 }
  51
  52 void DecisionEngineOld::shutdown()
  53 {
  54   Trace("decision") << "Shutting down decision engine" << std::endl;
  55
  56   Assert(d_engineState == 1);
  57   d_engineState = 2;
  58   d_enabledITEStrategy.reset(nullptr);
  59 }
  60
  61 SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch)
  62 {
  63   Assert(d_cnfStream != nullptr)
  64       << "Forgot to set cnfStream for decision engine?";
  65   Assert(d_satSolver != nullptr)
  66       << "Forgot to set satSolver for decision engine?";
  67
  68   SatLiteral ret = d_enabledITEStrategy == nullptr
  69                        ? undefSatLiteral
  70                        : d_enabledITEStrategy->getNext(stopSearch);
  71   // if we are doing stop only, we don't return the literal
  72   return d_decisionStopOnly ? undefSatLiteral : ret;
  73 }
  74
  75 void DecisionEngineOld::addAssertion(TNode assertion, bool isLemma)
  76 {
  77   // new assertions, reset whatever result we knew
  78   d_result = SAT_VALUE_UNKNOWN;
  79   if (d_enabledITEStrategy != nullptr)
  80   {
  81     d_enabledITEStrategy->addAssertion(assertion);
  82   }
  83 }
  84
  85 void DecisionEngineOld::addSkolemDefinition(TNode lem,
  86                                             TNode skolem,
  87                                             bool isLemma)
  88 {
  89   // new assertions, reset whatever result we knew
  90   d_result = SAT_VALUE_UNKNOWN;
  91   if (d_enabledITEStrategy != nullptr)
  92   {
  93     d_enabledITEStrategy->addSkolemDefinition(lem, skolem);
  94   }
  95 }
  96
  97 }  // namespace cvc5