Make learned literal computation more robust (#8308)

Simplifies our computation so that preprocessed learned literals are those exactly appearing as top-level assertions only.

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8728593469aaee370542b3a6568c89224fa23a53..066c8395f443fed49b6a0fc8eca44f1f909faa9c 100644 (file)
--- 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<Node>& assertions,
-    std::unordered_map<size_t, Node>& skolemMap,
-    const std::vector<Node>& ppl)
+    std::unordered_map<size_t, Node>& 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 fc3c68ca54ae31526a94079c080ed57c0d109997..f852a39c63051cd1485a0c95d68df88055b05108 100644 (file)
--- 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<Node>& assertions,
-                           std::unordered_map<size_t, Node>& skolemMap,
-                           const std::vector<Node>& ppl);
+                           std::unordered_map<size_t, Node>& 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 44bc79d4364b7597daf15e08ba22bff569ccff3b..78e011e7437487a25b528983bc9c3dded32d4490 100644 (file)
--- 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<Node>& assertions,
-    std::unordered_map<size_t, Node>& skolemMap,
-    const std::vector<Node>& ppl)
+    std::unordered_map<size_t, Node>& 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 3e95f4a03e7b32819eb83ff893949e90bb24e38b..b034f322f834ab5ed9c5658a0a8e3e924e307e6d 100644 (file)
--- 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<Node>& assertions,
-                           std::unordered_map<size_t, Node>& skolemMap,
-                           const std::vector<Node>& ppl);
+                           std::unordered_map<size_t, Node>& 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 b5415f7140af792e3bfddc838f559e7b1685f3b6..f71cacbe916d959967ced2d8363600a81ffca669 100644 (file)
--- 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<Node>& assertions,
-    std::unordered_map<size_t, Node>& skolemMap,
-    const std::vector<Node>& ppl)
+    const std::unordered_map<size_t, Node>& 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<TNode> 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 c15e04e98153d83ff7ece35462f524ff4c9bdc62..2b0be2fb05bb8502ec23b279fd04d8a29eccc5c7 100644 (file)
--- 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<Node>& assertions,
-                           std::unordered_map<size_t, Node>& skolemMap,
-                           const std::vector<Node>& ppl);
+                           const std::unordered_map<size_t, Node>& skolemMap);
   /**
    * Notify the given literal was asserted
    */

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index cf3c40ac081c14440e19fbf4f24d4839a04e88af..8876692b73ff387be59dfe0e736b264a09d669fa 100644 (file)
--- 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<Node>& assertions = ap.ref();
-    const std::vector<Node>& 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 b653b854a85adc3bd68f980fcc8636bd07e20d58..06cbf3cd3a620ee19fb122a67dc6648700afc0dc 100644 (file)
--- 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)