src/decision/decision_engine.cpp

   1 /*********************                                                        */
   2 /*! \file decision_engine.cpp
   3  ** \verbatim
   4  ** Original author: kshitij
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2012  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Decision engine
  15  **
  16  ** Decision engine
  17  **/
  18
  19 #include "decision/decision_engine.h"
  20 #include "decision/justification_heuristic.h"
  21 #include "decision/relevancy.h"
  22
  23 #include "expr/node.h"
  24 #include "util/options.h"
  25
  26 using namespace std;
  27
  28 namespace CVC4 {
  29
  30   DecisionEngine::DecisionEngine(context::Context *sc,
  31                                  context::Context *uc) :
  32   d_enabledStrategies(),
  33   d_needIteSkolemMap(),
  34   d_relevancyStrategy(NULL),
  35   d_assertions(),
  36   d_cnfStream(NULL),
  37   d_satSolver(NULL),
  38   d_satContext(sc),
  39   d_userContext(uc),
  40   d_result(SAT_VALUE_UNKNOWN)
  41 {
  42   const Options* options = Options::current();
  43   Trace("decision") << "Creating decision engine" << std::endl;
  44
  45   if(options->incrementalSolving) return;
  46
  47   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
  48   if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
  49     ITEDecisionStrategy* ds =
  50       new decision::JustificationHeuristic(this, d_satContext);
  51     enableStrategy(ds);
  52     d_needIteSkolemMap.push_back(ds);
  53   }
  54   if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) {
  55     RelevancyStrategy* ds =
  56       new decision::Relevancy(this, d_satContext, options->decisionOptions);
  57     enableStrategy(ds);
  58     d_needIteSkolemMap.push_back(ds);
  59     d_relevancyStrategy = ds;
  60   }
  61 }
  62
  63 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  64 {
  65   d_enabledStrategies.push_back(ds);
  66 }
  67
  68
  69 bool DecisionEngine::isRelevant(SatVariable var)
  70 {
  71   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  72   if(d_relevancyStrategy != NULL) {
  73     //Assert(d_cnfStream->hasNode(var));
  74     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  75   } else {
  76     return true;
  77   }
  78 }
  79
  80 SatValue DecisionEngine::getPolarity(SatVariable var)
  81 {
  82   Debug("decision") << "getPolariry(" << var <<")" << std::endl;
  83   if(d_relevancyStrategy != NULL) {
  84     Assert(isRelevant(var));
  85     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
  86   } else {
  87     return SAT_VALUE_UNKNOWN;
  88   }
  89 }
  90
  91
  92
  93
  94
  95
  96
  97
  98 void DecisionEngine::addAssertions(const vector<Node> &assertions)
  99 {
 100   Assert(false);  // doing this so that we revisit what to do
 101                   // here. Currently not being used.
 102
 103   // d_result = SAT_VALUE_UNKNOWN;
 104   // d_assertions.reserve(assertions.size());
 105   // for(unsigned i = 0; i < assertions.size(); ++i)
 106   //   d_assertions.push_back(assertions[i]);
 107 }
 108
 109 void DecisionEngine::addAssertions(const vector<Node> &assertions,
 110                                    unsigned assertionsEnd,
 111                                    IteSkolemMap iteSkolemMap)
 112 {
 113   // new assertions, reset whatever result we knew
 114   d_result = SAT_VALUE_UNKNOWN;
 115
 116   d_assertions.reserve(assertions.size());
 117   for(unsigned i = 0; i < assertions.size(); ++i)
 118     d_assertions.push_back(assertions[i]);
 119
 120   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 121     d_needIteSkolemMap[i]->
 122       addAssertions(assertions, assertionsEnd, iteSkolemMap);
 123 }
 124
 125 // void DecisionEngine::addAssertion(Node n)
 126 // {
 127 //   d_result = SAT_VALUE_UNKNOWN;
 128 //   if(needIteSkolemMap()) {
 129 //     d_assertions.push_back(n);
 130 //   }
 131 //   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 132 //     d_needIteSkolemMap[i]->notifyAssertionsAvailable();
 133 // }
 134
 135
 136 }/* CVC4 namespace */