This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use.
namespace cvc5 {
namespace decision {
-DecisionEngine::DecisionEngine(context::Context* c,
- context::UserContext* u,
- prop::SkolemDefManager* skdm,
- ResourceManager* rm)
- : d_decEngineOld(new DecisionEngineOld(c, u)),
- d_jstrat(new JustificationStrategy(c, u, skdm)),
+DecisionEngine::DecisionEngine(context::Context* c, ResourceManager* rm)
+ : d_context(c),
d_resourceManager(rm),
- d_useOld(options::decisionMode() != options::DecisionMode::JUSTIFICATION)
+ d_cnfStream(nullptr),
+ d_satSolver(nullptr)
{
}
-void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss,
- prop::CnfStream* cs)
+void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs)
{
- if (d_useOld)
- {
- d_decEngineOld->setSatSolver(ss);
- d_decEngineOld->setCnfStream(cs);
- return;
- }
- d_jstrat->finishInit(ss, cs);
-}
-
-void DecisionEngine::presolve()
-{
- if (!d_useOld)
- {
- d_jstrat->presolve();
- }
+ d_satSolver = ss;
+ d_cnfStream = cs;
}
prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
{
d_resourceManager->spendResource(Resource::DecisionStep);
- if (d_useOld)
- {
- return d_decEngineOld->getNext(stopSearch);
- }
- return d_jstrat->getNext(stopSearch);
-}
-
-bool DecisionEngine::isDone()
-{
- if (d_useOld)
- {
- return d_decEngineOld->isDone();
- }
- return d_jstrat->isDone();
+ return getNextInternal(stopSearch);
}
-void DecisionEngine::addAssertion(TNode assertion)
+DecisionEngineEmpty::DecisionEngineEmpty(context::Context* sc,
+ ResourceManager* rm)
+ : DecisionEngine(sc, rm)
{
- if (d_useOld)
- {
- d_decEngineOld->addAssertion(assertion);
- return;
- }
- d_jstrat->addAssertion(assertion);
}
-
-void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
-{
- if (d_useOld)
- {
- d_decEngineOld->addSkolemDefinition(lem, skolem);
- }
- else
- {
- d_jstrat->addSkolemDefinition(lem, skolem);
- }
-}
-
-void DecisionEngine::notifyAsserted(TNode n)
+bool DecisionEngineEmpty::isDone() { return false; }
+void DecisionEngineEmpty::addAssertion(TNode assertion) {}
+void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {}
+prop::SatLiteral DecisionEngineEmpty::getNextInternal(bool& stopSearch)
{
- if (d_useOld)
- {
- return;
- }
- // old implementation does not use this
- d_jstrat->notifyAsserted(n);
+ return undefSatLiteral;
}
} // namespace decision
#ifndef CVC5__DECISION__DECISION_ENGINE_H
#define CVC5__DECISION__DECISION_ENGINE_H
-#include "decision/justification_strategy.h"
#include "expr/node.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_types.h"
namespace cvc5 {
-
-namespace prop {
-class SkolemDefManager;
-}
-
-class DecisionEngineOld;
-
namespace decision {
class DecisionEngine
public:
/** Constructor */
DecisionEngine(context::Context* sc,
- context::UserContext* uc,
- prop::SkolemDefManager* skdm,
ResourceManager* rm);
+ virtual ~DecisionEngine() {}
/** Finish initialize */
void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
/** Presolve, called at the beginning of each check-sat call */
- void presolve();
+ virtual void presolve() {}
- /** Gets the next decision based on strategies that are enabled */
+ /**
+ * Gets the next decision based on strategies that are enabled. This sets
+ * stopSearch to true if no further SAT variables need to be assigned in
+ * this SAT context.
+ */
prop::SatLiteral getNext(bool& stopSearch);
/** Is the DecisionEngine in a state where it has solved everything? */
- bool isDone();
+ virtual bool isDone() = 0;
/**
* Notify this class that assertion is an (input) assertion, not corresponding
* to a skolem definition.
*/
- void addAssertion(TNode assertion);
+ virtual void addAssertion(TNode assertion) = 0;
/**
- * !!!! temporary until the old justification implementation is deleted.
- * Notify this class that lem is the skolem definition for skolem, which is
+ * Notify this class that lem is the skolem definition for skolem, which is
* a part of the current assertions.
*/
- void addSkolemDefinition(TNode lem, TNode skolem);
+ virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
/**
* Notify this class that the literal n has been asserted, possibly
* propagated by the SAT solver.
*/
- void notifyAsserted(TNode n);
+ virtual void notifyAsserted(TNode n) {}
- private:
- /** The old implementation */
- std::unique_ptr<DecisionEngineOld> d_decEngineOld;
- /** The new implementation */
- std::unique_ptr<JustificationStrategy> d_jstrat;
+ protected:
+ /** Get next internal, the engine-specific implementation of getNext */
+ virtual prop::SatLiteral getNextInternal(bool& stopSearch) = 0;
+ /** Pointer to the SAT context */
+ context::Context* d_context;
/** Pointer to resource manager for associated SmtEngine */
ResourceManager* d_resourceManager;
- /** using old implementation? */
- bool d_useOld;
+ /** Pointer to the CNF stream */
+ prop::CnfStream* d_cnfStream;
+ /** Pointer to the SAT solver */
+ prop::CDCLTSatSolverInterface* d_satSolver;
+};
+
+/**
+ * Instance of the above class which does nothing. This is used when
+ * the decision mode is set to internal.
+ */
+class DecisionEngineEmpty : public DecisionEngine
+{
+ public:
+ DecisionEngineEmpty(context::Context* sc, ResourceManager* rm);
+ bool isDone() override;
+ void addAssertion(TNode assertion) override;
+ void addSkolemDefinition(TNode lem, TNode skolem) override;
+
+ protected:
+ prop::SatLiteral getNextInternal(bool& stopSearch) override;
};
} // namespace decision
namespace cvc5 {
DecisionEngineOld::DecisionEngineOld(context::Context* sc,
- context::UserContext* uc)
- : d_cnfStream(nullptr),
- d_satSolver(nullptr),
- d_satContext(sc),
- d_userContext(uc),
+ context::UserContext* uc,
+ ResourceManager* rm)
+ : DecisionEngine(sc, rm),
d_result(sc, SAT_VALUE_UNKNOWN),
d_engineState(0),
- d_enabledITEStrategy(nullptr)
+ d_enabledITEStrategy(nullptr),
+ d_decisionStopOnly(options::decisionMode()
+ == options::DecisionMode::STOPONLY_OLD)
{
Trace("decision") << "Creating decision engine" << std::endl;
Assert(d_engineState == 0);
Trace("decision-init") << "DecisionEngineOld::init()" << std::endl;
Trace("decision-init") << " * options->decisionMode: "
<< options::decisionMode() << std::endl;
- Trace("decision-init") << " * options->decisionStopOnly: "
- << options::decisionStopOnly() << std::endl;
+ Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly
+ << std::endl;
if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
{
- d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
- this, d_userContext, d_satContext));
+ d_enabledITEStrategy.reset(
+ new decision::JustificationHeuristic(this, uc, sc));
}
}
d_enabledITEStrategy.reset(nullptr);
}
-SatLiteral DecisionEngineOld::getNext(bool& stopSearch)
+SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch)
{
Assert(d_cnfStream != nullptr)
<< "Forgot to set cnfStream for decision engine?";
Assert(d_satSolver != nullptr)
<< "Forgot to set satSolver for decision engine?";
- return d_enabledITEStrategy == nullptr
- ? undefSatLiteral
- : d_enabledITEStrategy->getNext(stopSearch);
+ SatLiteral ret = d_enabledITEStrategy == nullptr
+ ? undefSatLiteral
+ : d_enabledITEStrategy->getNext(stopSearch);
+ // if we are doing stop only, we don't return the literal
+ return d_decisionStopOnly ? undefSatLiteral : ret;
}
void DecisionEngineOld::addAssertion(TNode assertion)
#include "base/output.h"
#include "context/cdo.h"
+#include "decision/decision_engine.h"
#include "decision/decision_strategy.h"
#include "expr/node.h"
#include "prop/cnf_stream.h"
namespace cvc5 {
-class DecisionEngineOld
+class DecisionEngineOld : public decision::DecisionEngine
{
public:
// Necessary functions
/** Constructor */
- DecisionEngineOld(context::Context* sc, context::UserContext* uc);
+ DecisionEngineOld(context::Context* sc,
+ context::UserContext* uc,
+ ResourceManager* rm);
/** Destructor, currently does nothing */
~DecisionEngineOld()
Trace("decision") << "Destroying decision engine" << std::endl;
}
- void setSatSolver(CDCLTSatSolverInterface* ss)
- {
- // setPropEngine should not be called more than once
- Assert(d_satSolver == NULL);
- Assert(ss != NULL);
- d_satSolver = ss;
- }
-
- void setCnfStream(CnfStream* cs)
- {
- // setPropEngine should not be called more than once
- Assert(d_cnfStream == NULL);
- Assert(cs != NULL);
- d_cnfStream = cs;
- }
-
/**
* This is called by SmtEngine, at shutdown time, just before
* destruction. It is important because there are destruction
// Interface for External World to use our services
/** Gets the next decision based on strategies that are enabled */
- SatLiteral getNext(bool& stopSearch);
+ SatLiteral getNextInternal(bool& stopSearch) override;
/** Is the DecisionEngineOld in a state where it has solved everything? */
- bool isDone()
+ bool isDone() override
{
Trace("decision") << "DecisionEngineOld::isDone() returning "
<< (d_result != SAT_VALUE_UNKNOWN)
* Notify this class that assertion is an (input) assertion, not corresponding
* to a skolem definition.
*/
- void addAssertion(TNode assertion);
+ void addAssertion(TNode assertion) override;
/**
* Notify this class that lem is the skolem definition for skolem, which is
* a part of the current assertions.
*/
- void addSkolemDefinition(TNode lem, TNode skolem);
+ void addSkolemDefinition(TNode lem, TNode skolem) override;
// Interface for Strategies to use stuff stored in Decision Engine
// (which was possibly requested by them on initialization)
// Disable creating decision engine without required parameters
DecisionEngineOld();
- CnfStream* d_cnfStream;
- CDCLTSatSolverInterface* d_satSolver;
-
- context::Context* d_satContext;
- context::UserContext* d_userContext;
-
// Does decision engine know the answer?
context::CDO<SatValue> d_result;
unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
/** The ITE decision strategy we have allocated */
std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
+ /** Whether we are using stop only */
+ bool d_decisionStopOnly;
}; /* DecisionEngineOld class */
JustificationStrategy::JustificationStrategy(context::Context* c,
context::UserContext* u,
- prop::SkolemDefManager* skdm)
- : d_context(c),
- d_cnfStream(nullptr),
- d_satSolver(nullptr),
+ prop::SkolemDefManager* skdm,
+ ResourceManager* rm)
+ : DecisionEngine(c, rm),
d_skdm(skdm),
d_assertions(
u,
d_lastDecisionLit(c),
d_currStatusDec(false),
d_useRlvOrder(options::jhRlvOrder()),
+ d_decisionStopOnly(options::decisionMode()
+ == options::DecisionMode::STOPONLY),
d_jhSkMode(options::jhSkolemMode()),
d_jhSkRlvMode(options::jhSkolemRlvMode())
{
}
-void JustificationStrategy::finishInit(CDCLTSatSolverInterface* ss,
- CnfStream* cs)
-{
- d_satSolver = ss;
- d_cnfStream = cs;
-}
-
void JustificationStrategy::presolve()
{
d_lastDecisionLit = Node::null();
d_stack.clear();
}
-SatLiteral JustificationStrategy::getNext(bool& stopSearch)
+SatLiteral JustificationStrategy::getNextInternal(bool& stopSearch)
{
// ensure we have an assertion
if (!refreshCurrentAssertion())
d_lastDecisionLit = next.first;
// record that we made a decision
d_currStatusDec = true;
+ if (d_decisionStopOnly)
+ {
+ // only doing stop-only, return undefSatLiteral.
+ return undefSatLiteral;
+ }
return lastChildVal == SAT_VALUE_FALSE ? ~nsl : nsl;
}
else
#include "context/cdinsert_hashmap.h"
#include "context/cdo.h"
#include "decision/assertion_list.h"
+#include "decision/decision_engine.h"
#include "decision/justify_info.h"
#include "decision/justify_stack.h"
#include "decision/justify_stats.h"
* definition, and Q alone would have sufficed to show the input formula
* was satisfied.
*/
-class JustificationStrategy
+class JustificationStrategy : public DecisionEngine
{
public:
/** Constructor */
JustificationStrategy(context::Context* c,
context::UserContext* u,
- prop::SkolemDefManager* skdm);
-
- /** Finish initialize */
- void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
+ prop::SkolemDefManager* skdm,
+ ResourceManager* rm);
/** Presolve, called at the beginning of each check-sat call */
- void presolve();
+ void presolve() override;
/**
* Gets the next decision based on the current assertion to satisfy. This
* @param stopSearch Set to true if we can stop the search
* @return The next SAT literal to decide on.
*/
- prop::SatLiteral getNext(bool& stopSearch);
+ prop::SatLiteral getNextInternal(bool& stopSearch) override;
/**
* Are we finished assigning values to literals?
* @return true if and only if all relevant input assertions are already
* propositionally satisfied by the current assignment.
*/
- bool isDone();
+ bool isDone() override;
/**
* Notify this class that assertion is an (input) assertion, not corresponding
* to a skolem definition.
*/
- void addAssertion(TNode assertion);
+ void addAssertion(TNode assertion) override;
/**
* Notify this class that lem is the skolem definition for skolem, which is
* a part of the current assertions.
*/
- void addSkolemDefinition(TNode lem, TNode skolem);
+ void addSkolemDefinition(TNode lem, TNode skolem) override;
/**
* Notify this class that literal n has been asserted. This is triggered when
* n is sent to TheoryEngine. This activates skolem definitions for skolems
* k that occur in n.
*/
- void notifyAsserted(TNode n);
+ void notifyAsserted(TNode n) override;
private:
/**
static bool isTheoryLiteral(TNode n);
/** Is n a theory atom? */
static bool isTheoryAtom(TNode n);
- /** Pointer to the SAT context */
- context::Context* d_context;
- /** Pointer to the CNF stream */
- prop::CnfStream* d_cnfStream;
- /** Pointer to the SAT solver */
- prop::CDCLTSatSolverInterface* d_satSolver;
/** Pointer to the skolem definition manager */
prop::SkolemDefManager* d_skdm;
/** The assertions, which are user-context dependent. */
//------------------------------------ options
/** using relevancy order */
bool d_useRlvOrder;
+ /** using stop only */
+ bool d_decisionStopOnly;
/** skolem mode */
options::JutificationSkolemMode d_jhSkMode;
/** skolem relevancy mode */
[[option.mode.JUSTIFICATION]]
name = "justification"
help = "An ATGP-inspired justification heuristic."
- [[option.mode.RELEVANCY]]
+ [[option.mode.STOPONLY]]
name = "justification-stoponly"
help = "Use the justification heuristic only to stop early, not for decisions."
This defines a new option that is accessible via
`d_options.{module.id}.decisionMode` and stores an automatically generated mode
`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and
-`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also
+`STOPONLY`. From the outside, it can be set by `--decision=internal`, but also
with `--decision-mode=justification`, and similarly from an SMT-LIB input with
`(set-option :decision internal)` and `(set-option :decision-mode
justification)`. The command-line help for this option looks as follows:
long = "decision=MODE"
type = "DecisionMode"
default = "INTERNAL"
- predicates = ["setDecisionModeStopOnly"]
help = "choose decision mode, see --decision=help"
help_mode = "Decision modes."
[[option.mode.INTERNAL]]
[[option.mode.JUSTIFICATION]]
name = "justification"
help = "An ATGP-inspired justification heuristic."
+[[option.mode.STOPONLY]]
+ name = "stoponly"
+ help = "Use the justification heuristic only to stop early, not for decisions."
[[option.mode.JUSTIFICATION_OLD]]
name = "justification-old"
help = "Older implementation of an ATGP-inspired justification heuristic."
-[[option.mode.RELEVANCY]]
- name = "justification-stoponly"
- help = "Use the justification heuristic only to stop early, not for decisions."
-
-[[option]]
- name = "decisionStopOnly"
- category = "undocumented"
- type = "bool"
+[[option.mode.STOPONLY_OLD]]
+ name = "stoponly-old"
+ help = "Use the old implementation of justification heuristic only to stop early, not for decisions."
[[option]]
name = "decisionThreshold"
}
}
-// decision/options_handlers.h
-void OptionsHandler::setDecisionModeStopOnly(const std::string& option,
- const std::string& flag,
- DecisionMode m)
-{
- d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY);
-}
-
void OptionsHandler::setProduceAssertions(const std::string& option,
const std::string& flag,
bool value)
const std::string& flag,
const std::string& optarg);
- // decision/options_handlers.h
- void setDecisionModeStopOnly(const std::string& option,
- const std::string& flag,
- DecisionMode m);
-
/**
* Throws a ModalException if this option is being set after final
* initialization.
#include "base/check.h"
#include "base/output.h"
-#include "decision/decision_engine.h"
#include "decision/decision_engine_old.h"
+#include "decision/justification_strategy.h"
#include "options/base_options.h"
#include "options/decision_options.h"
#include "options/main_options.h"
context::UserContext* userContext = d_env.getUserContext();
ResourceManager* rm = d_env.getResourceManager();
- d_decisionEngine.reset(
- new decision::DecisionEngine(satContext, userContext, d_skdm.get(), rm));
+ options::DecisionMode dmode = options::decisionMode();
+ if (dmode == options::DecisionMode::JUSTIFICATION
+ || dmode == options::DecisionMode::STOPONLY)
+ {
+ d_decisionEngine.reset(new decision::JustificationStrategy(
+ satContext, userContext, d_skdm.get(), rm));
+ }
+ else if (dmode == options::DecisionMode::JUSTIFICATION_OLD
+ || dmode == options::DecisionMode::STOPONLY_OLD)
+ {
+ d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm));
+ }
+ else
+ {
+ d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm));
+ }
d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
if(stopSearch) {
Trace("decision") << " *** Decision Engine stopped search *** " << std::endl;
}
- return options::decisionStopOnly() ? undefSatLiteral : ret;
+ return ret;
}
bool TheoryProxy::theoryNeedCheck() const {
? true
: false);
- Trace("smt") << "setting decision mode to " << decMode << std::endl;
opts.decision.decisionMode = decMode;
- opts.decision.decisionStopOnly = stoponly;
+ if (stoponly)
+ {
+ if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
+ {
+ opts.decision.decisionMode = options::DecisionMode::STOPONLY;
+ }
+ else
+ {
+ Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL);
+ }
+ }
+ Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
+ << std::endl;
}
if (options::incrementalSolving())
{
projects / cvc5.git / commitdiff