diff options
| -rw-r--r-- | src/Makefile.am | 4 | ||||
| -rw-r--r-- | src/theory/decision_manager.cpp | 73 | ||||
| -rw-r--r-- | src/theory/decision_manager.h | 122 | ||||
| -rw-r--r-- | src/theory/decision_strategy.cpp | 145 | ||||
| -rw-r--r-- | src/theory/decision_strategy.h | 146 | ||||
| -rw-r--r-- | src/theory/theory.cpp | 8 | ||||
| -rw-r--r-- | src/theory/theory.h | 13 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 92 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 15 |
9 files changed, 572 insertions, 46 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 5f6d7e9ad..77fd455bb 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -406,6 +406,10 @@ libcvc4_la_SOURCES = \ theory/datatypes/type_enumerator.h \ theory/datatypes/sygus_simple_sym.cpp \ theory/datatypes/sygus_simple_sym.h \ + theory/decision_manager.cpp \ + theory/decision_manager.h \ + theory/decision_strategy.cpp \ + theory/decision_strategy.h \ theory/ext_theory.cpp \ theory/ext_theory.h \ theory/fp/theory_fp.cpp \ 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 diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h new file mode 100644 index 000000000..ff30a13f8 --- /dev/null +++ b/src/theory/decision_manager.h @@ -0,0 +1,122 @@ +/********************* */ +/*! \file decision_manager.h + ** \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 Decision manager, which manages all decision strategies owned by + ** theory solvers within TheoryEngine. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DECISION_MANAGER__H +#define __CVC4__THEORY__DECISION_MANAGER__H + +#include <map> +#include "theory/decision_strategy.h" + +namespace CVC4 { +namespace theory { + +/** DecisionManager + * + * This class manages all "decision strategies" for theory solvers in + * TheoryEngine. A decision strategy is a callback in the SAT solver for + * imposing its next decision. This is useful, for instance, in + * branch-and-bound algorithms where we require that the first decision + * is a bound on some quantity. For instance, finite model finding may impose + * a bound on the cardinality of an uninterpreted sort as the first decision. + * + * This class maintains a user-context-dependent set of pointers to + * DecisionStrategy objects, which implement indivdual decision strategies. + * + * Decision strategies may be registered to this class via registerStrategy + * at any time during solving. They are cleared via a call to reset during + * TheoryEngine's postSolve method. + * + * Decision strategies have a fixed order, which is managed by the enumeration + * type StrategyId, where strategies with smaller id have higher precedence + * in our global decision strategy. + */ +class DecisionManager +{ + public: + enum StrategyId + { + // The order of the global decision strategy used by the TheoryEngine + // for getNextDecision. + + //----- assume-feasibile strategies + // These are required to go first for the sake of model-soundness. In + // other words, if these strategies did not go first, we might answer + // "sat" for problems that are unsat. + STRAT_QUANT_CEGQI_FEASIBLE, + STRAT_QUANT_SYGUS_FEASIBLE, + STRAT_QUANT_SYGUS_STREAM_FEASIBLE, + // placeholder for last model-sound required strategy + STRAT_LAST_M_SOUND, + + //----- finite model finding strategies + // We require these go here for the sake of finite-model completeness. In + // other words, if these strategies did not go before other decisions, we + // might be non-terminating instead of answering "sat" with a solution + // within a given a bound. + STRAT_UF_COMBINED_CARD, + STRAT_UF_CARD, + STRAT_DT_SYGUS_ENUM_ACTIVE, + STRAT_DT_SYGUS_ENUM_SIZE, + STRAT_QUANT_BOUND_INT_SIZE, + STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, + STRAT_STRINGS_SUM_LENGTHS, + STRAT_SEP_NEG_GUARD, + // placeholder for last finite-model-complete required strategy + STRAT_LAST_FM_COMPLETE, + + //----- decision strategies that are optimizations + STRAT_ARRAYS, + + STRAT_LAST + }; + DecisionManager(context::Context* satContext); + ~DecisionManager() {} + /** reset the strategy + * + * This clears all decision strategies that are registered to this manager. + * We require that each satisfiability check beyond the first calls this + * function exactly once. Currently, it is called during + * TheoryEngine::postSolve. + */ + void reset(); + /** + * Registers the strategy ds with this manager. The id specifies when the + * strategy should be run. + */ + void registerStrategy(StrategyId id, DecisionStrategy* ds); + /** Get the next decision request + * + * If this method returns a non-null node n, then n is a literal corresponding + * to the next decision that the SAT solver should take. If this method + * returns null, then no decisions are required by a decision strategy + * registered to this class. In the latter case, the SAT solver will choose + * a decision based on its given heuristic. + * + * The argument priority has the same role as in + * Theory::getNextDecisionRequest. + */ + Node getNextDecisionRequest(unsigned& priorty); + + private: + /** Map containing all strategies registered to this manager */ + std::map<StrategyId, std::vector<DecisionStrategy*> > d_reg_strategy; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__DECISION_MANAGER__H */ diff --git a/src/theory/decision_strategy.cpp b/src/theory/decision_strategy.cpp new file mode 100644 index 000000000..fcd11f6ba --- /dev/null +++ b/src/theory/decision_strategy.cpp @@ -0,0 +1,145 @@ +/********************* */ +/*! \file decision_strategy.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 base classes for decision strategies used by theory + ** solvers for use in the DecisionManager of TheoryEngine. + **/ + +#include "theory/decision_strategy.h" + +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext, + Valuation valuation) + : d_valuation(valuation), + d_has_curr_literal(false, satContext), + d_curr_literal(0, satContext) +{ +} + +void DecisionStrategyFmf::initialize() { d_literals.clear(); } + +Node DecisionStrategyFmf::getNextDecisionRequest() +{ + Trace("dec-strategy-debug") + << "Get next decision request " << identify() << "..." << std::endl; + if (d_has_curr_literal.get()) + { + Trace("dec-strategy-debug") << "...already has decision" << std::endl; + return Node::null(); + } + bool success; + unsigned curr_lit = d_curr_literal.get(); + do + { + success = true; + // get the current literal + Node lit = getLiteral(curr_lit); + Trace("dec-strategy-debug") + << "...check literal #" << curr_lit << " : " << lit << std::endl; + // if out of literals, we are done in the current SAT context + if (!lit.isNull()) + { + bool value; + if (!d_valuation.hasSatValue(lit, value)) + { + Trace("dec-strategy-debug") << "...not assigned, return." << std::endl; + // if it has not been decided, return it + return lit; + } + else if (!value) + { + Trace("dec-strategy-debug") + << "...assigned false, increment." << std::endl; + // asserted false, the current literal is incremented + curr_lit = d_curr_literal.get() + 1; + d_curr_literal.set(curr_lit); + // repeat + success = false; + } + else + { + Trace("dec-strategy-debug") << "...already assigned true." << std::endl; + } + } + else + { + Trace("dec-strategy-debug") << "...exhausted literals." << std::endl; + } + } while (!success); + // the current literal has been decided with the right polarity, we are done + d_has_curr_literal = true; + return Node::null(); +} + +bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const +{ + if (d_has_curr_literal.get()) + { + i = d_curr_literal.get(); + return true; + } + return false; +} + +Node DecisionStrategyFmf::getAssertedLiteral() +{ + if (d_has_curr_literal.get()) + { + Assert(d_curr_literal.get() < d_literals.size()); + return getLiteral(d_curr_literal.get()); + } + return Node::null(); +} + +Node DecisionStrategyFmf::getLiteral(unsigned n) +{ + // allocate until the index is valid + while (n >= d_literals.size()) + { + Node lit = mkLiteral(d_literals.size()); + if (!lit.isNull()) + { + lit = Rewriter::rewrite(lit); + lit = d_valuation.ensureLiteral(lit); + } + d_literals.push_back(lit); + } + return d_literals[n]; +} + +DecisionStrategySingleton::DecisionStrategySingleton( + const char* name, + Node lit, + context::Context* satContext, + Valuation valuation) + : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit) +{ +} + +Node DecisionStrategySingleton::mkLiteral(unsigned n) +{ + if (n == 0) + { + return d_literal; + } + return Node::null(); +} + +Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; } + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h new file mode 100644 index 000000000..04788f515 --- /dev/null +++ b/src/theory/decision_strategy.h @@ -0,0 +1,146 @@ +/********************* */ +/*! \file decision_strategy.h + ** \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 Base classes for decision strategies used by theory solvers + ** for use in the DecisionManager of TheoryEngine. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DECISION_STRATEGY__H +#define __CVC4__THEORY__DECISION_STRATEGY__H + +#include <map> +#include "context/cdo.h" +#include "expr/node.h" +#include "theory/valuation.h" + +namespace CVC4 { +namespace theory { + +/** + * Virtual base class for decision strategies. + */ +class DecisionStrategy +{ + public: + DecisionStrategy() {} + virtual ~DecisionStrategy() {} + /** + * Initalize this strategy, This is called once per satisfiability call by + * the DecisionManager, prior to using this strategy. + */ + virtual void initialize() = 0; + /** + * If this method returns a non-null node n, then n is the required next + * decision of this strategy. It must be the case that n is a literal in + * the current CNF stream. + */ + virtual Node getNextDecisionRequest() = 0; + /** identify this strategy (for debugging) */ + virtual std::string identify() const = 0; +}; + +/** + * Decision strategy finite model finding. + * + * This is a virtual base class for decision strategies that follow the + * "finite model finding" pattern for decisions. Such strategies have the + * distinguishing feature that they are interested in a stream of literals + * L_1, L_2, L_3, ... and so on. At any given time, they request that L_i is + * asserted true for a minimal i. + * + * To enforce this strategy, this class maintains a SAT-context dependent + * index d_curr_literal, which corresponds to the minimal index of a literal + * in the above list that is not asserted false. A call to + * getNextDecisionRequest increments this value until we find a literal L_j + * that is not assigned false. If L_j is unassigned, we return it as a decision, + * otherwise we return no decisions. + */ +class DecisionStrategyFmf : public DecisionStrategy +{ + public: + DecisionStrategyFmf(context::Context* satContext, Valuation valuation); + virtual ~DecisionStrategyFmf() {} + /** initialize */ + void initialize() override; + /** get next decision request */ + Node getNextDecisionRequest() override; + /** Make the n^th literal of this strategy */ + virtual Node mkLiteral(unsigned n) = 0; + /** + * This method returns true iff there exists a (minimal) i such that L_i + * is a literal allocated by this class, and is asserted true in the current + * context. If it returns true, the argument i is set to this i. + */ + bool getAssertedLiteralIndex(unsigned& i) const; + /** + * This method returns the literal L_i allocated by this class that + * has been asserted true in the current context and is such that i is + * minimal. It returns null if no such literals exist. + */ + Node getAssertedLiteral(); + /** Get the n^th literal of this strategy */ + Node getLiteral(unsigned lit); + + protected: + /** + * The valuation of this class, used for knowing what literals are asserted, + * and with what polarity. + */ + Valuation d_valuation; + /** + * The (SAT-context-dependent) flag that is true if there exists a literal + * of this class that is asserted true in the current context, according to + * d_valuation. + */ + context::CDO<bool> d_has_curr_literal; + /** + * The (SAT-context-dependent) index of the current literal of this strategy. + * This corresponds to the first literal that is not asserted false in the + * current context, according to d_valuation. + */ + context::CDO<unsigned> d_curr_literal; + /** the list of literals of this strategy */ + std::vector<Node> d_literals; +}; + +/** + * Special case of above where we only wish to allocate a single literal L_1. + */ +class DecisionStrategySingleton : public DecisionStrategyFmf +{ + public: + DecisionStrategySingleton(const char* name, + Node lit, + context::Context* satContext, + Valuation valuation); + /** + * Make the n^th literal of this strategy. This method returns d_literal if + * n=0, null otherwise. + */ + Node mkLiteral(unsigned n) override; + /** Get single literal */ + Node getSingleLiteral(); + /** identify */ + std::string identify() const override { return d_name; } + + private: + /** the name of this strategy */ + std::string d_name; + /** the literal to decide on */ + Node d_literal; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__DECISION_STRATEGY__H */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index eedf0ff52..a4e814e8c 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -69,6 +69,7 @@ Theory::Theory(TheoryId id, d_sharedTermsIndex(satContext, 0), d_careGraph(NULL), d_quantEngine(NULL), + d_decManager(nullptr), d_extTheory(NULL), d_checkTime(getStatsPrefix(id) + name + "::checkTime"), d_computeCareGraphTime(getStatsPrefix(id) + name @@ -351,6 +352,13 @@ void Theory::setQuantifiersEngine(QuantifiersEngine* qe) { d_quantEngine = qe; } +void Theory::setDecisionManager(DecisionManager* dm) +{ + Assert(d_decManager == nullptr); + Assert(dm != nullptr); + d_decManager = dm; +} + void Theory::setupExtTheory() { Assert(d_extTheory == NULL); d_extTheory = new ExtTheory(this); diff --git a/src/theory/theory.h b/src/theory/theory.h index 5d176a36b..534f091bf 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -25,8 +25,8 @@ #include <string> #include <unordered_set> -#include "context/cdlist.h" #include "context/cdhashset.h" +#include "context/cdlist.h" #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" @@ -39,6 +39,7 @@ #include "smt/logic_request.h" #include "theory/assertion.h" #include "theory/care_graph.h" +#include "theory/decision_manager.h" #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/valuation.h" @@ -130,6 +131,9 @@ private: */ QuantifiersEngine* d_quantEngine; + /** Pointer to the decision manager. */ + DecisionManager* d_decManager; + /** Extended theory module or NULL. Owned by the theory. */ ExtTheory* d_extTheory; @@ -404,6 +408,9 @@ public: return d_quantEngine; } + /** Get the decision manager associated to this theory. */ + DecisionManager* getDecisionManager() { return d_decManager; } + /** * Finish theory initialization. At this point, options and the logic * setting are final, and the master equality engine and quantifiers @@ -461,7 +468,9 @@ public: virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { } /** Called to set the quantifiers engine. */ - virtual void setQuantifiersEngine(QuantifiersEngine* qe); + void setQuantifiersEngine(QuantifiersEngine* qe); + /** Called to set the decision manager. */ + void setDecisionManager(DecisionManager* dm); /** Setup an ExtTheory module for this Theory. Can only be called once. */ void setupExtTheory(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 41ab45170..37276ac5e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -244,6 +244,9 @@ void TheoryEngine::finishInit() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if (d_theoryTable[theoryId]) { + // set the decision manager for the theory + d_theoryTable[theoryId]->setDecisionManager(d_decManager.get()); + // finish initializing the theory d_theoryTable[theoryId]->finishInit(); } } @@ -273,50 +276,50 @@ void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ } } - TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo, LemmaChannels* channels) -: d_propEngine(NULL), - d_decisionEngine(NULL), - d_context(context), - d_userContext(userContext), - d_logicInfo(logicInfo), - d_sharedTerms(this, context), - d_masterEqualityEngine(NULL), - d_masterEENotify(*this), - d_quantEngine(NULL), - d_curr_model(NULL), - d_aloc_curr_model(false), - d_curr_model_builder(NULL), - d_aloc_curr_model_builder(false), - d_ppCache(), - d_possiblePropagations(context), - d_hasPropagated(context), - d_inConflict(context, false), - d_hasShutDown(false), - d_incomplete(context, false), - d_propagationMap(context), - d_propagationMapTimestamp(context, 0), - d_propagatedLiterals(context), - d_propagatedLiteralsIndex(context, 0), - d_atomRequests(context), - d_tform_remover(iteRemover), - d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), - d_true(), - d_false(), - d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()), - d_channels(channels), - d_inPreregister(false), - d_factsAsserted(context, false), - d_preRegistrationVisitor(this, context), - d_sharedTermsVisitor(d_sharedTerms), - d_theoryAlternatives(), - d_attr_handle(), - d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) + : d_propEngine(nullptr), + d_decisionEngine(nullptr), + d_context(context), + d_userContext(userContext), + d_logicInfo(logicInfo), + d_sharedTerms(this, context), + d_masterEqualityEngine(nullptr), + d_masterEENotify(*this), + d_quantEngine(nullptr), + d_decManager(new DecisionManager(context)), + d_curr_model(nullptr), + d_aloc_curr_model(false), + d_curr_model_builder(nullptr), + d_aloc_curr_model_builder(false), + d_ppCache(), + d_possiblePropagations(context), + d_hasPropagated(context), + d_inConflict(context, false), + d_hasShutDown(false), + d_incomplete(context, false), + d_propagationMap(context), + d_propagationMapTimestamp(context, 0), + d_propagatedLiterals(context), + d_propagatedLiteralsIndex(context, 0), + d_atomRequests(context), + d_tform_remover(iteRemover), + d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), + d_true(), + d_false(), + d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()), + d_channels(channels), + d_inPreregister(false), + d_factsAsserted(context, false), + d_preRegistrationVisitor(this, context), + d_sharedTermsVisitor(d_sharedTerms), + d_theoryAlternatives(), + d_attr_handle(), + d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) @@ -324,7 +327,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_theoryTable[theoryId] = NULL; d_theoryOut[theoryId] = NULL; } - + smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -763,9 +766,10 @@ void TheoryEngine::propagate(Theory::Effort effort) { } Node TheoryEngine::getNextDecisionRequest() { - // Definition of the statement that is to be run by every theory unsigned min_priority = 0; - Node dec; + Node dec = d_decManager->getNextDecisionRequest(min_priority); + + // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif @@ -939,6 +943,10 @@ bool TheoryEngine::presolve() { }/* TheoryEngine::presolve() */ void TheoryEngine::postsolve() { + // Reset the decision manager. This clears its decision strategies, which are + // user-context-dependent. + d_decManager->reset(); + // Reset the interrupt flag d_interrupted = false; bool CVC4_UNUSED wasInConflict = d_inConflict; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 65402f0a6..b5ac208d7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -35,6 +35,7 @@ #include "smt/command.h" #include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" +#include "theory/decision_manager.h" #include "theory/interrupted.h" #include "theory/rewriter.h" #include "theory/shared_terms_database.h" @@ -198,6 +199,10 @@ class TheoryEngine { * The quantifiers engine */ theory::QuantifiersEngine* d_quantEngine; + /** + * The decision manager + */ + std::unique_ptr<theory::DecisionManager> d_decManager; /** * Default model object @@ -524,9 +529,15 @@ public: theory::QuantifiersEngine* getQuantifiersEngine() const { return d_quantEngine; } + /** + * Get a pointer to the underlying decision manager. + */ + theory::DecisionManager* getDecisionManager() const + { + return d_decManager.get(); + } -private: - + private: /** * Helper for preprocess */ |