src/decision/decision_engine.cpp

   1 /*********************                                                        */
   2 /*! \file decision_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Kshitij Bansal, Tim King, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Decision engine
  13  **
  14  ** Decision engine
  15  **/
  16 #include "decision/decision_engine.h"
  17
  18 #include "decision/decision_attributes.h"
  19 #include "decision/justification_heuristic.h"
  20 #include "expr/node.h"
  21 #include "options/decision_options.h"
  22 #include "options/smt_options.h"
  23
  24 using namespace std;
  25
  26 namespace CVC4 {
  27
  28 DecisionEngine::DecisionEngine(context::Context* sc,
  29                                context::UserContext* uc,
  30                                ResourceManager* rm)
  31     : d_enabledITEStrategy(nullptr),
  32       d_needIteSkolemMap(),
  33       d_relevancyStrategy(nullptr),
  34       d_assertions(uc),
  35       d_cnfStream(nullptr),
  36       d_satSolver(nullptr),
  37       d_satContext(sc),
  38       d_userContext(uc),
  39       d_result(sc, SAT_VALUE_UNKNOWN),
  40       d_engineState(0),
  41       d_resourceManager(rm)
  42 {
  43   Trace("decision") << "Creating decision engine" << std::endl;
  44 }
  45
  46 void DecisionEngine::init()
  47 {
  48   Assert(d_engineState == 0);
  49   d_engineState = 1;
  50
  51   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
  52   Trace("decision-init") << " * options->decisionMode: "
  53                          << options::decisionMode() << std:: endl;
  54   Trace("decision-init") << " * options->decisionStopOnly: "
  55                          << options::decisionStopOnly() << std::endl;
  56
  57   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
  58   {
  59     d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
  60         this, d_userContext, d_satContext));
  61     d_needIteSkolemMap.push_back(d_enabledITEStrategy.get());
  62   }
  63 }
  64
  65 void DecisionEngine::shutdown()
  66 {
  67   Trace("decision") << "Shutting down decision engine" << std::endl;
  68
  69   Assert(d_engineState == 1);
  70   d_engineState = 2;
  71   d_enabledITEStrategy.reset(nullptr);
  72   d_needIteSkolemMap.clear();
  73 }
  74
  75 SatLiteral DecisionEngine::getNext(bool& stopSearch)
  76 {
  77   d_resourceManager->spendResource(ResourceManager::Resource::DecisionStep);
  78   Assert(d_cnfStream != nullptr)
  79       << "Forgot to set cnfStream for decision engine?";
  80   Assert(d_satSolver != nullptr)
  81       << "Forgot to set satSolver for decision engine?";
  82
  83   return d_enabledITEStrategy == nullptr
  84              ? undefSatLiteral
  85              : d_enabledITEStrategy->getNext(stopSearch);
  86 }
  87
  88 bool DecisionEngine::isRelevant(SatVariable var)
  89 {
  90   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  91   if (d_relevancyStrategy != nullptr)
  92   {
  93     //Assert(d_cnfStream->hasNode(var));
  94     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  95   }
  96   else
  97   {
  98     return true;
  99   }
 100 }
 101
 102 SatValue DecisionEngine::getPolarity(SatVariable var)
 103 {
 104   Debug("decision") << "getPolarity(" << var <<")" << std::endl;
 105   if (d_relevancyStrategy != nullptr)
 106   {
 107     Assert(isRelevant(var));
 108     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
 109   }
 110   else
 111   {
 112     return SAT_VALUE_UNKNOWN;
 113   }
 114 }
 115
 116 void DecisionEngine::addAssertions(
 117     const preprocessing::AssertionPipeline& assertions)
 118 {
 119   // new assertions, reset whatever result we knew
 120   d_result = SAT_VALUE_UNKNOWN;
 121
 122   for (const Node& assertion : assertions)
 123   {
 124     d_assertions.push_back(assertion);
 125   }
 126
 127   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 128   {
 129     d_needIteSkolemMap[i]->addAssertions(assertions);
 130   }
 131 }
 132
 133 }/* CVC4 namespace */