From f3a5261af19230d40ddc360fa5220ee03ab8d7f5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Apr 2022 20:36:51 -0500 Subject: [PATCH] Updates to zero level learner (#8597) Now tracks learned literals for all types. Unifies the output of `-o learned-literals`. Followup PRs will add the deep restart feature, which configures which kind of learned literals can be used when restarting. --- .../preprocessing_pass_context.cpp | 30 +-- src/prop/prop_engine.cpp | 17 +- src/prop/prop_engine.h | 13 +- src/prop/theory_proxy.cpp | 28 ++- src/prop/theory_proxy.h | 11 +- src/prop/zero_level_learner.cpp | 223 +++++++++++++----- src/prop/zero_level_learner.h | 57 +++-- src/smt/solver_engine.cpp | 2 +- 8 files changed, 270 insertions(+), 111 deletions(-) diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 52e28f50a..d14113f0a 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -16,8 +16,8 @@ #include "preprocessing/preprocessing_pass_context.h" #include "expr/node_algorithm.h" -#include "expr/skolem_manager.h" #include "options/base_options.h" +#include "prop/prop_engine.h" #include "smt/env.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -83,23 +83,11 @@ std::vector PreprocessingPassContext::getLearnedLiterals() const return d_llm.getLearnedLiterals(); } -void PreprocessingPassContext::printSubstitution(const Node& lhs, - const Node& rhs) const -{ - Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs)); - output(OutputTag::LEARNED_LITS) - << "(learned-lit " << eq << " :preprocess-subs)" << std::endl; - output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl; -} - void PreprocessingPassContext::addSubstitution(const Node& lhs, const Node& rhs, ProofGenerator* pg) { - if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS)) - { - printSubstitution(lhs, rhs); - } + d_propEngine->notifyTopLevelSubstitution(lhs, rhs); d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg); } @@ -108,23 +96,17 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, PfRule id, const std::vector& args) { - if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS)) - { - printSubstitution(lhs, rhs); - } + d_propEngine->notifyTopLevelSubstitution(lhs, rhs); d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); } void PreprocessingPassContext::addSubstitutions( theory::TrustSubstitutionMap& tm) { - if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS)) + std::unordered_map subs = tm.get().getSubstitutions(); + for (const std::pair& s : subs) { - std::unordered_map subs = tm.get().getSubstitutions(); - for (const std::pair& s : subs) - { - printSubstitution(s.first, s.second); - } + d_propEngine->notifyTopLevelSubstitution(s.first, s.second); } d_env.getTopLevelSubstitutions().addSubstitutions(tm); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 53f6877fe..eebd54492 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -22,6 +22,7 @@ #include "base/check.h" #include "base/output.h" #include "decision/justification_strategy.h" +#include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -165,6 +166,17 @@ TrustNode PropEngine::removeItes(TNode node, return d_theoryProxy->removeItes(node, newLemmas); } +void PropEngine::notifyTopLevelSubstitution(const Node& lhs, + const Node& rhs) const +{ + d_theoryProxy->notifyTopLevelSubstitution(lhs, rhs); + if (isOutputOn(OutputTag::SUBS)) + { + Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs)); + output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl; + } +} + void PropEngine::assertInputFormulas( const std::vector& assertions, std::unordered_map& skolemMap) @@ -693,9 +705,10 @@ std::shared_ptr PropEngine::getRefutation() return cdp.getProofFor(fnode); } -std::vector PropEngine::getLearnedZeroLevelLiterals() const +std::vector PropEngine::getLearnedZeroLevelLiterals( + modes::LearnedLitType ltype) const { - return d_theoryProxy->getLearnedZeroLevelLiterals(); + return d_theoryProxy->getLearnedZeroLevelLiterals(ltype); } } // namespace prop diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f69da4387..be4306934 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -20,6 +20,7 @@ #ifndef CVC5__PROP_ENGINE_H #define CVC5__PROP_ENGINE_H +#include "api/cpp/cvc5_types.h" #include "context/cdlist.h" #include "expr/node.h" #include "proof/proof.h" @@ -99,6 +100,13 @@ class PropEngine : protected EnvObj */ TrustNode removeItes(TNode node, std::vector& ppLemmas); + /** + * Notify that lhs was substituted by rhs during preprocessing. This impacts + * the tracked learned literals and output traces. + * @param lhs The left-hand side of the substitution + * @param rhs The right-hand side of the substitution + */ + void notifyTopLevelSubstitution(const Node& lhs, const Node& rhs) const; /** * Converts the given formulas to CNF and assert the CNF to the SAT solver. * These formulas are asserted permanently for the current context. @@ -301,8 +309,9 @@ class PropEngine : protected EnvObj /** Return the prop engine proof for assumption-based unsat cores. */ std::shared_ptr getRefutation(); - /** Get the zero-level assertions */ - std::vector getLearnedZeroLevelLiterals() const; + /** Get the zero-level assertions of the given type */ + std::vector getLearnedZeroLevelLiterals( + modes::LearnedLitType ltype) const; private: /** Dump out the satisfying assignment (after SAT result) */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index aa439f6cc..abd37695c 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -52,11 +52,11 @@ TheoryProxy::TheoryProxy(Env& env, d_skdm(skdm), d_zll(nullptr) { - bool trackTopLevelLearned = isOutputOn(OutputTag::LEARNED_LITS) - || options().smt.produceLearnedLiterals; - if (trackTopLevelLearned) + bool trackZeroLevel = isOutputOn(OutputTag::LEARNED_LITS) + || options().smt.produceLearnedLiterals; + if (trackZeroLevel) { - d_zll = std::make_unique(env, propEngine); + d_zll = std::make_unique(env, theoryEngine); } } @@ -72,6 +72,15 @@ void TheoryProxy::presolve() d_theoryEngine->presolve(); } +void TheoryProxy::notifyTopLevelSubstitution(const Node& lhs, + const Node& rhs) const +{ + if (d_zll != nullptr) + { + d_zll->notifyTopLevelSubstitution(lhs, rhs); + } +} + void TheoryProxy::notifyInputFormulas( const std::vector& assertions, std::unordered_map& skolemMap) @@ -100,7 +109,7 @@ void TheoryProxy::notifyInputFormulas( // determine what is learnable if (d_zll != nullptr) { - d_zll->notifyInputFormulas(assertions, skolemMap); + d_zll->notifyInputFormulas(assertions); } } @@ -127,8 +136,8 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { d_queue.pop(); if (d_zll != nullptr) { - // check if this corresponds to a zero-level asserted literal - d_zll->notifyAsserted(assertion); + int32_t alevel = d_propEngine->getDecisionLevel(assertion); + d_zll->notifyAsserted(assertion, alevel); } // now, assert to theory engine d_theoryEngine->assertFact(assertion); @@ -302,11 +311,12 @@ void TheoryProxy::getSkolems(TNode node, void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } -std::vector TheoryProxy::getLearnedZeroLevelLiterals() const +std::vector TheoryProxy::getLearnedZeroLevelLiterals( + modes::LearnedLitType ltype) const { if (d_zll != nullptr) { - return d_zll->getLearnedZeroLevelLiterals(); + return d_zll->getLearnedZeroLevelLiterals(ltype); } return {}; } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 8274e24be..8d0270fa4 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -24,6 +24,7 @@ #include "context/cdqueue.h" #include "expr/node.h" #include "proof/trust_node.h" +#include "prop/learned_db.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" #include "smt/env_obj.h" @@ -69,6 +70,13 @@ class TheoryProxy : protected EnvObj, public Registrar /** Presolve, which calls presolve for the modules managed by this class */ void presolve(); + /** + * Notify that lhs was substituted by rhs during preprocessing. This impacts + * the tracked learned literals and output traces. + * @param lhs The left-hand side of the substitution + * @param rhs The right-hand side of the substitution + */ + void notifyTopLevelSubstitution(const Node& lhs, const Node& rhs) const; /** * Notifies this module of the input assertions. * @param assertion The preprocessed input assertions, @@ -169,7 +177,8 @@ class TheoryProxy : protected EnvObj, public Registrar void preRegister(Node n) override; /** Get the zero-level assertions */ - std::vector getLearnedZeroLevelLiterals() const; + std::vector getLearnedZeroLevelLiterals( + modes::LearnedLitType ltype) const; private: /** The prop engine we are using. */ diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index cb37c6abc..a98136ca8 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -19,31 +19,34 @@ #include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/smt_options.h" -#include "prop/prop_engine.h" #include "smt/env.h" #include "smt/smt_statistics_registry.h" +#include "theory/theory_engine.h" #include "theory/trust_substitutions.h" namespace cvc5::internal { namespace prop { -ZeroLevelLearner::ZeroLevelLearner(Env& env, PropEngine* propEngine) +ZeroLevelLearner::ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine) : EnvObj(env), - d_propEngine(propEngine), + d_theoryEngine(theoryEngine), d_levelZeroAsserts(userContext()), - d_levelZeroAssertsLearned(userContext()), + d_ldb(userContext()), d_nonZeroAssert(context(), false), d_ppnAtoms(userContext()), - d_pplAtoms(userContext()), + d_ppnTerms(userContext()), + d_ppnSyms(userContext()), d_assertNoLearnCount(0) { + // get the learned types + d_learnedTypes.insert(modes::LearnedLitType::INPUT); } ZeroLevelLearner::~ZeroLevelLearner() {} void ZeroLevelLearner::getAtoms(TNode a, std::unordered_set& visited, - NodeSet& ppLits) + std::unordered_set& atoms) { std::vector visit; TNode cur; @@ -60,17 +63,24 @@ void ZeroLevelLearner::getAtoms(TNode a, visit.insert(visit.end(), cur.begin(), cur.end()); continue; } - ppLits.insert(cur); + atoms.insert(cur); } } while (!visit.empty()); } -void ZeroLevelLearner::notifyInputFormulas( - const std::vector& assertions, - const std::unordered_map& skolemMap) +void ZeroLevelLearner::notifyTopLevelSubstitution(const Node& lhs, + const Node& rhs) +{ + // process as a preprocess solved learned literal. + Node eq = lhs.eqNode(rhs); + processLearnedLiteral(eq, modes::LearnedLitType::PREPROCESS_SOLVED); +} + +void ZeroLevelLearner::notifyInputFormulas(const std::vector& assertions) { - d_assertNoLearnCount = 0; std::unordered_set visited; + std::unordered_set visitedWithinAtom; + std::unordered_set inputSymbols; // We consider top level literals of assertions, including those occurring // as children of AND to be the preprocessed learned literals only, and not // the literals tracked by the preprocessor @@ -94,87 +104,194 @@ void ZeroLevelLearner::notifyInputFormulas( { continue; } + // we mark that we visited this visited.insert(atom); - d_pplAtoms.insert(atom); - } - if (isOutputOn(OutputTag::LEARNED_LITS)) - { // output learned literals from preprocessing - for (const Node& lit : d_pplAtoms) - { - output(OutputTag::LEARNED_LITS) - << "(learned-lit " << SkolemManager::getOriginalForm(lit) - << " :preprocess)" << std::endl; - } + processLearnedLiteral(lit, modes::LearnedLitType::PREPROCESS); + // also get its symbols + expr::getSymbols(atom, inputSymbols, visitedWithinAtom); + // remember we've seen it + d_levelZeroAsserts.insert(lit); } // Compute the set of literals in the preprocessed assertions + std::unordered_set inputAtoms; for (const Node& a : assertions) { - getAtoms(a, visited, d_ppnAtoms); + getAtoms(a, visited, inputAtoms); + } + for (const Node& a : inputAtoms) + { + d_ppnAtoms.insert(a); + // also get its symbols + expr::getSymbols(a, inputSymbols, visitedWithinAtom); + } + for (const TNode& t : visitedWithinAtom) + { + d_ppnTerms.insert(t); + } + for (const Node& s : inputSymbols) + { + d_ppnSyms.insert(s); } Trace("level-zero") << "Preprocess status:" << std::endl; Trace("level-zero") << "#Non-learned lits = " << d_ppnAtoms.size() << std::endl; - Trace("level-zero") << "#Learned lits = " << d_pplAtoms.size() << std::endl; - Trace("level-zero") << "#Top level subs = " + Trace("level-zero") << "#Symbols = " << d_ppnSyms.size() << std::endl; + Trace("level-zero") << "#Subterms = " << d_ppnTerms.size() << std::endl; + Trace("level-zero") << "#Current top level subs = " << d_env.getTopLevelSubstitutions().get().size() << std::endl; + Trace("level-zero") << d_ldb.toStringDebug(); } -void ZeroLevelLearner::notifyAsserted(TNode assertion) +bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel) { // check if at level zero if (d_nonZeroAssert.get()) { + // already not at level zero, skip + d_assertNoLearnCount++; + } + else if (alevel != 0) + { + Trace("level-zero-dec") << "First non-zero: " << assertion << std::endl; + d_nonZeroAssert = true; d_assertNoLearnCount++; } else if (d_levelZeroAsserts.find(assertion) == d_levelZeroAsserts.end()) { - int32_t alevel = d_propEngine->getDecisionLevel(assertion); - if (alevel == 0) + // remember we've processed this + d_levelZeroAsserts.insert(assertion); + // process what we should do with the learned literal + modes::LearnedLitType ltype = computeLearnedLiteralType(assertion); + processLearnedLiteral(assertion, ltype); + return true; + } + return true; +} + +modes::LearnedLitType ZeroLevelLearner::computeLearnedLiteralType( + const Node& lit) +{ + // literal was learned, determine its type + TNode aatom = lit.getKind() == kind::NOT ? lit[0] : lit; + bool internal = d_ppnAtoms.find(aatom) == d_ppnAtoms.end(); + modes::LearnedLitType ltype = + internal ? modes::LearnedLitType::INTERNAL : modes::LearnedLitType::INPUT; + // compute if solvable + if (internal) + { + Subs ss; + if (getSolved(lit, ss)) { - TNode aatom = assertion.getKind() == kind::NOT ? assertion[0] : assertion; - bool learnable = d_ppnAtoms.find(aatom) != d_ppnAtoms.end(); - Trace("level-zero-assert") - << "Level zero assert: " << assertion << ", learnable=" << learnable - << ", already learned=" - << (d_pplAtoms.find(aatom) != d_pplAtoms.end()) << std::endl; - d_levelZeroAsserts.insert(assertion); - if (learnable) + // if we solved for any variable from input, we are SOLVABLE. + for (const Node& v : ss.d_vars) { - d_assertNoLearnCount = 0; - d_levelZeroAssertsLearned.insert(assertion); - Trace("level-zero-assert") - << "#learned now " << d_levelZeroAssertsLearned.size() << std::endl; - if (isOutputOn(OutputTag::LEARNED_LITS)) + if (d_ppnSyms.find(v) == d_ppnSyms.end()) { - // get the original form so that internally generated variables - // are mapped back to their original form - output(OutputTag::LEARNED_LITS) - << "(learned-lit " << SkolemManager::getOriginalForm(assertion) - << ")" << std::endl; + Trace("level-zero-assert") << "...solvable due to " << v << std::endl; + ltype = modes::LearnedLitType::SOLVABLE; + break; } - return; } } - else + if (ltype != modes::LearnedLitType::SOLVABLE) { - d_nonZeroAssert = true; + // maybe a constant prop? + if (lit.getKind() == kind::EQUAL) + { + for (size_t i = 0; i < 2; i++) + { + if (lit[i].isConst() + && d_ppnTerms.find(lit[1 - i]) != d_ppnTerms.end()) + { + ltype = modes::LearnedLitType::CONSTANT_PROP; + break; + } + } + } } - d_assertNoLearnCount++; + } + Trace("level-zero-assert") + << "Level zero assert: " << lit << ", type=" << ltype << std::endl; + return ltype; +} + +void ZeroLevelLearner::processLearnedLiteral(const Node& lit, + modes::LearnedLitType ltype) +{ + // add to the database + d_ldb.addLearnedLiteral(lit, ltype); + // reset the counter for deep restart if the literal was learnable + if (isLearnable(ltype)) + { + d_assertNoLearnCount = 0; + } + // print to stream + if (isOutputOn(OutputTag::LEARNED_LITS)) + { + // get the original form so that internally generated variables + // are mapped back to their original form + output(OutputTag::LEARNED_LITS) + << "(learned-lit " << SkolemManager::getOriginalForm(lit); + if (ltype != modes::LearnedLitType::INPUT) + { + std::stringstream tss; + tss << ltype; + std::string ltstr = tss.str(); + std::transform( + ltstr.begin(), ltstr.end(), ltstr.begin(), [](unsigned char c) { + return std::tolower(c); + }); + output(OutputTag::LEARNED_LITS) << " :" << ltstr; + } + output(OutputTag::LEARNED_LITS) << ")" << std::endl; } } -std::vector ZeroLevelLearner::getLearnedZeroLevelLiterals() const +std::vector ZeroLevelLearner::getLearnedZeroLevelLiterals( + modes::LearnedLitType ltype) const { - std::vector ret; - for (const Node& n : d_levelZeroAssertsLearned) + std::vector ret = d_ldb.getLearnedLiterals(ltype); + if (TraceIsOn("level-zero")) { - ret.push_back(n); + if (!ret.empty()) + { + Trace("level-zero") << "...learned #literals (" << ltype + << ") = " << ret.size() << std::endl; + } } return ret; } +bool ZeroLevelLearner::isLearnable(modes::LearnedLitType ltype) const +{ + return d_learnedTypes.find(ltype) != d_learnedTypes.end(); +} + +bool ZeroLevelLearner::getSolved(const Node& lit, Subs& subs) +{ + context::Context dummyContext; + theory::TrustSubstitutionMap subsOut(&dummyContext); + TrustNode tlit = TrustNode::mkTrustLemma(lit); + theory::Theory::PPAssertStatus status = d_theoryEngine->solve(tlit, subsOut); + if (status == theory::Theory::PP_ASSERT_STATUS_SOLVED) + { + Trace("level-zero-debug") << lit << " is solvable" << std::endl; + // extract the substitution + std::unordered_map ss = subsOut.get().getSubstitutions(); + for (const std::pair& s : ss) + { + subs.add(s.first, s.second); + Trace("level-zero-debug") + << " subs: " << s.first << " -> " << s.second << std::endl; + } + return true; + } + Trace("level-zero-debug") << lit << " is not solvable" << std::endl; + return false; +} + } // namespace prop } // namespace cvc5::internal diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h index dcb27d8e9..e61d41584 100644 --- a/src/prop/zero_level_learner.h +++ b/src/prop/zero_level_learner.h @@ -23,12 +23,15 @@ #include "context/cdhashset.h" #include "context/cdo.h" #include "expr/node.h" +#include "expr/subs.h" +#include "prop/learned_db.h" #include "smt/env_obj.h" namespace cvc5::internal { -namespace prop { -class PropEngine; +class TheoryEngine; + +namespace prop { /** * The module for processing literals that are learned at decision level zero. @@ -45,45 +48,61 @@ class ZeroLevelLearner : protected EnvObj using NodeSet = context::CDHashSet; public: - ZeroLevelLearner(Env& env, PropEngine* propEngine); + ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine); ~ZeroLevelLearner(); - void notifyInputFormulas(const std::vector& assertions, - const std::unordered_map& skolemMap); + void notifyTopLevelSubstitution(const Node& lhs, const Node& rhs); + /** Notify the input formulas and the skolem map */ + void notifyInputFormulas(const std::vector& assertions); /** - * Notify the given literal was asserted + * Notify the given literal was asserted at the given assertion level. + * Return false if a deep restart is requested. */ - void notifyAsserted(TNode assertion); + bool notifyAsserted(TNode assertion, int32_t alevel); /** Get the zero-level assertions */ - std::vector getLearnedZeroLevelLiterals() const; + std::vector getLearnedZeroLevelLiterals( + modes::LearnedLitType ltype) const; private: static void getAtoms(TNode a, std::unordered_set& visited, - NodeSet& ppLits); - - /** The prop engine we are using. */ - PropEngine* d_propEngine; + std::unordered_set& atoms); + /** Process learned literal */ + void processLearnedLiteral(const Node& lit, modes::LearnedLitType ltype); + /** compute type for learned literal */ + modes::LearnedLitType computeLearnedLiteralType(const Node& lit); + /** is learnable based on the value of options */ + bool isLearnable(modes::LearnedLitType ltype) const; + /** get solved */ + bool getSolved(const Node& lit, Subs& subs); + + /** The theory engine we are using */ + TheoryEngine* d_theoryEngine; /** Set of literals that hold at level 0 */ NodeSet d_levelZeroAsserts; - /** Set of learnable literals that hold at level 0 */ - NodeSet d_levelZeroAssertsLearned; + /** What we have learned */ + LearnedDb d_ldb; /** Whether we have seen an assertion level > 0 */ context::CDO d_nonZeroAssert; - /** Preprocessed literals that are not learned */ + /** + * Atoms of literals from the input formula that were not learned at + * preprocess. + */ NodeSet d_ppnAtoms; - - /** Already learned TEMPORARY */ - NodeSet d_pplAtoms; - + /** Subterms of the above atoms. */ + NodeSet d_ppnTerms; + /** Symbols in the above atoms. */ + NodeSet d_ppnSyms; /** Current counter of assertions */ size_t d_assertNoLearnCount; + /** learnable learned literal types (for deep restart), based on option */ + std::unordered_set d_learnedTypes; }; /* class ZeroLevelLearner */ } // namespace prop diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 744eb3b42..b763adc54 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1254,7 +1254,7 @@ std::vector SolverEngine::getLearnedLiterals() // although other modes could use the preprocessor PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - return pe->getLearnedZeroLevelLiterals(); + return pe->getLearnedZeroLevelLiterals(modes::LearnedLitType::INPUT); } void SolverEngine::checkProof() -- 2.30.2