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
|
/********************* */
/*! \file decision_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 "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
{
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
};
DecisionManager(context::Context* satContext);
~DecisionManager() {}
/** reset the strategy
*
* This clears all decision strategies that are registered to this manager.
* We require that each satisfiability check beyond the first calls this
* function exactly once. Currently, it is called during
* TheoryEngine::postSolve.
*/
void reset();
/**
* Registers the strategy ds with this manager. The id specifies when the
* strategy should be run.
*/
void registerStrategy(StrategyId id, DecisionStrategy* ds);
/** 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.
*
* The argument priority has the same role as in
* Theory::getNextDecisionRequest.
*/
Node getNextDecisionRequest(unsigned& priorty);
private:
/** Map containing all strategies registered to this manager */
std::map<StrategyId, std::vector<DecisionStrategy*> > d_reg_strategy;
};
} // namespace theory
} // namespace CVC4
#endif /* __CVC4__THEORY__DECISION_MANAGER__H */
|
