src/decision/decision_engine.cpp

   1 /*********************                                                        */
   2 /*! \file decision_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Kshitij Bansal, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Decision engine
  13  **
  14  ** Decision engine
  15  **/
  16 #include "decision/decision_engine.h"
  17
  18 #include "decision/decision_attributes.h"
  19 #include "decision/justification_heuristic.h"
  20 #include "expr/node.h"
  21 #include "options/decision_mode.h"
  22 #include "options/decision_options.h"
  23 #include "options/smt_options.h"
  24
  25 using namespace std;
  26
  27 namespace CVC4 {
  28
  29 DecisionEngine::DecisionEngine(context::Context *sc,
  30                                context::UserContext *uc) :
  31   d_enabledStrategies(),
  32   d_needIteSkolemMap(),
  33   d_relevancyStrategy(NULL),
  34   d_assertions(uc),
  35   d_cnfStream(NULL),
  36   d_satSolver(NULL),
  37   d_satContext(sc),
  38   d_userContext(uc),
  39   d_result(sc, SAT_VALUE_UNKNOWN),
  40   d_engineState(0)
  41 {
  42   Trace("decision") << "Creating decision engine" << std::endl;
  43 }
  44
  45 void DecisionEngine::init()
  46 {
  47   Assert(d_engineState == 0);
  48   d_engineState = 1;
  49
  50   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
  51   Trace("decision-init") << " * options->decisionMode: "
  52                          << options::decisionMode() << std:: endl;
  53   Trace("decision-init") << " * options->decisionStopOnly: "
  54                          << options::decisionStopOnly() << std::endl;
  55
  56   if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
  57   if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
  58     ITEDecisionStrategy* ds =
  59       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
  60     enableStrategy(ds);
  61     d_needIteSkolemMap.push_back(ds);
  62   }
  63 }
  64
  65
  66 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  67 {
  68   d_enabledStrategies.push_back(ds);
  69 }
  70
  71 void DecisionEngine::clearStrategies(){
  72   for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
  73     delete d_enabledStrategies[i];
  74   }
  75   d_enabledStrategies.clear();
  76   d_needIteSkolemMap.clear();
  77 }
  78
  79 bool DecisionEngine::isRelevant(SatVariable var)
  80 {
  81   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  82   if(d_relevancyStrategy != NULL) {
  83     //Assert(d_cnfStream->hasNode(var));
  84     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  85   } else {
  86     return true;
  87   }
  88 }
  89
  90 SatValue DecisionEngine::getPolarity(SatVariable var)
  91 {
  92   Debug("decision") << "getPolarity(" << var <<")" << std::endl;
  93   if(d_relevancyStrategy != NULL) {
  94     Assert(isRelevant(var));
  95     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
  96   } else {
  97     return SAT_VALUE_UNKNOWN;
  98   }
  99 }
 100
 101 void DecisionEngine::addAssertions(const vector<Node> &assertions)
 102 {
 103   Assert(false);  // doing this so that we revisit what to do
 104                   // here. Currently not being used.
 105
 106   // d_result = SAT_VALUE_UNKNOWN;
 107   // d_assertions.reserve(assertions.size());
 108   // for(unsigned i = 0; i < assertions.size(); ++i)
 109   //   d_assertions.push_back(assertions[i]);
 110 }
 111
 112 void DecisionEngine::addAssertions(const vector<Node> &assertions,
 113                                    unsigned assertionsEnd,
 114                                    IteSkolemMap iteSkolemMap)
 115 {
 116   // new assertions, reset whatever result we knew
 117   d_result = SAT_VALUE_UNKNOWN;
 118
 119   // d_assertions.reserve(assertions.size());
 120   for(unsigned i = 0; i < assertions.size(); ++i)
 121     d_assertions.push_back(assertions[i]);
 122
 123   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 124     d_needIteSkolemMap[i]->
 125       addAssertions(assertions, assertionsEnd, iteSkolemMap);
 126 }
 127
 128 }/* CVC4 namespace */