1 /********************* */
2 /*! \file decision_manager.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of Decision manager, which manages all decision
13 ** strategies owned by theory solvers within TheoryEngine.
16 #include "theory/decision_manager.h"
18 #include "theory/rewriter.h"
20 using namespace CVC4::kind
;
25 DecisionManager::DecisionManager(context::Context
* userContext
)
26 : d_strategyCacheC(userContext
)
30 void DecisionManager::presolve()
32 Trace("dec-manager") << "DecisionManager: presolve." << std::endl
;
33 // remove the strategies that are not in this user context
34 std::unordered_set
<DecisionStrategy
*> active
;
35 for (DecisionStrategyList::const_iterator i
= d_strategyCacheC
.begin();
36 i
!= d_strategyCacheC
.end();
41 active
.insert(d_strategyCache
.begin(), d_strategyCache
.end());
42 std::map
<StrategyId
, std::vector
<DecisionStrategy
*> > tmp
= d_reg_strategy
;
43 d_reg_strategy
.clear();
44 for (std::pair
<const StrategyId
, std::vector
<DecisionStrategy
*> >& rs
: tmp
)
46 for (DecisionStrategy
* ds
: rs
.second
)
48 if (active
.find(ds
) != active
.end())
50 // if its active, we keep it
51 d_reg_strategy
[rs
.first
].push_back(ds
);
57 void DecisionManager::registerStrategy(StrategyId id
,
61 Trace("dec-manager") << "DecisionManager: Register strategy : "
62 << ds
->identify() << ", id = " << id
<< std::endl
;
64 d_reg_strategy
[id
].push_back(ds
);
65 if (sscope
== STRAT_SCOPE_USER_CTX_DEPENDENT
)
67 // store it in the user-context-dependent list
68 d_strategyCacheC
.push_back(ds
);
70 else if (sscope
== STRAT_SCOPE_CTX_INDEPENDENT
)
72 // it is context independent
73 d_strategyCache
.insert(ds
);
77 // it is local to this call, we don't cache it
78 Assert(sscope
== STRAT_SCOPE_LOCAL_SOLVE
);
82 Node
DecisionManager::getNextDecisionRequest()
84 Trace("dec-manager-debug")
85 << "DecisionManager: Get next decision..." << std::endl
;
86 for (const std::pair
<const StrategyId
, std::vector
<DecisionStrategy
*> >& rs
:
89 for (unsigned i
= 0, size
= rs
.second
.size(); i
< size
; i
++)
91 DecisionStrategy
* ds
= rs
.second
[i
];
92 Node lit
= ds
->getNextDecisionRequest();
96 << "DecisionManager: -> literal " << lit
<< " decided by strategy "
97 << ds
->identify() << std::endl
;
100 Trace("dec-manager-debug") << "DecisionManager: " << ds
->identify()
101 << " has no decisions." << std::endl
;
104 Trace("dec-manager-debug")
105 << "DecisionManager: -> no decisions." << std::endl
;
109 } // namespace theory