From 4128af1ac9aba2512aa339b2276c5e8fc719af45 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Mar 2022 18:32:45 -0500 Subject: [PATCH] Make learned literal computation more robust (#8308) Simplifies our computation so that preprocessed learned literals are those exactly appearing as top-level assertions only. --- src/prop/prop_engine.cpp | 5 ++-- src/prop/prop_engine.h | 4 +--- src/prop/theory_proxy.cpp | 5 ++-- src/prop/theory_proxy.h | 5 +--- src/prop/zero_level_learner.cpp | 23 ++++++++++++------- src/prop/zero_level_learner.h | 3 +-- src/smt/smt_solver.cpp | 8 ++++--- .../regress0/printer/learned-lit-output.smt2 | 1 + 8 files changed, 28 insertions(+), 26 deletions(-) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 872859346..066c8395f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -166,11 +166,10 @@ TrustNode PropEngine::removeItes(TNode node, void PropEngine::assertInputFormulas( const std::vector& assertions, - std::unordered_map& skolemMap, - const std::vector& ppl) + std::unordered_map& skolemMap) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - d_theoryProxy->notifyInputFormulas(assertions, skolemMap, ppl); + d_theoryProxy->notifyInputFormulas(assertions, skolemMap); for (const Node& node : assertions) { Debug("prop") << "assertFormula(" << node << ")" << std::endl; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index fc3c68ca5..f852a39c6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -108,11 +108,9 @@ 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, - const std::vector& ppl); + std::unordered_map& skolemMap); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 44bc79d43..78e011e74 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -74,8 +74,7 @@ void TheoryProxy::presolve() void TheoryProxy::notifyInputFormulas( const std::vector& assertions, - std::unordered_map& skolemMap, - const std::vector& ppl) + std::unordered_map& skolemMap) { // notify the theory engine of preprocessed assertions d_theoryEngine->notifyPreprocessedAssertions(assertions); @@ -101,7 +100,7 @@ void TheoryProxy::notifyInputFormulas( // determine what is learnable if (d_zll != nullptr) { - d_zll->notifyInputFormulas(assertions, skolemMap, ppl); + d_zll->notifyInputFormulas(assertions, skolemMap); } } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 3e95f4a03..b034f322f 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -74,12 +74,9 @@ class TheoryProxy : protected EnvObj, public Registrar * @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); + std::unordered_map& skolemMap); /** * Notify a lemma or input assertion, possibly corresponding to a skolem * definition. diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index b5415f714..f71cacbe9 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -67,30 +67,37 @@ void ZeroLevelLearner::getAtoms(TNode a, void ZeroLevelLearner::notifyInputFormulas( const std::vector& assertions, - std::unordered_map& skolemMap, - const std::vector& ppl) + const std::unordered_map& skolemMap) { d_assertNoLearnCount = 0; - // 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) + // We consider top level literals of assertions to be the preprocessed + // learned literals only, and not the literals tracked by the preprocessor + // (Preprocessor::getLearnedLiterals). This means that a learned literal from + // e.g. circuit propagation that is not trivially a top level assertion will + // be considered an ordinary learned literal. + // Note that d_pplAtoms and d_ppnAtoms are disjoint + for (const Node& lit : assertions) { TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit; + if (expr::isBooleanConnective(atom)) + { + continue; + } visited.insert(atom); d_pplAtoms.insert(atom); } if (isOutputOn(OutputTag::LEARNED_LITS)) { // output learned literals from preprocessing - for (const Node& lit : ppl) + for (const Node& lit : d_pplAtoms) { output(OutputTag::LEARNED_LITS) << "(learned-lit " << SkolemManager::getOriginalForm(lit) << " :preprocess)" << std::endl; } } + // Compute the set of literals in the preprocessed assertions for (const Node& a : assertions) { getAtoms(a, visited, d_ppnAtoms); @@ -99,7 +106,7 @@ void ZeroLevelLearner::notifyInputFormulas( 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") << "#Learned lits = " << d_pplAtoms.size() << std::endl; Trace("level-zero") << "#Top level subs = " << d_env.getTopLevelSubstitutions().get().size() << std::endl; diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h index c15e04e98..2b0be2fb0 100644 --- a/src/prop/zero_level_learner.h +++ b/src/prop/zero_level_learner.h @@ -50,8 +50,7 @@ class ZeroLevelLearner : protected EnvObj ~ZeroLevelLearner(); void notifyInputFormulas(const std::vector& assertions, - std::unordered_map& skolemMap, - const std::vector& ppl); + const std::unordered_map& skolemMap); /** * Notify the given literal was asserted */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index cf3c40ac0..8876692b7 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -238,12 +238,14 @@ 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. + // specially. Note that we don't pass the preprocess learned literals + // d_pp.getLearnedLiterals() here, since they may not exactly correspond + // to the actual preprocessed learned literals, as the input may have + // undergone further preprocessing. preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap(); - d_propEngine->assertInputFormulas(assertions, ism, ppl); + d_propEngine->assertInputFormulas(assertions, ism); } // clear the current assertions diff --git a/test/regress/regress0/printer/learned-lit-output.smt2 b/test/regress/regress0/printer/learned-lit-output.smt2 index b653b854a..06cbf3cd3 100644 --- a/test/regress/regress0/printer/learned-lit-output.smt2 +++ b/test/regress/regress0/printer/learned-lit-output.smt2 @@ -3,6 +3,7 @@ ; EXPECT: learned-lit ; EXPECT: learned-lit ; EXPECT: learned-lit +; EXPECT: learned-lit ; EXPECT: sat (set-logic ALL) (declare-fun x () Int) -- 2.30.2