src/decision/decision_engine.cpp

   1 /*********************                                                        */
   2 /*! \file decision_engine.cpp
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Tim King, Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Decision engine
  13  **
  14  ** Decision engine
  15  **/
  16
  17 #include "decision/decision_engine.h"
  18 #include "decision/justification_heuristic.h"
  19
  20 #include "expr/node.h"
  21 #include "decision/options.h"
  22 #include "decision/decision_mode.h"
  23
  24 #include "smt/options.h"
  25
  26 using namespace std;
  27
  28 namespace CVC4 {
  29
  30 DecisionEngine::DecisionEngine(context::Context *sc,
  31                                context::UserContext *uc) :
  32   d_enabledStrategies(),
  33   d_needIteSkolemMap(),
  34   d_relevancyStrategy(NULL),
  35   d_assertions(uc),
  36   d_cnfStream(NULL),
  37   d_satSolver(NULL),
  38   d_satContext(sc),
  39   d_userContext(uc),
  40   d_result(sc, SAT_VALUE_UNKNOWN),
  41   d_engineState(0)
  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() == decision::DECISION_STRATEGY_INTERNAL) { }
  58   if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
  59     ITEDecisionStrategy* ds =
  60       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
  61     enableStrategy(ds);
  62     d_needIteSkolemMap.push_back(ds);
  63   }
  64 }
  65
  66
  67 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  68 {
  69   d_enabledStrategies.push_back(ds);
  70 }
  71
  72 void DecisionEngine::clearStrategies(){
  73   for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
  74     delete d_enabledStrategies[i];
  75   }
  76   d_enabledStrategies.clear();
  77   d_needIteSkolemMap.clear();
  78 }
  79
  80 bool DecisionEngine::isRelevant(SatVariable var)
  81 {
  82   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  83   if(d_relevancyStrategy != NULL) {
  84     //Assert(d_cnfStream->hasNode(var));
  85     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  86   } else {
  87     return true;
  88   }
  89 }
  90
  91 SatValue DecisionEngine::getPolarity(SatVariable var)
  92 {
  93   Debug("decision") << "getPolarity(" << var <<")" << std::endl;
  94   if(d_relevancyStrategy != NULL) {
  95     Assert(isRelevant(var));
  96     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
  97   } else {
  98     return SAT_VALUE_UNKNOWN;
  99   }
 100 }
 101
 102 void DecisionEngine::addAssertions(const vector<Node> &assertions)
 103 {
 104   Assert(false);  // doing this so that we revisit what to do
 105                   // here. Currently not being used.
 106
 107   // d_result = SAT_VALUE_UNKNOWN;
 108   // d_assertions.reserve(assertions.size());
 109   // for(unsigned i = 0; i < assertions.size(); ++i)
 110   //   d_assertions.push_back(assertions[i]);
 111 }
 112
 113 void DecisionEngine::addAssertions(const vector<Node> &assertions,
 114                                    unsigned assertionsEnd,
 115                                    IteSkolemMap iteSkolemMap)
 116 {
 117   // new assertions, reset whatever result we knew
 118   d_result = SAT_VALUE_UNKNOWN;
 119
 120   // d_assertions.reserve(assertions.size());
 121   for(unsigned i = 0; i < assertions.size(); ++i)
 122     d_assertions.push_back(assertions[i]);
 123
 124   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 125     d_needIteSkolemMap[i]->
 126       addAssertions(assertions, assertionsEnd, iteSkolemMap);
 127 }
 128
 129 }/* CVC4 namespace */