1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of Decision manager, which manages all decision |
14 |
|
* strategies owned by theory solvers within TheoryEngine. |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "theory/decision_manager.h" |
18 |
|
|
19 |
|
#include "theory/rewriter.h" |
20 |
|
|
21 |
|
using namespace cvc5::kind; |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
|
26 |
8954 |
DecisionManager::DecisionManager(context::Context* userContext) |
27 |
8954 |
: d_strategyCacheC(userContext) |
28 |
|
{ |
29 |
8954 |
} |
30 |
|
|
31 |
12748 |
void DecisionManager::presolve() |
32 |
|
{ |
33 |
12748 |
Trace("dec-manager") << "DecisionManager: presolve." << std::endl; |
34 |
|
// remove the strategies that are not in this user context |
35 |
25496 |
std::unordered_set<DecisionStrategy*> active; |
36 |
15019 |
for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin(); |
37 |
15019 |
i != d_strategyCacheC.end(); |
38 |
|
++i) |
39 |
|
{ |
40 |
2271 |
active.insert(*i); |
41 |
|
} |
42 |
12748 |
active.insert(d_strategyCache.begin(), d_strategyCache.end()); |
43 |
25496 |
std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy; |
44 |
12748 |
d_reg_strategy.clear(); |
45 |
18950 |
for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp) |
46 |
|
{ |
47 |
12864 |
for (DecisionStrategy* ds : rs.second) |
48 |
|
{ |
49 |
6662 |
if (active.find(ds) != active.end()) |
50 |
|
{ |
51 |
|
// if its active, we keep it |
52 |
6505 |
d_reg_strategy[rs.first].push_back(ds); |
53 |
|
} |
54 |
|
} |
55 |
|
} |
56 |
12748 |
} |
57 |
|
|
58 |
12600 |
void DecisionManager::registerStrategy(StrategyId id, |
59 |
|
DecisionStrategy* ds, |
60 |
|
StrategyScope sscope) |
61 |
|
{ |
62 |
25200 |
Trace("dec-manager") << "DecisionManager: Register strategy : " |
63 |
12600 |
<< ds->identify() << ", id = " << id << std::endl; |
64 |
12600 |
ds->initialize(); |
65 |
12600 |
d_reg_strategy[id].push_back(ds); |
66 |
12600 |
if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT) |
67 |
|
{ |
68 |
|
// store it in the user-context-dependent list |
69 |
3996 |
d_strategyCacheC.push_back(ds); |
70 |
|
} |
71 |
8604 |
else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT) |
72 |
|
{ |
73 |
|
// it is context independent |
74 |
8541 |
d_strategyCache.insert(ds); |
75 |
|
} |
76 |
|
else |
77 |
|
{ |
78 |
|
// it is local to this call, we don't cache it |
79 |
63 |
Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE); |
80 |
|
} |
81 |
12600 |
} |
82 |
|
|
83 |
1989483 |
Node DecisionManager::getNextDecisionRequest() |
84 |
|
{ |
85 |
3978966 |
Trace("dec-manager-debug") |
86 |
1989483 |
<< "DecisionManager: Get next decision..." << std::endl; |
87 |
2938407 |
for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : |
88 |
1989483 |
d_reg_strategy) |
89 |
|
{ |
90 |
6512381 |
for (unsigned i = 0, size = rs.second.size(); i < size; i++) |
91 |
|
{ |
92 |
3573974 |
DecisionStrategy* ds = rs.second[i]; |
93 |
7100051 |
Node lit = ds->getNextDecisionRequest(); |
94 |
3573972 |
if (!lit.isNull()) |
95 |
|
{ |
96 |
95790 |
Trace("dec-manager") |
97 |
47895 |
<< "DecisionManager: -> literal " << lit << " decided by strategy " |
98 |
47895 |
<< ds->identify() << std::endl; |
99 |
47895 |
return lit; |
100 |
|
} |
101 |
7052154 |
Trace("dec-manager-debug") << "DecisionManager: " << ds->identify() |
102 |
3526077 |
<< " has no decisions." << std::endl; |
103 |
|
} |
104 |
|
} |
105 |
3883172 |
Trace("dec-manager-debug") |
106 |
1941586 |
<< "DecisionManager: -> no decisions." << std::endl; |
107 |
1941586 |
return Node::null(); |
108 |
|
} |
109 |
|
|
110 |
|
} // namespace theory |
111 |
27735 |
} // namespace cvc5 |