This also introduces the produceDifficulty option which is analogous to produceUnsatCores.
It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.
[[option.mode.ASSUMPTIONS]]
name = "assumptions"
help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
+[[option.mode.PP_ONLY]]
+ name = "pp-only"
+ help = "Not producing unsat cores, but tracking proofs of preprocessing (internal only)."
[[option]]
name = "minimalUnsatCores"
default = "false"
help = "turn on unsat assumptions generation"
+[[option]]
+ name = "produceDifficulty"
+ category = "regular"
+ long = "produce-difficulty"
+ type = "bool"
+ default = "false"
+ help = "enable tracking of difficulty."
+
[[option]]
name = "difficultyMode"
category = "regular"
{
return d_proofNodeManager != nullptr
&& (!d_options.smt.unsatCores
- || d_options.smt.unsatCoresMode
- != options::UnsatCoresMode::ASSUMPTIONS);
+ || (d_options.smt.unsatCoresMode
+ != options::UnsatCoresMode::ASSUMPTIONS
+ && d_options.smt.unsatCoresMode
+ != options::UnsatCoresMode::PP_ONLY));
}
bool Env::isTheoryProofProducing() const
{
opts.driver.dumpUnsatCores = true;
}
+ if (opts.smt.produceDifficulty)
+ {
+ if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
+ {
+ opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY;
+ }
+ opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
+ }
if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
|| opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
|| opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
bool SetDefaults::safeUnsatCores(const Options& opts) const
{
// whether we want to force safe unsat cores, i.e., if we are in the default
- // ASSUMPTIONS mode, since other ones are experimental
- return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
+ // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental
+ return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS
+ || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY;
}
bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
#include <sstream>
+#include "options/smt_options.h"
+#include "smt/env.h"
+
using namespace cvc5::kind;
namespace cvc5 {
RelevanceManager::RelevanceManager(context::UserContext* userContext,
Valuation val)
- : d_val(val), d_input(userContext), d_computed(false), d_success(false)
+ : d_val(val),
+ d_input(userContext),
+ d_computed(false),
+ d_success(false),
+ d_trackRSetExp(false),
+ d_miniscopeTopLevel(true)
{
+ if (options::produceDifficulty())
+ {
+ d_dman.reset(new DifficultyManager(userContext, val));
+ d_trackRSetExp = true;
+ // we cannot miniscope AND at the top level, since we need to
+ // preserve the exact form of preprocessed assertions so the dependencies
+ // are tracked.
+ d_miniscopeTopLevel = false;
+ }
}
void RelevanceManager::notifyPreprocessedAssertions(
std::vector<Node> toProcess;
for (const Node& a : assertions)
{
- if (a.getKind() == AND)
+ if (d_miniscopeTopLevel && a.getKind() == AND)
{
// split top-level AND
for (const Node& ac : a)
while (i < toProcess.size())
{
Node a = toProcess[i];
- if (a.getKind() == AND)
+ if (d_miniscopeTopLevel && a.getKind() == AND)
{
+ // difficulty tracking disables miniscoping of AND
+ Assert(d_dman == nullptr);
// split AND
for (const Node& ac : a)
{
{
d_computed = true;
d_rset.clear();
+ d_rsetExp.clear();
Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
std::unordered_map<TNode, int> cache;
for (const Node& node: d_input)
{
ret = value ? 1 : -1;
d_rset.insert(cur);
+ if (d_trackRSetExp)
+ {
+ d_rsetExp[cur] = n;
+ }
}
cache[cur] = ret;
}
return d_rset;
}
+void RelevanceManager::notifyLemma(Node n)
+{
+ if (d_dman != nullptr)
+ {
+ // ensure we know which literals are relevant, and why
+ computeRelevance();
+ d_dman->notifyLemma(d_rsetExp, n);
+ }
+}
+
+void RelevanceManager::notifyCandidateModel(TheoryModel* m)
+{
+ if (d_dman != nullptr)
+ {
+ d_dman->notifyCandidateModel(d_input, m);
+ }
+}
+
+void RelevanceManager::getDifficultyMap(std::map<Node, Node>& dmap)
+{
+ if (d_dman != nullptr)
+ {
+ d_dman->getDifficultyMap(dmap);
+ }
+}
+
} // namespace theory
} // namespace cvc5
#include "context/cdlist.h"
#include "expr/node.h"
+#include "theory/difficulty_manager.h"
#include "theory/valuation.h"
namespace cvc5 {
namespace theory {
+class TheoryModel;
+
/**
* This class manages queries related to relevance of asserted literals.
* In particular, note the following definition:
* if not already done so. This call is valid during a full effort check in
* TheoryEngine, or after TheoryEngine has terminated with "sat". This method
* sets the flag success to false if we failed to compute relevant
- * assertions, which can occur if
+ * assertions, which occurs if the values from the SAT solver do not satisfy
+ * the assertions we are notified of. This should never happen.
*
* The value of this return is only valid if success was not updated to false.
*/
const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
+ /** Notify lemma, for difficulty measurements */
+ void notifyLemma(Node n);
+ /** Notify that m is a (candidate) model, for difficulty measurements */
+ void notifyCandidateModel(TheoryModel* m);
+ /**
+ * Get difficulty map
+ */
+ void getDifficultyMap(std::map<Node, Node>& dmap);
private:
/**
* aborts and indicates that all literals are relevant.
*/
bool d_success;
+ /** Are we tracking the sources of why a literal is relevant */
+ bool d_trackRSetExp;
+ /**
+ * Whether we have miniscoped top-level AND of assertions, which is done
+ * as an optimization. This is disabled if e.g. we are computing difficulty,
+ * which requires preserving the original form of the preprocessed
+ * assertions.
+ */
+ bool d_miniscopeTopLevel;
+ /**
+ * Map from the domain of d_rset to the assertion in d_input that is the
+ * reason why that literal is currently relevant.
+ */
+ std::map<TNode, TNode> d_rsetExp;
+ /** Difficulty module */
+ std::unique_ptr<DifficultyManager> d_dman;
};
} // namespace theory
<< options::tcMode() << " not supported";
}
// create the relevance filter if any option requires it
- if (options::relevanceFilter())
+ if (options::relevanceFilter() || options::produceDifficulty())
{
- d_relManager.reset(
- new RelevanceManager(userContext(), theory::Valuation(this)));
+ d_relManager.reset(new RelevanceManager(userContext(), Valuation(this)));
}
// initialize the quantifiers engine
d_quantEngine->check(Theory::EFFORT_LAST_CALL);
}
}
+ // notify the relevant manager
+ if (d_relManager != nullptr)
+ {
+ d_relManager->notifyCandidateModel(getModel());
+ }
if (!d_inConflict && !needCheck())
{
// We only mark that we are in "SAT mode". We build the model later only
return d_relManager->getRelevantAssertions(success);
}
+void TheoryEngine::getDifficultyMap(std::map<Node, Node>& dmap)
+{
+ Assert(d_relManager != nullptr);
+ d_relManager->getDifficultyMap(dmap);
+}
+
Node TheoryEngine::getModelValue(TNode var) {
if (var.isConst())
{
// If specified, we must add this lemma to the set of those that need to be
// justified, where note we pass all auxiliary lemmas in skAsserts as well,
// since these by extension must be justified as well.
- if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
+ if (d_relManager != nullptr)
{
std::vector<Node> skAsserts;
std::vector<Node> sks;
Node retLemma =
d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
- d_relManager->notifyPreprocessedAssertion(retLemma);
- d_relManager->notifyPreprocessedAssertions(skAsserts);
+ if (isLemmaPropertyNeedsJustify(p))
+ {
+ d_relManager->notifyPreprocessedAssertion(retLemma);
+ d_relManager->notifyPreprocessedAssertions(skAsserts);
+ }
+ d_relManager->notifyLemma(retLemma);
}
// Mark that we added some lemmas
*/
const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
+ /**
+ * Get difficulty map, which populates dmap, mapping preprocessed assertions
+ * to a value that estimates their difficulty for solving the current problem.
+ *
+ * For details, see theory/difficuly_manager.h.
+ */
+ void getDifficultyMap(std::map<Node, Node>& dmap);
+
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
projects / cvc5.git / commitdiff