Add learned literal manager utility (#6709)

This is a simple class to maintain a list of literals that we have learned that may be useful during preprocessing.

This is work towards a "learned rewrite" preprocessing pass / better support for Int/BV translations during preprocessing.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 775e04b9c21f2628586e575cfee268b75832ee73..1edafb9779dbdc02bc8593d9ca4f3a5427cb7c04 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -52,6 +52,8 @@ libcvc5_add_sources(
   omt/omt_optimizer.h
   preprocessing/assertion_pipeline.cpp
   preprocessing/assertion_pipeline.h
+  preprocessing/learned_literal_manager.cpp
+  preprocessing/learned_literal_manager.h
   preprocessing/passes/ackermann.cpp
   preprocessing/passes/ackermann.h
   preprocessing/passes/apply_substs.cpp

diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp
new file mode 100644 (file)
index 0000000..5b30159
--- /dev/null
+++ b/src/preprocessing/learned_literal_manager.cpp
@@ -0,0 +1,52 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Learned literal manager
+ */
+
+#include "preprocessing/learned_literal_manager.h"
+
+#include "theory/rewriter.h"
+
+namespace cvc5 {
+namespace preprocessing {
+
+LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
+                                             context::UserContext* u,
+                                             ProofNodeManager* pnm)
+    : d_topLevelSubs(tls), d_learnedLits(u)
+{
+}
+
+void LearnedLiteralManager::notifyLearnedLiteral(Node lit)
+{
+  d_learnedLits.insert(lit);
+  Trace("pp-llm") << "LLM:notifyLearnedLiteral: " << lit << std::endl;
+}
+
+std::vector<Node> LearnedLiteralManager::getLearnedLiterals() const
+{
+  std::vector<Node> currLearnedLits;
+  for (const auto& lit: d_learnedLits)
+  {
+    // update based on substitutions
+    Node tlsNode = d_topLevelSubs.get().apply(lit);
+    tlsNode = theory::Rewriter::rewrite(tlsNode);
+    currLearnedLits.push_back(tlsNode);
+    Trace("pp-llm") << "Learned literal : " << tlsNode << " from " << lit
+                    << std::endl;
+  }
+  return currLearnedLits;
+}
+
+}  // namespace preprocessing
+}  // namespace cvc5

diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h
new file mode 100644 (file)
index 0000000..2148b3f
--- /dev/null
+++ b/src/preprocessing/learned_literal_manager.h
@@ -0,0 +1,71 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Learned literal manager
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H
+#define CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H
+
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "theory/trust_substitutions.h"
+
+namespace cvc5 {
+namespace preprocessing {
+
+/**
+ * This class maintains the list of learned literals that have been inferred
+ * during preprocessing but we have not fully processed e.g. via substitutions.
+ *
+ * In particular, notice that if an equality (= x t) is learned at top level,
+ * we may add x -> t to top level substitutions if t does not contain x; we can
+ * henceforth forget that (= x t) is a learned literal. On the other hand, if
+ * a literal like (> x t) is learned at top-level, it may be useful to remember
+ * this information. This class is concerned with the latter kind of literals.
+ */
+class LearnedLiteralManager
+{
+ public:
+  LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
+                        context::UserContext* u,
+                        ProofNodeManager* pnm);
+  /**
+   * 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(Node lit);
+  /**
+   * Get learned literals, which returns the current set of learned literals
+   * provided to this class. These literals are refreshed so that the current
+   * top-level substitutions are applied to them, and then are rewritten.
+   */
+  std::vector<Node> getLearnedLiterals() const;
+
+ private:
+  /** Learned literal map */
+  typedef context::CDHashSet<Node> NodeSet;
+  /* The top level substitutions */
+  theory::TrustSubstitutionMap& d_topLevelSubs;
+  /** Learned literals */
+  NodeSet d_learnedLits;
+};
+
+}  // namespace preprocessing
+}  // namespace cvc5
+
+#endif /* CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H */