src/theory/decision_manager.h

   1 /*********************                                                        */
   2 /*! \file decision_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 manager, which manages all decision strategies owned by
  13  ** theory solvers within TheoryEngine.
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__THEORY__DECISION_MANAGER__H
  19 #define CVC4__THEORY__DECISION_MANAGER__H
  20
  21 #include <map>
  22 #include "context/cdlist.h"
  23 #include "theory/decision_strategy.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /** DecisionManager
  29  *
  30  * This class manages all "decision strategies" for theory solvers in
  31  * TheoryEngine. A decision strategy is a callback in the SAT solver for
  32  * imposing its next decision. This is useful, for instance, in
  33  * branch-and-bound algorithms where we require that the first decision
  34  * is a bound on some quantity. For instance, finite model finding may impose
  35  * a bound on the cardinality of an uninterpreted sort as the first decision.
  36  *
  37  * This class maintains a user-context-dependent set of pointers to
  38  * DecisionStrategy objects, which implement indivdual decision strategies.
  39  *
  40  * Decision strategies may be registered to this class via registerStrategy
  41  * at any time during solving. They are cleared via a call to reset during
  42  * TheoryEngine's postSolve method.
  43  *
  44  * Decision strategies have a fixed order, which is managed by the enumeration
  45  * type StrategyId, where strategies with smaller id have higher precedence
  46  * in our global decision strategy.
  47  */
  48 class DecisionManager
  49 {
  50   typedef context::CDList<DecisionStrategy*> DecisionStrategyList;
  51
  52  public:
  53   enum StrategyId
  54   {
  55     // The order of the global decision strategy used by the TheoryEngine
  56     // for getNextDecision.
  57
  58     //----- assume-feasibile strategies
  59     //  These are required to go first for the sake of model-soundness. In
  60     //  other words, if these strategies did not go first, we might answer
  61     //  "sat" for problems that are unsat.
  62     STRAT_QUANT_CEGQI_FEASIBLE,
  63     STRAT_QUANT_SYGUS_FEASIBLE,
  64     // placeholder for last model-sound required strategy
  65     STRAT_LAST_M_SOUND,
  66
  67     //----- finite model finding strategies
  68     //  We require these go here for the sake of finite-model completeness. In
  69     //  other words, if these strategies did not go before other decisions, we
  70     //  might be non-terminating instead of answering "sat" with a solution
  71     //  within a given a bound.
  72     STRAT_UF_COMBINED_CARD,
  73     STRAT_UF_CARD,
  74     STRAT_DT_SYGUS_ENUM_ACTIVE,
  75     STRAT_DT_SYGUS_ENUM_SIZE,
  76     STRAT_STRINGS_SUM_LENGTHS,
  77     STRAT_QUANT_BOUND_INT_SIZE,
  78     STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS,
  79     STRAT_SEP_NEG_GUARD,
  80     // placeholder for last finite-model-complete required strategy
  81     STRAT_LAST_FM_COMPLETE,
  82
  83     //----- decision strategies that are optimizations
  84     STRAT_ARRAYS,
  85
  86     STRAT_LAST
  87   };
  88   /** The scope of a strategy, used in registerStrategy below */
  89   enum StrategyScope
  90   {
  91     // The strategy is user-context dependent, that is, it is cleared when
  92     // the user context is popped.
  93     STRAT_SCOPE_USER_CTX_DEPENDENT,
  94     // The strategy is local to a check-sat call, that is, it is cleared on
  95     // a call to presolve.
  96     STRAT_SCOPE_LOCAL_SOLVE,
  97     // The strategy is context-independent.
  98     STRAT_SCOPE_CTX_INDEPENDENT,
  99   };
 100   DecisionManager(context::Context* userContext);
 101   ~DecisionManager() {}
 102   /** presolve
 103    *
 104    * This clears all decision strategies that are registered to this manager
 105    * that no longer exist in the current user context.
 106    * We require that each satisfiability check beyond the first calls this
 107    * function exactly once. It is called during TheoryEngine::presolve.
 108    */
 109   void presolve();
 110   /**
 111    * Registers the strategy ds with this manager. The id specifies when the
 112    * strategy should be run. The argument sscope indicates the scope of the
 113    * strategy, i.e. how long it persists.
 114    *
 115    * Typically, strategies that are user-context-dependent are those that are
 116    * in response to an assertion (e.g. a strategy that decides that a sygus
 117    * conjecture is feasible). An example of a strategy that is context
 118    * independent is the combined cardinality decision strategy for finite model
 119    * finding for UF, which is not specific to any formula/type.
 120    */
 121   void registerStrategy(StrategyId id,
 122                         DecisionStrategy* ds,
 123                         StrategyScope sscope = STRAT_SCOPE_USER_CTX_DEPENDENT);
 124   /** Get the next decision request
 125    *
 126    * If this method returns a non-null node n, then n is a literal corresponding
 127    * to the next decision that the SAT solver should take. If this method
 128    * returns null, then no decisions are required by a decision strategy
 129    * registered to this class. In the latter case, the SAT solver will choose
 130    * a decision based on its given heuristic.
 131    */
 132   Node getNextDecisionRequest();
 133
 134  private:
 135   /** Map containing all strategies registered to this manager */
 136   std::map<StrategyId, std::vector<DecisionStrategy*> > d_reg_strategy;
 137   /** Set of decision strategies in this user context */
 138   DecisionStrategyList d_strategyCacheC;
 139   /** Set of decision strategies that are context independent */
 140   std::unordered_set<DecisionStrategy*> d_strategyCache;
 141 };
 142
 143 }  // namespace theory
 144 }  // namespace CVC4
 145
 146 #endif /* CVC4__THEORY__DECISION_MANAGER__H */