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 \
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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
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);
#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"
#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"
*/
QuantifiersEngine* d_quantEngine;
+ /** Pointer to the decision manager. */
+ DecisionManager* d_decManager;
+
/** Extended theory module or NULL. Owned by the theory. */
ExtTheory* d_extTheory;
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
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();
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();
}
}
}
}
-
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)
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);
}
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
}/* 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;
#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"
* The quantifiers engine
*/
theory::QuantifiersEngine* d_quantEngine;
+ /**
+ * The decision manager
+ */
+ std::unique_ptr<theory::DecisionManager> d_decManager;
/**
* Default model object
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
*/
projects / cvc5.git / commitdiff