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, context::UserContext* uc)
  29     : d_enabledITEStrategies(),
  30       d_needIteSkolemMap(),
  31       d_relevancyStrategy(NULL),
  32       d_assertions(uc),
  33       d_cnfStream(NULL),
  34       d_satSolver(NULL),
  35       d_satContext(sc),
  36       d_userContext(uc),
  37       d_result(sc, SAT_VALUE_UNKNOWN),
  38       d_engineState(0)
  39 {
  40   Trace("decision") << "Creating decision engine" << std::endl;
  41 }
  42
  43 void DecisionEngine::init()
  44 {
  45   Assert(d_engineState == 0);
  46   d_engineState = 1;
  47
  48   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
  49   Trace("decision-init") << " * options->decisionMode: "
  50                          << options::decisionMode() << std:: endl;
  51   Trace("decision-init") << " * options->decisionStopOnly: "
  52                          << options::decisionStopOnly() << std::endl;
  53
  54   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
  55   {
  56     d_enabledITEStrategies.emplace_back(new decision::JustificationHeuristic(
  57         this, d_userContext, d_satContext));
  58     d_needIteSkolemMap.push_back(d_enabledITEStrategies.back().get());
  59   }
  60 }
  61
  62 void DecisionEngine::shutdown()
  63 {
  64   Trace("decision") << "Shutting down decision engine" << std::endl;
  65
  66   Assert(d_engineState == 1);
  67   d_engineState = 2;
  68
  69   d_enabledITEStrategies.clear();
  70   d_needIteSkolemMap.clear();
  71 }
  72
  73 bool DecisionEngine::isRelevant(SatVariable var)
  74 {
  75   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  76   if(d_relevancyStrategy != NULL) {
  77     //Assert(d_cnfStream->hasNode(var));
  78     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  79   } else {
  80     return true;
  81   }
  82 }
  83
  84 SatValue DecisionEngine::getPolarity(SatVariable var)
  85 {
  86   Debug("decision") << "getPolarity(" << var <<")" << std::endl;
  87   if(d_relevancyStrategy != NULL) {
  88     Assert(isRelevant(var));
  89     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
  90   } else {
  91     return SAT_VALUE_UNKNOWN;
  92   }
  93 }
  94
  95 void DecisionEngine::addAssertions(
  96     const preprocessing::AssertionPipeline& assertions)
  97 {
  98   // new assertions, reset whatever result we knew
  99   d_result = SAT_VALUE_UNKNOWN;
 100
 101   for (const Node& assertion : assertions)
 102   {
 103     d_assertions.push_back(assertion);
 104   }
 105
 106   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 107   {
 108     d_needIteSkolemMap[i]->addAssertions(assertions);
 109   }
 110 }
 111
 112 }/* CVC4 namespace */