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 |
9853 |
DecisionManager::DecisionManager(context::Context* userContext) |
27 |
9853 |
: d_strategyCacheC(userContext) |
28 |
|
{ |
29 |
9853 |
} |
30 |
|
|
31 |
15204 |
void DecisionManager::presolve() |
32 |
|
{ |
33 |
15204 |
Trace("dec-manager") << "DecisionManager: presolve." << std::endl; |
34 |
|
// remove the strategies that are not in this user context |
35 |
30408 |
std::unordered_set<DecisionStrategy*> active; |
36 |
17514 |
for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin(); |
37 |
17514 |
i != d_strategyCacheC.end(); |
38 |
|
++i) |
39 |
|
{ |
40 |
2310 |
active.insert(*i); |
41 |
|
} |
42 |
15204 |
active.insert(d_strategyCache.begin(), d_strategyCache.end()); |
43 |
30408 |
std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy; |
44 |
15204 |
d_reg_strategy.clear(); |
45 |
23055 |
for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp) |
46 |
|
{ |
47 |
16186 |
for (DecisionStrategy* ds : rs.second) |
48 |
|
{ |
49 |
8335 |
if (active.find(ds) != active.end()) |
50 |
|
{ |
51 |
|
// if its active, we keep it |
52 |
8146 |
d_reg_strategy[rs.first].push_back(ds); |
53 |
|
} |
54 |
|
} |
55 |
|
} |
56 |
15204 |
} |
57 |
|
|
58 |
13832 |
void DecisionManager::registerStrategy(StrategyId id, |
59 |
|
DecisionStrategy* ds, |
60 |
|
StrategyScope sscope) |
61 |
|
{ |
62 |
27664 |
Trace("dec-manager") << "DecisionManager: Register strategy : " |
63 |
13832 |
<< ds->identify() << ", id = " << id << std::endl; |
64 |
13832 |
ds->initialize(); |
65 |
13832 |
d_reg_strategy[id].push_back(ds); |
66 |
13832 |
if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT) |
67 |
|
{ |
68 |
|
// store it in the user-context-dependent list |
69 |
4350 |
d_strategyCacheC.push_back(ds); |
70 |
|
} |
71 |
9482 |
else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT) |
72 |
|
{ |
73 |
|
// it is context independent |
74 |
9404 |
d_strategyCache.insert(ds); |
75 |
|
} |
76 |
|
else |
77 |
|
{ |
78 |
|
// it is local to this call, we don't cache it |
79 |
78 |
Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE); |
80 |
|
} |
81 |
13832 |
} |
82 |
|
|
83 |
2826800 |
Node DecisionManager::getNextDecisionRequest() |
84 |
|
{ |
85 |
5653600 |
Trace("dec-manager-debug") |
86 |
2826800 |
<< "DecisionManager: Get next decision..." << std::endl; |
87 |
4044534 |
for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : |
88 |
2826800 |
d_reg_strategy) |
89 |
|
{ |
90 |
8793862 |
for (unsigned i = 0, size = rs.second.size(); i < size; i++) |
91 |
|
{ |
92 |
4749328 |
DecisionStrategy* ds = rs.second[i]; |
93 |
9438185 |
Node lit = ds->getNextDecisionRequest(); |
94 |
4749326 |
if (!lit.isNull()) |
95 |
|
{ |
96 |
120938 |
Trace("dec-manager") |
97 |
60469 |
<< "DecisionManager: -> literal " << lit << " decided by strategy " |
98 |
60469 |
<< ds->identify() << std::endl; |
99 |
60469 |
return lit; |
100 |
|
} |
101 |
9377714 |
Trace("dec-manager-debug") << "DecisionManager: " << ds->identify() |
102 |
4688857 |
<< " has no decisions." << std::endl; |
103 |
|
} |
104 |
|
} |
105 |
5532658 |
Trace("dec-manager-debug") |
106 |
2766329 |
<< "DecisionManager: -> no decisions." << std::endl; |
107 |
2766329 |
return Node::null(); |
108 |
|
} |
109 |
|
|
110 |
|
} // namespace theory |
111 |
29322 |
} // namespace cvc5 |