GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/decision_manager.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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-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.\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
8994
  ~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 */