1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Mathias Preiner
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Decision manager, which manages all decision strategies owned by
14 * theory solvers within TheoryEngine.
17 #include "cvc5_private.h"
19 #ifndef CVC5__THEORY__DECISION_MANAGER__H
20 #define CVC5__THEORY__DECISION_MANAGER__H
23 #include "context/cdlist.h"
24 #include "theory/decision_strategy.h"
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.
38 * This class maintains a user-context-dependent set of pointers to
39 * DecisionStrategy objects, which implement indivdual decision strategies.
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.
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.
51 typedef context::CDList
<DecisionStrategy
*> DecisionStrategyList
;
56 // The order of the global decision strategy used by the TheoryEngine
57 // for getNextDecision.
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
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
,
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
,
81 // placeholder for last finite-model-complete required strategy
82 STRAT_LAST_FM_COMPLETE
,
84 //----- decision strategies that are optimizations
89 /** The scope of a strategy, used in registerStrategy below */
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
,
101 DecisionManager(context::Context
* userContext
);
102 ~DecisionManager() {}
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.
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.
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.
122 void registerStrategy(StrategyId id
,
123 DecisionStrategy
* ds
,
124 StrategyScope sscope
= STRAT_SCOPE_USER_CTX_DEPENDENT
);
125 /** Get the next decision request
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.
133 Node
getNextDecisionRequest();
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
;
144 } // namespace theory
147 #endif /* CVC5__THEORY__DECISION_MANAGER__H */