diff options
Diffstat (limited to 'src/theory')
| -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 |
4 files changed, 110 insertions, 10 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 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(). */ |