src/theory/decision_manager.h

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