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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 

* branchandbound 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 usercontextdependent 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 

// assumefeasibile strategies 
59 

// These are required to go first for the sake of modelsoundness. 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 modelsound required strategy 
65 

STRAT_LAST_M_SOUND, 
66 


67 

// finite model finding strategies 
68 

// We require these go here for the sake of finitemodel completeness. In 
69 

// other words, if these strategies did not go before other decisions, we 
70 

// might be nonterminating 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 finitemodelcomplete 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 usercontext 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 checksat call, that is, it is cleared on 
95 

// a call to presolve. 
96 

STRAT_SCOPE_LOCAL_SOLVE, 
97 

// The strategy is contextindependent. 
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 usercontextdependent 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 nonnull 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 */ 