From 14155a4a00177a496eb48df0d50e38e2190908c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Jan 2022 17:28:02 -0600 Subject: [PATCH] Add -o learned-lits to output learned literals (#7934) Prints both literals learned during preprocessing, and during search. This feature was recently requested by Cetora. --- src/CMakeLists.txt | 2 + src/options/base_options.toml | 7 +- src/prop/prop_engine.cpp | 31 ++-- src/prop/prop_engine.h | 8 +- src/prop/theory_proxy.cpp | 62 ++++++- src/prop/theory_proxy.h | 28 +++- src/prop/zero_level_learner.cpp | 155 ++++++++++++++++++ src/prop/zero_level_learner.h | 93 +++++++++++ src/smt/preprocessor.cpp | 9 + src/smt/preprocessor.h | 2 + src/smt/smt_solver.cpp | 3 +- src/theory/substitutions.h | 2 + test/regress/CMakeLists.txt | 1 + .../regress0/printer/learned-lit-output.smt2 | 12 ++ 14 files changed, 386 insertions(+), 29 deletions(-) create mode 100644 src/prop/zero_level_learner.cpp create mode 100644 src/prop/zero_level_learner.h create mode 100644 test/regress/regress0/printer/learned-lit-output.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 830c70ca9..b17f82ac6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -277,6 +277,8 @@ libcvc5_add_sources( prop/skolem_def_manager.h prop/theory_proxy.cpp prop/theory_proxy.h + prop/zero_level_learner.cpp + prop/zero_level_learner.h smt/abduction_solver.cpp smt/abduction_solver.h smt/abstract_values.cpp diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 415dbf9f3..86ce22c6f 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -186,8 +186,13 @@ name = "Base" [[option.mode.RAW_BENCHMARK]] name = "raw-benchmark" help = "print the benchmark back on the output verbatim as it is processed" - description = "With ``-o raw_benchmark``, cvc5 prints the benchmark back just as it has been parsed." + description = "With ``-o raw-benchmark``, cvc5 prints the benchmark back just as it has been parsed." example-file = "regress0/datatypes/datatype-dump.cvc.smt2" +[[option.mode.LEARNED_LITS]] + name = "learned-lits" + help = "print input literals that hold globally" + description = "With ``-o learned-lits``, cvc5 prints input literals that it has learned to hold globally." + example-file = "regress0/printer/learned-lit-output.smt2" # Stores then enabled output tags. [[option]] diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index df18f9a85..b2b432723 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -175,28 +175,11 @@ TrustNode PropEngine::removeItes(TNode node, void PropEngine::assertInputFormulas( const std::vector& assertions, - std::unordered_map& skolemMap) + std::unordered_map& skolemMap, + const std::vector& ppl) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - // notify the theory engine of preprocessed assertions - d_theoryEngine->notifyPreprocessedAssertions(assertions); - // Now, notify the theory proxy of the assertions and skolem definitions. - // Notice we do this before asserting the formulas to the CNF stream below, - // since (preregistration) lemmas may occur during calls to assertInternal. - // These lemmas we want to be notified about after the theory proxy has - // been notified about all input assertions. - std::unordered_map::iterator it; - for (size_t i = 0, asize = assertions.size(); i < asize; i++) - { - // is the assertion a skolem definition? - it = skolemMap.find(i); - Node skolem; - if (it != skolemMap.end()) - { - skolem = it->second; - } - d_theoryProxy->notifyAssertion(assertions[i], skolem, false); - } + d_theoryProxy->notifyInputFormulas(assertions, skolemMap, ppl); for (const Node& node : assertions) { Debug("prop") << "assertFormula(" << node << ")" << std::endl; @@ -418,7 +401,8 @@ Result PropEngine::checkSat() { } Debug("prop") << "PropEngine::checkSat() => " << result << std::endl; - if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) { + if (result == SAT_VALUE_TRUE && d_theoryProxy->isIncomplete()) + { return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); } return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT); @@ -691,5 +675,10 @@ std::shared_ptr PropEngine::getRefutation() return cdp.getProofFor(fnode); } +const std::unordered_set& PropEngine::getLearnedZeroLevelLiterals() const +{ + return d_theoryProxy->getLearnedZeroLevelLiterals(); +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 53062ad92..0497c6738 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -31,7 +31,6 @@ namespace cvc5 { -class Env; class ResourceManager; class ProofNodeManager; class TheoryEngine; @@ -109,9 +108,11 @@ class PropEngine : protected EnvObj * @param skolemMap a map which says which skolem (if any) each assertion * corresponds to. For example, if (ite C (= k a) (= k b)) is the i^th * assertion, then skolemMap may contain the entry { i -> k }. + * @param ppl the list of preprocessed learned literals */ void assertInputFormulas(const std::vector& assertions, - std::unordered_map& skolemMap); + std::unordered_map& skolemMap, + const std::vector& ppl); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -293,6 +294,9 @@ class PropEngine : protected EnvObj /** Return the prop engine proof for assumption-based unsat cores. */ std::shared_ptr getRefutation(); + /** Get the zero-level assertions */ + const std::unordered_set& getLearnedZeroLevelLiterals() const; + private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 269921da2..58a7fb666 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,11 +19,14 @@ #include "context/context.h" #include "decision/decision_engine.h" +#include "expr/node_algorithm.h" +#include "options/base_options.h" #include "options/decision_options.h" #include "options/smt_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/skolem_def_manager.h" +#include "prop/zero_level_learner.h" #include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" @@ -44,10 +47,16 @@ TheoryProxy::TheoryProxy(Env& env, d_decisionEngine(decisionEngine), d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()), d_theoryEngine(theoryEngine), - d_queue(env.getContext()), + d_queue(context()), d_tpp(env, *theoryEngine), - d_skdm(skdm) + d_skdm(skdm), + d_zll(nullptr) { + bool trackTopLevelLearned = isOutputOn(OutputTag::LEARNED_LITS); + if (trackTopLevelLearned) + { + d_zll = std::make_unique(env, propEngine); + } } TheoryProxy::~TheoryProxy() { @@ -62,6 +71,39 @@ void TheoryProxy::presolve() d_theoryEngine->presolve(); } +void TheoryProxy::notifyInputFormulas( + const std::vector& assertions, + std::unordered_map& skolemMap, + const std::vector& ppl) +{ + // notify the theory engine of preprocessed assertions + d_theoryEngine->notifyPreprocessedAssertions(assertions); + // Now, notify the theory proxy of the assertions and skolem definitions. + // Notice we do this before asserting the formulas to the CNF stream below, + // since (preregistration) lemmas may occur during calls to assertInternal. + // These lemmas we want to be notified about after the theory proxy has + // been notified about all input assertions. + std::unordered_map::iterator it; + for (size_t i = 0, asize = assertions.size(); i < asize; i++) + { + // is the assertion a skolem definition? + it = skolemMap.find(i); + Node skolem; + if (it != skolemMap.end()) + { + skolem = it->second; + } + notifyAssertion(assertions[i], skolem, false); + } + + // the zero-level learner needs to be notified of the input assertions, to + // determine what is learnable + if (d_zll != nullptr) + { + d_zll->notifyInputFormulas(assertions, skolemMap, ppl); + } +} + void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma) { if (skolem.isNull()) @@ -83,6 +125,11 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { while (!d_queue.empty()) { TNode assertion = d_queue.front(); d_queue.pop(); + if (d_zll != nullptr) + { + // check if this corresponds to a zero-level asserted literal + d_zll->notifyAsserted(assertion); + } // now, assert to theory engine d_theoryEngine->assertFact(assertion); if (d_dmNeedsActiveDefs) @@ -177,6 +224,11 @@ bool TheoryProxy::theoryNeedCheck() const { return d_theoryEngine->needCheck(); } +bool TheoryProxy::isIncomplete() const +{ + return d_theoryEngine->isIncomplete(); +} + TNode TheoryProxy::getNode(SatLiteral lit) { return d_cnfStream->getNode(lit); } @@ -237,5 +289,11 @@ void TheoryProxy::getSkolems(TNode node, void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } +const std::unordered_set& TheoryProxy::getLearnedZeroLevelLiterals() const +{ + Assert(d_zll != nullptr); + return d_zll->getLearnedZeroLevelLiterals(); +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 8e998583d..85070b4c7 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -20,6 +20,7 @@ #include +#include "context/cdhashset.h" #include "context/cdqueue.h" #include "expr/node.h" #include "proof/trust_node.h" @@ -44,12 +45,15 @@ namespace prop { class PropEngine; class CnfStream; class SkolemDefManager; +class ZeroLevelLearner; /** * The proxy class that allows the SatSolver to communicate with the theories */ class TheoryProxy : protected EnvObj, public Registrar { + using NodeSet = context::CDHashSet; + public: TheoryProxy(Env& env, PropEngine* propEngine, @@ -65,6 +69,17 @@ class TheoryProxy : protected EnvObj, public Registrar /** Presolve, which calls presolve for the modules managed by this class */ void presolve(); + /** + * Notifies this module of the input assertions. + * @param assertion The preprocessed input assertions, + * @param skolemMap Map from indices in assertion to the Skolem they are + * the definition for + * @param ppl The preprocessed learned literals, that is, the literals that + * hold at top-level, as computed by the circuit propagator. + */ + void notifyInputFormulas(const std::vector& assertions, + std::unordered_map& skolemMap, + const std::vector& ppl); /** * Notify a lemma or input assertion, possibly corresponding to a skolem * definition. @@ -87,6 +102,9 @@ class TheoryProxy : protected EnvObj, public Registrar bool theoryNeedCheck() const; + /** Is incomplete */ + bool isIncomplete() const; + /** * Notifies of a new variable at a decision level. */ @@ -135,6 +153,9 @@ class TheoryProxy : protected EnvObj, public Registrar /** Preregister term */ void preRegister(Node n) override; + /** Get the zero-level assertions */ + const std::unordered_set& getLearnedZeroLevelLiterals() const; + private: /** The prop engine we are using. */ PropEngine* d_propEngine; @@ -168,10 +189,13 @@ class TheoryProxy : protected EnvObj, public Registrar /** The skolem definition manager */ SkolemDefManager* d_skdm; + + /** The zero level learner */ + std::unique_ptr d_zll; + }; /* class TheoryProxy */ } // namespace prop - } // namespace cvc5 -#endif /* CVC5__PROP__SAT_H */ +#endif diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp new file mode 100644 index 000000000..1b11662aa --- /dev/null +++ b/src/prop/zero_level_learner.cpp @@ -0,0 +1,155 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Learner for literals asserted at level zero. + */ +#include "prop/zero_level_learner.h" + +#include "context/context.h" +#include "expr/node_algorithm.h" +#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/trust_substitutions.h" + +namespace cvc5 { +namespace prop { + +ZeroLevelLearner::ZeroLevelLearner(Env& env, PropEngine* propEngine) + : EnvObj(env), + d_propEngine(propEngine), + d_nonZeroAssert(context(), false), + d_assertNoLearnCount(0) +{ +} + +ZeroLevelLearner::~ZeroLevelLearner() {} + +void ZeroLevelLearner::getAtoms(TNode a, + std::unordered_set& visited, + std::unordered_set& ppLits) +{ + std::vector visit; + TNode cur; + visit.push_back(a); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (expr::isBooleanConnective(cur)) + { + visit.insert(visit.end(), cur.begin(), cur.end()); + continue; + } + ppLits.insert(cur); + } + } while (!visit.empty()); +} + +void ZeroLevelLearner::notifyInputFormulas( + const std::vector& assertions, + std::unordered_map& skolemMap, + const std::vector& ppl) +{ + d_assertNoLearnCount = 0; + d_ppnAtoms.clear(); + // Copy the preprocessed assertions and skolem map information directly + // Also, compute the set of literals in the preprocessed assertions + std::unordered_set visited; + // learned literals and d_ppnAtoms are disjoint + for (const Node& lit : ppl) + { + TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit; + visited.insert(atom); + d_pplAtoms.insert(atom); + } + if (isOutputOn(OutputTag::LEARNED_LITS)) + { + // output learned literals from preprocessing + for (const Node& lit : ppl) + { + output(OutputTag::LEARNED_LITS) + << "(learned-lit " << lit << " :preprocess)" << std::endl; + } + } + for (const Node& a : assertions) + { + getAtoms(a, visited, d_ppnAtoms); + } + + Trace("level-zero") << "Preprocess status:" << std::endl; + Trace("level-zero") << "#Non-learned lits = " << d_ppnAtoms.size() + << std::endl; + Trace("level-zero") << "#Learned lits = " << ppl.size() << std::endl; + Trace("level-zero") << "#Top level subs = " + << d_env.getTopLevelSubstitutions().get().size() + << std::endl; +} + +void ZeroLevelLearner::notifyAsserted(TNode assertion) +{ + // check if at level zero + if (d_nonZeroAssert.get()) + { + d_assertNoLearnCount++; + } + else if (d_levelZeroAsserts.find(assertion) == d_levelZeroAsserts.end()) + { + int32_t alevel = d_propEngine->getDecisionLevel(assertion); + if (alevel == 0) + { + 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) + { + d_assertNoLearnCount = 0; + d_levelZeroAssertsLearned.insert(assertion); + Trace("level-zero-assert") + << "#learned now " << d_levelZeroAssertsLearned.size() << std::endl; + 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(assertion) + << ")" << std::endl; + } + return; + } + } + else + { + d_nonZeroAssert = true; + } + d_assertNoLearnCount++; + } +} + +const std::unordered_set& ZeroLevelLearner::getLearnedZeroLevelLiterals() + const +{ + return d_levelZeroAssertsLearned; +} + +} // namespace prop +} // namespace cvc5 diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h new file mode 100644 index 000000000..e9979e723 --- /dev/null +++ b/src/prop/zero_level_learner.h @@ -0,0 +1,93 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Learner for literals asserted at level zero. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROP__ZERO_LEVEL_LEARNER_H +#define CVC5__PROP__ZERO_LEVEL_LEARNER_H + +#include + +#include "context/cdhashset.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "smt/env_obj.h" + +namespace cvc5 { +namespace prop { + +class PropEngine; + +/** + * The module for processing literals that are learned at decision level zero. + * + * This tracks the literals that are asserted at decision level zero. It + * computes which literals are "learnable", which currently is limited to those + * that are over atoms that appear in the input assertions. + * + * The module can be queried for the set of learned literals, and also is + * responsible for printing the literals it learns. + */ +class ZeroLevelLearner : protected EnvObj +{ + using NodeSet = context::CDHashSet; + + public: + ZeroLevelLearner(Env& env, PropEngine* propEngine); + + ~ZeroLevelLearner(); + + void notifyInputFormulas(const std::vector& assertions, + std::unordered_map& skolemMap, + const std::vector& ppl); + /** + * Notify the given literal was asserted + */ + void notifyAsserted(TNode assertion); + + /** Get the zero-level assertions */ + const std::unordered_set& getLearnedZeroLevelLiterals() const; + + private: + static void getAtoms(TNode a, + std::unordered_set& visited, + std::unordered_set& ppLits); + + /** The prop engine we are using. */ + PropEngine* d_propEngine; + + /** Set of literals that hold at level 0 */ + std::unordered_set d_levelZeroAsserts; + + /** Set of learnable literals that hold at level 0 */ + std::unordered_set d_levelZeroAssertsLearned; + + /** Whether we have seen an assertion level > 0 */ + context::CDO d_nonZeroAssert; + + /** Preprocessed literals that are not learned */ + std::unordered_set d_ppnAtoms; + + /** Already learned TEMPORARY */ + std::unordered_set d_pplAtoms; + + /** Current counter of assertions */ + size_t d_assertNoLearnCount; +}; /* class ZeroLevelLearner */ + +} // namespace prop +} // namespace cvc5 + +#endif diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 985e811ab..249037a18 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -99,6 +99,15 @@ void Preprocessor::clearLearnedLiterals() d_propagator.getLearnedLiterals().clear(); } +std::vector Preprocessor::getLearnedLiterals() const +{ + if (d_ppContext == nullptr) + { + return {}; + } + return d_ppContext->getLearnedLiterals(); +} + void Preprocessor::cleanup() { d_processor.cleanup(); } Node Preprocessor::expandDefinitions(const Node& n) diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index c91d106f5..92be021d5 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -70,6 +70,8 @@ class Preprocessor : protected EnvObj * Clear learned literals from the Boolean propagator. */ void clearLearnedLiterals(); + /** Get learned literals */ + std::vector getLearnedLiterals() const; /** * Cleanup, which deletes the processing passes owned by this module. This * is required to be done explicitly so that passes are deleted before the diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c1608a80b..07d260c7e 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -220,11 +220,12 @@ void SmtSolver::processAssertions(Assertions& as) { d_env.verbose(2) << "converting to CNF..." << endl; const std::vector& assertions = ap.ref(); + const std::vector& ppl = d_pp.getLearnedLiterals(); // It is important to distinguish the input assertions from the skolem // definitions, as the decision justification heuristic treates the latter // specially. preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap(); - d_propEngine->assertInputFormulas(assertions, ism); + d_propEngine->assertInputFormulas(assertions, ism, ppl); } // clear the current assertions diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 2154c7fd5..f93a1b892 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -103,6 +103,8 @@ class SubstitutionMap */ void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true); + /** Size of the substitutions */ + size_t size() const { return d_substitutions.size(); } /** * Returns true iff x is in the substitution map */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3bc432e5c..19db389b4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -877,6 +877,7 @@ set(regress_0_tests regress0/printer/bv_consts_dec.smt2 regress0/printer/empty_sort.smt2 regress0/printer/empty_symbol_name.smt2 + regress0/printer/learned-lit-output.smt2 regress0/printer/let_shadowing.smt2 regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc.smt2 diff --git a/test/regress/regress0/printer/learned-lit-output.smt2 b/test/regress/regress0/printer/learned-lit-output.smt2 new file mode 100644 index 000000000..b653b854a --- /dev/null +++ b/test/regress/regress0/printer/learned-lit-output.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -o learned-lits +; SCRUBBER: sed -e 's/(learned-lit.*/learned-lit/' +; EXPECT: learned-lit +; EXPECT: learned-lit +; EXPECT: learned-lit +; EXPECT: sat +(set-logic ALL) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (> x 10)) +(assert (or (< x 5) (> y 0))) +(check-sat) -- 2.30.2