Integrate learned literal manager into preprocessing pass context (#6718)

Towards "learned rewrite" preprocessing pass / improvements to Int <-> BV.

diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp
index 5b301592a080d7915e6b1f95b4de02b283e18bd3..fa6a017910833b99c4b4d9b6d4524aabdaaf25e5 100644 (file)
--- 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 2148b3f7c060bd18f88b539e6c9f921f64ad4d70..2b02736286884079863725caf11484b8bd8f46fb 100644 (file)
--- 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 b05dbbe1c4ff8fbfe58b4ce868e4f59f8aac0eab..5610b0117fb907802d03163a502173e2ca63012e 100644 (file)
--- 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 eaccce1a9b8627d93687f2597182c4f81a1f5cb9..b21fcb261deb70b46cefee70bf685a4a13b8b99a 100644 (file)
--- 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 722c82f6be17404c7bba461096c3cea269691605..1af73e45339fad281ca4fd8758ef5d34de32dddf 100644 (file)
--- 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.