src/decision/decision_engine.cpp

   1 /*********************                                                        */
   2 /*! \file decision_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Kshitij Bansal, Tim King, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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_options.h"
  22 #include "options/smt_options.h"
  23
  24 using namespace std;
  25
  26 namespace CVC4 {
  27
  28 DecisionEngine::DecisionEngine(context::Context *sc,
  29                                context::UserContext *uc) :
  30   d_enabledStrategies(),
  31   d_needIteSkolemMap(),
  32   d_relevancyStrategy(NULL),
  33   d_assertions(uc),
  34   d_cnfStream(NULL),
  35   d_satSolver(NULL),
  36   d_satContext(sc),
  37   d_userContext(uc),
  38   d_result(sc, SAT_VALUE_UNKNOWN),
  39   d_engineState(0)
  40 {
  41   Trace("decision") << "Creating decision engine" << std::endl;
  42 }
  43
  44 void DecisionEngine::init()
  45 {
  46   Assert(d_engineState == 0);
  47   d_engineState = 1;
  48
  49   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
  50   Trace("decision-init") << " * options->decisionMode: "
  51                          << options::decisionMode() << std:: endl;
  52   Trace("decision-init") << " * options->decisionStopOnly: "
  53                          << options::decisionStopOnly() << std::endl;
  54
  55   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
  56   {
  57     ITEDecisionStrategy* ds =
  58       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
  59     enableStrategy(ds);
  60     d_needIteSkolemMap.push_back(ds);
  61   }
  62 }
  63
  64
  65 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
  66 {
  67   d_enabledStrategies.push_back(ds);
  68 }
  69
  70 void DecisionEngine::clearStrategies(){
  71   for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
  72     delete d_enabledStrategies[i];
  73   }
  74   d_enabledStrategies.clear();
  75   d_needIteSkolemMap.clear();
  76 }
  77
  78 bool DecisionEngine::isRelevant(SatVariable var)
  79 {
  80   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
  81   if(d_relevancyStrategy != NULL) {
  82     //Assert(d_cnfStream->hasNode(var));
  83     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
  84   } else {
  85     return true;
  86   }
  87 }
  88
  89 SatValue DecisionEngine::getPolarity(SatVariable var)
  90 {
  91   Debug("decision") << "getPolarity(" << var <<")" << std::endl;
  92   if(d_relevancyStrategy != NULL) {
  93     Assert(isRelevant(var));
  94     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
  95   } else {
  96     return SAT_VALUE_UNKNOWN;
  97   }
  98 }
  99
 100 void DecisionEngine::addAssertions(
 101     const preprocessing::AssertionPipeline& assertions)
 102 {
 103   // new assertions, reset whatever result we knew
 104   d_result = SAT_VALUE_UNKNOWN;
 105
 106   for (const Node& assertion : assertions)
 107   {
 108     d_assertions.push_back(assertion);
 109   }
 110
 111   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
 112   {
 113     d_needIteSkolemMap[i]->addAssertions(assertions);
 114   }
 115 }
 116
 117 }/* CVC4 namespace */