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(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   const Options* options = Options::current();
  53   if(options->incrementalSolving) return;
  54
  55   Trace("decision-init") << " * options->decisionMode: "
  56                          << options->decisionMode << std:: endl;
  57   Trace("decision-init") << " * options->decisionOptions.stopOnly: "
  58                          << ((options->decisionOptions).stopOnly) << std::endl;
  59
  60   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
  61   if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
  62     ITEDecisionStrategy* ds =
  63       new decision::JustificationHeuristic(this, d_satContext);
  64     enableStrategy(ds);
  65     d_needIteSkolemMap.push_back(ds);
  66   }
  67   if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) {
  68     RelevancyStrategy* ds =
  69       new decision::Relevancy(this, d_satContext, options->decisionOptions);
  70     enableStrategy(ds);
  71     d_needIteSkolemMap.push_back(ds);
  72     d_relevancyStrategy = ds;
  73   }
  74 }
  75
  76
  77 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  78 {
  79   d_enabledStrategies.push_back(ds);
  80 }
  81
  82
  83 bool DecisionEngine::isRelevant(SatVariable var)
  84 {
  85   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  86   if(d_relevancyStrategy != NULL) {
  87     //Assert(d_cnfStream->hasNode(var));
  88     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  89   } else {
  90     return true;
  91   }
  92 }
  93
  94 SatValue DecisionEngine::getPolarity(SatVariable var)
  95 {
  96   Debug("decision") << "getPolariry(" << var <<")" << std::endl;
  97   if(d_relevancyStrategy != NULL) {
  98     Assert(isRelevant(var));
  99     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
 100   } else {
 101     return SAT_VALUE_UNKNOWN;
 102   }
 103 }
 104
 105
 106
 107
 108
 109
 110
 111
 112 void DecisionEngine::addAssertions(const vector<Node> &assertions)
 113 {
 114   Assert(false);  // doing this so that we revisit what to do
 115                   // here. Currently not being used.
 116
 117   // d_result = SAT_VALUE_UNKNOWN;
 118   // d_assertions.reserve(assertions.size());
 119   // for(unsigned i = 0; i < assertions.size(); ++i)
 120   //   d_assertions.push_back(assertions[i]);
 121 }
 122
 123 void DecisionEngine::addAssertions(const vector<Node> &assertions,
 124                                    unsigned assertionsEnd,
 125                                    IteSkolemMap iteSkolemMap)
 126 {
 127   // new assertions, reset whatever result we knew
 128   d_result = SAT_VALUE_UNKNOWN;
 129
 130   d_assertions.reserve(assertions.size());
 131   for(unsigned i = 0; i < assertions.size(); ++i)
 132     d_assertions.push_back(assertions[i]);
 133
 134   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 135     d_needIteSkolemMap[i]->
 136       addAssertions(assertions, assertionsEnd, iteSkolemMap);
 137 }
 138
 139 // void DecisionEngine::addAssertion(Node n)
 140 // {
 141 //   d_result = SAT_VALUE_UNKNOWN;
 142 //   if(needIteSkolemMap()) {
 143 //     d_assertions.push_back(n);
 144 //   }
 145 //   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 146 //     d_needIteSkolemMap[i]->notifyAssertionsAvailable();
 147 // }
 148
 149
 150 }/* CVC4 namespace */