diff options
-rw-r--r-- | src/options/smt_options.toml | 11 | ||||
-rw-r--r-- | src/smt/env.cpp | 6 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 13 | ||||
-rw-r--r-- | src/theory/relevance_manager.cpp | 56 | ||||
-rw-r--r-- | src/theory/relevance_manager.h | 30 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 26 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 8 |
7 files changed, 136 insertions, 14 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 7d0dab720..26af86ca2 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -196,6 +196,9 @@ name = "SMT Layer" [[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" @@ -221,6 +224,14 @@ name = "SMT Layer" 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" long = "difficulty-mode=MODE" diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 12e3c7520..f42a51dd0 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -86,8 +86,10 @@ bool Env::isSatProofProducing() const { 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 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 6e7939ff7..a226de807 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -81,6 +81,14 @@ void SetDefaults::setDefaultsPre(Options& opts) { 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) @@ -1142,8 +1150,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, 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, diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index 9746f4a22..e1a342178 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -17,6 +17,9 @@ #include <sstream> +#include "options/smt_options.h" +#include "smt/env.h" + using namespace cvc5::kind; namespace cvc5 { @@ -24,8 +27,22 @@ namespace theory { 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( @@ -35,7 +52,7 @@ 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) @@ -64,8 +81,10 @@ void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess) 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) { @@ -91,6 +110,7 @@ void RelevanceManager::computeRelevance() { 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) @@ -271,6 +291,10 @@ int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache) { ret = value ? 1 : -1; d_rset.insert(cur); + if (d_trackRSetExp) + { + d_rsetExp[cur] = n; + } } cache[cur] = ret; } @@ -326,5 +350,31 @@ const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions( 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 diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index 6c69861fd..f8cd8e1ee 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -23,11 +23,14 @@ #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: @@ -100,11 +103,20 @@ class RelevanceManager * 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: /** @@ -157,6 +169,22 @@ class RelevanceManager * 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 diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index be4b7dd76..54cfc9a6d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -155,10 +155,9 @@ void TheoryEngine::finishInit() << 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 @@ -530,6 +529,11 @@ void TheoryEngine::check(Theory::Effort effort) { 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 @@ -1140,6 +1144,12 @@ const std::unordered_set<TNode>& TheoryEngine::getRelevantAssertions( 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()) { @@ -1365,14 +1375,18 @@ void TheoryEngine::lemma(TrustNode tlemma, // 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 diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 496966149..4e8beb967 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -390,6 +390,14 @@ class TheoryEngine : protected EnvObj 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(). */ |