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