diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-12 13:18:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-12 13:18:13 -0500 |
commit | f4f11801394afa718a5125e4386704a72e74ca48 (patch) | |
tree | 05ebc80af205de90000942de8cfb58a906fcc890 /src/theory/decision_manager.cpp | |
parent | 700a21a55d277d7bb4e475849e98aab58d91dba5 (diff) |
Initial infrastructure for theory decision manager (#2447)
Diffstat (limited to 'src/theory/decision_manager.cpp')
-rw-r--r-- | src/theory/decision_manager.cpp | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/src/theory/decision_manager.cpp b/src/theory/decision_manager.cpp new file mode 100644 index 000000000..3cc67fe6d --- /dev/null +++ b/src/theory/decision_manager.cpp @@ -0,0 +1,73 @@ +/********************* */ +/*! \file decision_manager.cpp + ** \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 Implementation of Decision manager, which manages all decision + ** strategies owned by theory solvers within TheoryEngine. + **/ + +#include "theory/decision_manager.h" + +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +DecisionManager::DecisionManager(context::Context* satContext) {} + +void DecisionManager::reset() +{ + Trace("dec-manager") << "DecisionManager: reset." << std::endl; + d_reg_strategy.clear(); +} + +void DecisionManager::registerStrategy(StrategyId id, DecisionStrategy* ds) +{ + Trace("dec-manager") << "DecisionManager: Register strategy : " + << ds->identify() << ", id = " << id << std::endl; + ds->initialize(); + d_reg_strategy[id].push_back(ds); +} + +Node DecisionManager::getNextDecisionRequest(unsigned& priority) +{ + Trace("dec-manager-debug") + << "DecisionManager: Get next decision..." << std::endl; + for (const std::pair<StrategyId, std::vector<DecisionStrategy*> >& rs : + d_reg_strategy) + { + for (unsigned i = 0, size = rs.second.size(); i < size; i++) + { + DecisionStrategy* ds = rs.second[i]; + Node lit = ds->getNextDecisionRequest(); + if (!lit.isNull()) + { + StrategyId sid = rs.first; + priority = sid < STRAT_LAST_M_SOUND + ? 0 + : (sid < STRAT_LAST_FM_COMPLETE ? 1 : 2); + Trace("dec-manager") + << "DecisionManager: -> literal " << lit << " decided by strategy " + << ds->identify() << std::endl; + return lit; + } + Trace("dec-manager-debug") << "DecisionManager: " << ds->identify() + << " has no decisions." << std::endl; + } + } + Trace("dec-manager-debug") + << "DecisionManager: -> no decisions." << std::endl; + return Node::null(); +} + +} // namespace theory +} // namespace CVC4 |