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(context::Context *sc,
  30                                  context::Context *uc) :
  31   d_enabledStrategies(),
  32   d_needIteSkolemMap(),
  33   d_assertions(),
  34   d_cnfStream(NULL),
  35   d_satSolver(NULL),
  36   d_satContext(sc),
  37   d_userContext(uc),
  38   d_result(SAT_VALUE_UNKNOWN)
  39 {
  40   const Options* options = Options::current();
  41   Trace("decision") << "Creating decision engine" << std::endl;
  42
  43   if(options->incrementalSolving) return;
  44
  45   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
  46   if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
  47     ITEDecisionStrategy* ds =
  48       new decision::JustificationHeuristic(this, d_satContext);
  49     enableStrategy(ds);
  50     d_needIteSkolemMap.push_back(ds);
  51   }
  52 }
  53
  54 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  55 {
  56   d_enabledStrategies.push_back(ds);
  57 }
  58
  59
  60 void DecisionEngine::addAssertions(const vector<Node> &assertions)
  61 {
  62   Assert(false);  // doing this so that we revisit what to do
  63                   // here. Currently not being used.
  64
  65   // d_result = SAT_VALUE_UNKNOWN;
  66   // d_assertions.reserve(assertions.size());
  67   // for(unsigned i = 0; i < assertions.size(); ++i)
  68   //   d_assertions.push_back(assertions[i]);
  69 }
  70
  71 void DecisionEngine::addAssertions
  72   (const vector<Node> &assertions,
  73    unsigned assertionsEnd,
  74    IteSkolemMap iteSkolemMap)
  75 {
  76   // new assertions, reset whatever result we knew
  77   d_result = SAT_VALUE_UNKNOWN;
  78
  79   d_assertions.reserve(assertions.size());
  80   for(unsigned i = 0; i < assertions.size(); ++i)
  81     d_assertions.push_back(assertions[i]);
  82
  83   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
  84     d_needIteSkolemMap[i]->
  85       addAssertions(assertions, assertionsEnd, iteSkolemMap);
  86 }
  87
  88 // void DecisionEngine::addAssertion(Node n)
  89 // {
  90 //   d_result = SAT_VALUE_UNKNOWN;
  91 //   if(needIteSkolemMap()) {
  92 //     d_assertions.push_back(n);
  93 //   }
  94 //   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
  95 //     d_needIteSkolemMap[i]->notifyAssertionsAvailable();
  96 // }
  97
  98
  99 }/* CVC4 namespace */