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(context::Context* sc,
  29                                      context::UserContext* uc,
  30                                      ResourceManager* rm)
  31     : DecisionEngine(sc, rm),
  32       d_result(sc, SAT_VALUE_UNKNOWN),
  33       d_engineState(0),
  34       d_enabledITEStrategy(nullptr),
  35       d_decisionStopOnly(options::decisionMode()
  36                          == options::DecisionMode::STOPONLY_OLD)
  37 {
  38   Trace("decision") << "Creating decision engine" << std::endl;
  39   Assert(d_engineState == 0);
  40   d_engineState = 1;
  41
  42   Trace("decision-init") << "DecisionEngineOld::init()" << std::endl;
  43   Trace("decision-init") << " * options->decisionMode: "
  44                          << options::decisionMode() << std::endl;
  45   Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly
  46                          << std::endl;
  47
  48   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
  49   {
  50     d_enabledITEStrategy.reset(
  51         new decision::JustificationHeuristic(this, uc, sc));
  52   }
  53 }
  54
  55 void DecisionEngineOld::shutdown()
  56 {
  57   Trace("decision") << "Shutting down decision engine" << std::endl;
  58
  59   Assert(d_engineState == 1);
  60   d_engineState = 2;
  61   d_enabledITEStrategy.reset(nullptr);
  62 }
  63
  64 SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch)
  65 {
  66   Assert(d_cnfStream != nullptr)
  67       << "Forgot to set cnfStream for decision engine?";
  68   Assert(d_satSolver != nullptr)
  69       << "Forgot to set satSolver for decision engine?";
  70
  71   SatLiteral ret = d_enabledITEStrategy == nullptr
  72                        ? undefSatLiteral
  73                        : d_enabledITEStrategy->getNext(stopSearch);
  74   // if we are doing stop only, we don't return the literal
  75   return d_decisionStopOnly ? undefSatLiteral : ret;
  76 }
  77
  78 void DecisionEngineOld::addAssertion(TNode assertion)
  79 {
  80   // new assertions, reset whatever result we knew
  81   d_result = SAT_VALUE_UNKNOWN;
  82   if (d_enabledITEStrategy != nullptr)
  83   {
  84     d_enabledITEStrategy->addAssertion(assertion);
  85   }
  86 }
  87
  88 void DecisionEngineOld::addSkolemDefinition(TNode lem, TNode skolem)
  89 {
  90   // new assertions, reset whatever result we knew
  91   d_result = SAT_VALUE_UNKNOWN;
  92   if (d_enabledITEStrategy != nullptr)
  93   {
  94     d_enabledITEStrategy->addSkolemDefinition(lem, skolem);
  95   }
  96 }
  97
  98 }  // namespace cvc5