diff options
Diffstat (limited to 'src/theory/relevance_manager.cpp')
-rw-r--r-- | src/theory/relevance_manager.cpp | 56 |
1 files changed, 53 insertions, 3 deletions
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 |