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
  22 #include "expr/node.h"
  23 #include "util/options.h"
  24
  25 using namespace std;
  26
  27 namespace CVC4 {
  28
  29 DecisionEngine::DecisionEngine() :
  30   d_needSimplifiedPreITEAssertions(),
  31   d_cnfStream(NULL),
  32   d_satSolver(NULL)
  33 {
  34   const Options* options = Options::current();
  35   Trace("decision") << "Creating decision engine" << std::endl;
  36   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
  37   if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
  38     DecisionStrategy* ds = new decision::JustificationHeuristic(this);
  39     enableStrategy(ds);
  40   }
  41 }
  42
  43 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  44 {
  45   d_enabledStrategies.push_back(ds);
  46   if( ds->needSimplifiedPreITEAssertions() )
  47     d_needSimplifiedPreITEAssertions.push_back(ds);
  48 }
  49
  50 void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
  51 {
  52   d_assertions.reserve(assertions.size());
  53   for(unsigned i = 0; i < assertions.size(); ++i)
  54     d_assertions.push_back(assertions[i]);
  55   for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
  56     d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
  57 }
  58
  59 }/* CVC4 namespace */