From 2dc245a5922e660b6f44032d55d452ad27dfc20f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Jun 2021 13:52:13 -0500
Subject: [PATCH] Integrate learned literal manager into preprocessing pass
 context (#6718)

Towards "learned rewrite" preprocessing pass / improvements to Int <-> BV.
---
 src/preprocessing/learned_literal_manager.cpp |  2 +-
 src/preprocessing/learned_literal_manager.h   |  2 +-
 src/preprocessing/passes/non_clausal_simp.cpp |  4 ++++
 .../preprocessing_pass_context.cpp            | 13 +++++++++++++
 .../preprocessing_pass_context.h              | 19 ++++++++++++++++++-
 5 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp
index 5b301592a..fa6a01791 100644
--- a/src/preprocessing/learned_literal_manager.cpp
+++ b/src/preprocessing/learned_literal_manager.cpp
@@ -27,7 +27,7 @@ LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
 {
 }
 
-void LearnedLiteralManager::notifyLearnedLiteral(Node lit)
+void LearnedLiteralManager::notifyLearnedLiteral(TNode lit)
 {
   d_learnedLits.insert(lit);
   Trace("pp-llm") << "LLM:notifyLearnedLiteral: " << lit << std::endl;
diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h
index 2148b3f7c..2b0273628 100644
--- a/src/preprocessing/learned_literal_manager.h
+++ b/src/preprocessing/learned_literal_manager.h
@@ -48,7 +48,7 @@ class LearnedLiteralManager
    * It should be rewritten, and such that top level substitutions have
    * been applied to it.
    */
-  void notifyLearnedLiteral(Node lit);
+  void notifyLearnedLiteral(TNode lit);
   /**
    * Get learned literals, which returns the current set of learned literals
    * provided to this class. These literals are refreshed so that the current
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index b05dbbe1c..5610b0117 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -249,6 +249,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         {
           // Keep the literal
           learned_literals[j++] = learned_literals[i];
+          // Its a literal that could not be processed as a substitution or
+          // conflict. In this case, we notify the context of the learned
+          // literal, which will process it with the learned literal manager.
+          d_preprocContext->notifyLearnedLiteral(learnedLiteral);
         }
         break;
     }
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index eaccce1a9..b21fcb261 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -30,6 +30,9 @@ PreprocessingPassContext::PreprocessingPassContext(
     : d_smt(smt),
       d_env(env),
       d_circuitPropagator(circuitPropagator),
+      d_llm(env.getTopLevelSubstitutions(),
+            env.getUserContext(),
+            env.getProofNodeManager()),
       d_symsInAssertions(env.getUserContext())
 {
 }
@@ -67,6 +70,16 @@ void PreprocessingPassContext::recordSymbolsInAssertions(
   }
 }
 
+void PreprocessingPassContext::notifyLearnedLiteral(TNode lit)
+{
+  d_llm.notifyLearnedLiteral(lit);
+}
+
+std::vector<Node> PreprocessingPassContext::getLearnedLiterals()
+{
+  return d_llm.getLearnedLiterals();
+}
+
 void PreprocessingPassContext::addSubstitution(const Node& lhs,
                                                const Node& rhs,
                                                ProofGenerator* pg)
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 722c82f6b..1af73e453 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -23,8 +23,8 @@
 #define CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
 #include "context/cdhashset.h"
+#include "preprocessing/learned_literal_manager.h"
 #include "smt/smt_engine.h"
-#include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 
 namespace cvc5 {
@@ -74,6 +74,18 @@ class PreprocessingPassContext
    */
   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
 
+  /**
+   * Notify learned literal. This method is called when a literal is
+   * entailed by the current set of assertions.
+   *
+   * It should be rewritten, and such that top level substitutions have
+   * been applied to it.
+   */
+  void notifyLearnedLiteral(TNode lit);
+  /**
+   * Get the learned literals
+   */
+  std::vector<Node> getLearnedLiterals();
   /**
    * Add substitution to the top-level substitutions, which also as a
    * consequence is used by the theory model.
@@ -100,6 +112,11 @@ class PreprocessingPassContext
   Env& d_env;
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
+  /**
+   * The learned literal manager
+   */
+  LearnedLiteralManager d_llm;
+
   /**
    * The (user-context-dependent) set of symbols that occur in at least one
    * assertion in the current user context.
-- 
2.30.2