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): taking, mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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 #include "decision/relevancy.h"
  20
  21 #include "expr/node.h"
  22 #include "decision/options.h"
  23 #include "decision/decision_mode.h"
  24
  25 #include "smt/options.h"
  26
  27 using namespace std;
  28
  29 namespace CVC4 {
  30
  31 DecisionEngine::DecisionEngine(context::Context *sc,
  32                                  context::Context *uc) :
  33   d_enabledStrategies(),
  34   d_needIteSkolemMap(),
  35   d_relevancyStrategy(NULL),
  36   d_assertions(),
  37   d_cnfStream(NULL),
  38   d_satSolver(NULL),
  39   d_satContext(sc),
  40   d_userContext(uc),
  41   d_result(sc, SAT_VALUE_UNKNOWN),
  42   d_engineState(0)
  43 {
  44   Trace("decision") << "Creating decision engine" << std::endl;
  45 }
  46
  47 void DecisionEngine::init()
  48 {
  49   Assert(d_engineState == 0);
  50   d_engineState = 1;
  51
  52   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
  53   if(options::incrementalSolving()) {
  54     if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) {
  55       if(options::decisionMode.wasSetByUser()) {
  56         Warning() << "Ignorning decision option since using incremental mode (currently not supported together)"
  57                   << std::endl;
  58       } else {
  59         Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)"
  60                  << std::endl;
  61       }
  62     }
  63     return;
  64   }
  65   Trace("decision-init") << " * options->decisionMode: "
  66                          << options::decisionMode() << std:: endl;
  67   Trace("decision-init") << " * options->decisionStopOnly: "
  68                          << options::decisionStopOnly() << std::endl;
  69
  70   if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
  71   if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
  72     ITEDecisionStrategy* ds =
  73       new decision::JustificationHeuristic(this, d_satContext);
  74     enableStrategy(ds);
  75     d_needIteSkolemMap.push_back(ds);
  76   }
  77   if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) {
  78     RelevancyStrategy* ds =
  79       new decision::Relevancy(this, d_satContext);
  80     enableStrategy(ds);
  81     d_needIteSkolemMap.push_back(ds);
  82     d_relevancyStrategy = ds;
  83   }
  84 }
  85
  86
  87 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  88 {
  89   d_enabledStrategies.push_back(ds);
  90 }
  91
  92
  93 bool DecisionEngine::isRelevant(SatVariable var)
  94 {
  95   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  96   if(d_relevancyStrategy != NULL) {
  97     //Assert(d_cnfStream->hasNode(var));
  98     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  99   } else {
 100     return true;
 101   }
 102 }
 103
 104 SatValue DecisionEngine::getPolarity(SatVariable var)
 105 {
 106   Debug("decision") << "getPolariry(" << var <<")" << std::endl;
 107   if(d_relevancyStrategy != NULL) {
 108     Assert(isRelevant(var));
 109     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
 110   } else {
 111     return SAT_VALUE_UNKNOWN;
 112   }
 113 }
 114
 115
 116
 117
 118
 119
 120
 121
 122 void DecisionEngine::addAssertions(const vector<Node> &assertions)
 123 {
 124   Assert(false);  // doing this so that we revisit what to do
 125                   // here. Currently not being used.
 126
 127   // d_result = SAT_VALUE_UNKNOWN;
 128   // d_assertions.reserve(assertions.size());
 129   // for(unsigned i = 0; i < assertions.size(); ++i)
 130   //   d_assertions.push_back(assertions[i]);
 131 }
 132
 133 void DecisionEngine::addAssertions(const vector<Node> &assertions,
 134                                    unsigned assertionsEnd,
 135                                    IteSkolemMap iteSkolemMap)
 136 {
 137   // new assertions, reset whatever result we knew
 138   d_result = SAT_VALUE_UNKNOWN;
 139
 140   d_assertions.reserve(assertions.size());
 141   for(unsigned i = 0; i < assertions.size(); ++i)
 142     d_assertions.push_back(assertions[i]);
 143
 144   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 145     d_needIteSkolemMap[i]->
 146       addAssertions(assertions, assertionsEnd, iteSkolemMap);
 147 }
 148
 149 // void DecisionEngine::addAssertion(Node n)
 150 // {
 151 //   d_result = SAT_VALUE_UNKNOWN;
 152 //   if(needIteSkolemMap()) {
 153 //     d_assertions.push_back(n);
 154 //   }
 155 //   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 156 //     d_needIteSkolemMap[i]->notifyAssertionsAvailable();
 157 // }
 158
 159
 160 }/* CVC4 namespace */