src/decision/decision_engine.h

   1 /*********************                                                        */
   2 /*! \file decision_engine.h
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, Tim King
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 "cvc4_private.h"
  18
  19 #ifndef __CVC4__DECISION__DECISION_ENGINE_H
  20 #define __CVC4__DECISION__DECISION_ENGINE_H
  21
  22 #include <vector>
  23
  24 #include "decision/decision_strategy.h"
  25
  26 #include "expr/node.h"
  27 #include "prop/cnf_stream.h"
  28 #include "prop/prop_engine.h"
  29 #include "prop/sat_solver_types.h"
  30 #include "theory/decision_attributes.h"
  31 #include "util/ite_removal.h"
  32 #include "util/output.h"
  33
  34 using namespace std;
  35 using namespace CVC4::prop;
  36 using namespace CVC4::decision;
  37
  38 namespace CVC4 {
  39
  40 class DecisionEngine {
  41
  42   vector <DecisionStrategy* > d_enabledStrategies;
  43   vector <ITEDecisionStrategy* > d_needIteSkolemMap;
  44   RelevancyStrategy* d_relevancyStrategy;
  45
  46   typedef context::CDList<Node> AssertionsList;
  47   AssertionsList d_assertions;
  48
  49   // PropEngine* d_propEngine;
  50   CnfStream* d_cnfStream;
  51   DPLLSatSolverInterface* d_satSolver;
  52
  53   context::Context* d_satContext;
  54   context::UserContext* d_userContext;
  55
  56   // Does decision engine know the answer?
  57   context::CDO<SatValue> d_result;
  58
  59   // Disable creating decision engine without required parameters
  60   DecisionEngine();
  61
  62   // init/shutdown state
  63   unsigned d_engineState;    // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
  64 public:
  65   // Necessary functions
  66
  67   /** Constructor */
  68   DecisionEngine(context::Context *sc, context::UserContext *uc);
  69
  70   /** Destructor, currently does nothing */
  71   ~DecisionEngine() {
  72     Trace("decision") << "Destroying decision engine" << std::endl;
  73   }
  74
  75   // void setPropEngine(PropEngine* pe) {
  76   //   // setPropEngine should not be called more than once
  77   //   Assert(d_propEngine == NULL);
  78   //   Assert(pe != NULL);
  79   //   d_propEngine = pe;
  80   // }
  81
  82   void setSatSolver(DPLLSatSolverInterface* ss) {
  83     // setPropEngine should not be called more than once
  84     Assert(d_satSolver == NULL);
  85     Assert(ss != NULL);
  86     d_satSolver = ss;
  87   }
  88
  89   void setCnfStream(CnfStream* cs) {
  90     // setPropEngine should not be called more than once
  91     Assert(d_cnfStream == NULL);
  92     Assert(cs != NULL);
  93     d_cnfStream = cs;
  94   }
  95
  96   /* enables decision stragies based on options */
  97   void init();
  98
  99   /* clears all of the strategies */
 100   void clearStrategies();
 101
 102
 103   /**
 104    * This is called by SmtEngine, at shutdown time, just before
 105    * destruction.  It is important because there are destruction
 106    * ordering issues between some parts of the system.
 107    */
 108   void shutdown() {
 109     Assert(d_engineState == 1);
 110     d_engineState = 2;
 111
 112     Trace("decision") << "Shutting down decision engine" << std::endl;
 113     clearStrategies();
 114   }
 115
 116   // Interface for External World to use our services
 117
 118   /** Gets the next decision based on strategies that are enabled */
 119   SatLiteral getNext(bool &stopSearch) {
 120     Assert(d_cnfStream != NULL,
 121            "Forgot to set cnfStream for decision engine?");
 122     Assert(d_satSolver != NULL,
 123            "Forgot to set satSolver for decision engine?");
 124
 125     SatLiteral ret = undefSatLiteral;
 126     for(unsigned i = 0;
 127         i < d_enabledStrategies.size()
 128           and ret == undefSatLiteral
 129           and stopSearch == false; ++i) {
 130       ret = d_enabledStrategies[i]->getNext(stopSearch);
 131     }
 132     return ret;
 133   }
 134
 135   /** Is a sat variable relevant */
 136   bool isRelevant(SatVariable var);
 137
 138   /**
 139    * Try to get tell SAT solver what polarity to try for a
 140    * decision. Return SAT_VALUE_UNKNOWN if it can't help
 141    */
 142   SatValue getPolarity(SatVariable var);
 143
 144   /** Is the DecisionEngine in a state where it has solved everything? */
 145   bool isDone() {
 146     Trace("decision") << "DecisionEngine::isDone() returning "
 147                       << (d_result != SAT_VALUE_UNKNOWN)
 148                       << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false")
 149                       << std::endl;
 150     return (d_result != SAT_VALUE_UNKNOWN);
 151   }
 152
 153   /** */
 154   Result getResult() {
 155     switch(d_result.get()) {
 156     case SAT_VALUE_TRUE: return Result(Result::SAT);
 157     case SAT_VALUE_FALSE: return Result(Result::UNSAT);
 158     case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
 159     default: Assert(false, "d_result is garbage");
 160     }
 161     return Result();
 162   }
 163
 164   /** */
 165   void setResult(SatValue val) {
 166     d_result = val;
 167   }
 168
 169   // External World helping us help the Strategies
 170
 171   /** If one of the enabled strategies needs them  */
 172   /* bool needIteSkolemMap() { */
 173   /*   return d_needIteSkolemMap.size() > 0; */
 174   /* } */
 175
 176   /* add a set of assertions */
 177   void addAssertions(const vector<Node> &assertions);
 178
 179   /**
 180    * add a set of assertions, while providing a mapping between skolem
 181    * variables and corresponding assertions. It is assumed that all
 182    * assertions after assertionEnd were generated by ite
 183    * removal. Hence, iteSkolemMap maps into only these.
 184    */
 185   void addAssertions(const vector<Node> &assertions,
 186                      unsigned assertionsEnd,
 187                      IteSkolemMap iteSkolemMap);
 188
 189   /* add a single assertion */
 190   void addAssertion(Node n);
 191
 192   // Interface for Strategies to use stuff stored in Decision Engine
 193   // (which was possibly requested by them on initialization)
 194
 195   /**
 196    * Get the assertions. Strategies are notified when these are available.
 197    */
 198   AssertionsList& getAssertions() {
 199     return d_assertions;
 200   }
 201
 202
 203   // Interface for Strategies to get information about External World
 204
 205   bool hasSatLiteral(TNode n) {
 206     return d_cnfStream->hasLiteral(n);
 207   }
 208   SatLiteral getSatLiteral(TNode n) {
 209     return d_cnfStream->getLiteral(n);
 210   }
 211   SatValue getSatValue(SatLiteral l) {
 212     return d_satSolver->value(l);
 213   }
 214   SatValue getSatValue(TNode n) {
 215     return getSatValue(getSatLiteral(n));
 216   }
 217   Node getNode(SatLiteral l) {
 218     return d_cnfStream->getNode(l);
 219   }
 220
 221 private:
 222   /**
 223    * Enable a particular decision strategy, also updating
 224    * corresponding vector<DecisionStrategy*>-s is the engine
 225    */
 226   void enableStrategy(DecisionStrategy* ds);
 227
 228 };/* DecisionEngine class */
 229
 230 }/* CVC4 namespace */
 231
 232 #endif /* __CVC4__DECISION__DECISION_ENGINE_H */