Add learned literal type and prop learned database (#8582)

In preparation for deep restart feature, and for extending the get-learned-literal interface to multiple types.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 740436229194dbeaa63a4d041c2af8f287d6a4d8..60627c4e8688ce76eaee47b26dc493a167a97e05 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -232,10 +232,8 @@ libcvc5_add_sources(
   prop/cryptominisat.h
   prop/kissat.cpp
   prop/kissat.h
-  prop/opt_clauses_manager.cpp
-  prop/opt_clauses_manager.h
-  prop/proof_cnf_stream.cpp
-  prop/proof_cnf_stream.h
+  prop/learned_db.cpp
+  prop/learned_db.h
   prop/minisat/core/Dimacs.h
   prop/minisat/core/Solver.cc
   prop/minisat/core/Solver.h
@@ -254,6 +252,10 @@ libcvc5_add_sources(
   prop/minisat/simp/SimpSolver.cc
   prop/minisat/simp/SimpSolver.h
   prop/minisat/utils/Options.h
+  prop/opt_clauses_manager.cpp
+  prop/opt_clauses_manager.h
+  prop/proof_cnf_stream.cpp
+  prop/proof_cnf_stream.h
   prop/proof_post_processor.cpp
   prop/proof_post_processor.h
   prop/prop_engine.cpp

diff --git a/src/api/cpp/cvc5_types.cpp b/src/api/cpp/cvc5_types.cpp
index 06095f3cfe5ffba40ee42ab07c1061c4ff3fe074..5915860ddb39de93c608f7fca1877a1f58dcbb20 100644 (file)
--- a/src/api/cpp/cvc5_types.cpp
+++ b/src/api/cpp/cvc5_types.cpp
@@ -43,3 +43,22 @@ std::ostream& operator<<(std::ostream& out, UnknownExplanation e)
 }
 
 }  // namespace cvc5
+
+namespace cvc5::modes {
+
+std::ostream& operator<<(std::ostream& out, LearnedLitType ltype)
+{
+  switch (ltype)
+  {
+    case LearnedLitType::PREPROCESS_SOLVED: out << "PREPROCESS_SOLVED"; break;
+    case LearnedLitType::PREPROCESS: out << "PREPROCESS"; break;
+    case LearnedLitType::INPUT: out << "INPUT"; break;
+    case LearnedLitType::SOLVABLE: out << "SOLVABLE"; break;
+    case LearnedLitType::CONSTANT_PROP: out << "CONSTANT_PROP"; break;
+    case LearnedLitType::INTERNAL: out << "INTERNAL"; break;
+    default: out << "?";
+  }
+  return out;
+}
+
+}  // namespace cvc5::modes

diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h
index 6579f64bcb01ab2f50bf8fa1daaf47a64b15c736..87944905dbcb917ee665d5fcc25d39521aeb0e28 100644 (file)
--- a/src/api/cpp/cvc5_types.h
+++ b/src/api/cpp/cvc5_types.h
@@ -132,6 +132,61 @@ enum BlockModelsMode
   VALUES
 };
 
+/**
+ * Types of learned literals.
+ *
+ * Specifies categories of literals learned for the method
+ * Solver::getLearnedLiterals.
+ *
+ * Note that a literal may conceptually belong to multiple categories. We
+ * classify literals based on the first criteria in this list that they meet.
+ */
+enum LearnedLitType
+{
+  /**
+   * An equality that was turned into a substitution during preprocessing.
+   *
+   * In particular, literals in this category are of the form (= x t) where
+   * x does not occur in t.
+   */
+  PREPROCESS_SOLVED,
+  /**
+   * A top-level literal (unit clause) from the preprocessed set of input
+   * formulas.
+   */
+  PREPROCESS,
+  /**
+   * A literal from the preprocessed set of input formulas that does not
+   * occur at top-level after preprocessing.
+   *
+   * Typically, this is the most interesting category of literals to learn.
+   */
+  INPUT,
+  /**
+   * An internal literal that is solvable for an input variable.
+   *
+   * In particular, literals in this category are of the form (= x t) where
+   * x does not occur in t, the preprocessed set of input formulas contains the
+   * term x, but not the literal (= x t).
+   *
+   * Note that solvable literals can be turned into substitutions during
+   * preprocessing.
+   */
+  SOLVABLE,
+  /**
+   * An internal literal that can be made into a constant propagation for an
+   * input term.
+   *
+   * In particular, literals in this category are of the form (= t c) where
+   * c is a constant, the preprocessed set of input formulas contains the
+   * term t, but not the literal (= t c).
+   */
+  CONSTANT_PROP,
+  /** Any internal literal that does not fall into the above categories. */
+  INTERNAL
+};
+/** Writes a learned literal type to a stream. */
+std::ostream& operator<<(std::ostream& out, LearnedLitType ltype);
 }
 
 #endif

diff --git a/src/prop/learned_db.cpp b/src/prop/learned_db.cpp
new file mode 100644 (file)
index 0000000..e2ae01a
--- /dev/null
+++ b/src/prop/learned_db.cpp
@@ -0,0 +1,113 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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.
+ * ****************************************************************************
+ *
+ * Stores learned information
+ */
+
+#include "prop/learned_db.h"
+
+#include <sstream>
+
+namespace cvc5::internal {
+namespace prop {
+
+LearnedDb::LearnedDb(context::Context* c)
+    : d_preprocessSolvedLits(c),
+      d_preprocessLits(c),
+      d_inputLits(c),
+      d_solvableLits(c),
+      d_cpropLits(c),
+      d_internalLits(c)
+{
+}
+
+LearnedDb::~LearnedDb() {}
+
+void LearnedDb::addLearnedLiteral(const Node& lit, modes::LearnedLitType ltype)
+{
+  NodeSet& lset = getLiteralSet(ltype);
+  lset.insert(lit);
+}
+
+std::vector<Node> LearnedDb::getLearnedLiterals(
+    modes::LearnedLitType ltype) const
+{
+  const NodeSet& lset = getLiteralSet(ltype);
+  std::vector<Node> ret;
+  for (const Node& n : lset)
+  {
+    ret.push_back(n);
+  }
+  return ret;
+}
+size_t LearnedDb::getNumLearnedLiterals(modes::LearnedLitType ltype) const
+{
+  const NodeSet& lset = getLiteralSet(ltype);
+  return lset.size();
+}
+
+context::CDHashSet<Node>& LearnedDb::getLiteralSet(modes::LearnedLitType ltype)
+{
+  switch (ltype)
+  {
+    case modes::LearnedLitType::PREPROCESS_SOLVED:
+      return d_preprocessSolvedLits;
+    case modes::LearnedLitType::PREPROCESS: return d_preprocessLits;
+    case modes::LearnedLitType::INPUT: return d_inputLits;
+    case modes::LearnedLitType::SOLVABLE: return d_solvableLits;
+    case modes::LearnedLitType::CONSTANT_PROP: return d_cpropLits;
+    default: Assert(ltype == modes::LearnedLitType::INTERNAL); break;
+  }
+  return d_internalLits;
+}
+
+const context::CDHashSet<Node>& LearnedDb::getLiteralSet(
+    modes::LearnedLitType ltype) const
+{
+  switch (ltype)
+  {
+    case modes::LearnedLitType::PREPROCESS_SOLVED:
+      return d_preprocessSolvedLits;
+    case modes::LearnedLitType::PREPROCESS: return d_preprocessLits;
+    case modes::LearnedLitType::INPUT: return d_inputLits;
+    case modes::LearnedLitType::SOLVABLE: return d_solvableLits;
+    case modes::LearnedLitType::CONSTANT_PROP: return d_cpropLits;
+    default: Assert(ltype == modes::LearnedLitType::INTERNAL); break;
+  }
+  return d_internalLits;
+}
+
+std::string LearnedDb::toStringDebug() const
+{
+  std::stringstream ss;
+  ss << toStringDebugType(modes::LearnedLitType::PREPROCESS_SOLVED);
+  ss << toStringDebugType(modes::LearnedLitType::PREPROCESS);
+  ss << toStringDebugType(modes::LearnedLitType::INPUT);
+  ss << toStringDebugType(modes::LearnedLitType::SOLVABLE);
+  ss << toStringDebugType(modes::LearnedLitType::CONSTANT_PROP);
+  ss << toStringDebugType(modes::LearnedLitType::INTERNAL);
+  return ss.str();
+}
+
+std::string LearnedDb::toStringDebugType(modes::LearnedLitType ltype) const
+{
+  std::stringstream ss;
+  const NodeSet& lset = getLiteralSet(ltype);
+  if (!lset.empty())
+  {
+    ss << "#Learned literals (" << ltype << ") = " << lset.size() << std::endl;
+  }
+  return ss.str();
+}
+
+}  // namespace prop
+}  // namespace cvc5::internal

diff --git a/src/prop/learned_db.h b/src/prop/learned_db.h
new file mode 100644 (file)
index 0000000..c60a27a
--- /dev/null
+++ b/src/prop/learned_db.h
@@ -0,0 +1,76 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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.
+ * ****************************************************************************
+ *
+ * Stores learned information
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROP__LEARNED_DB_H
+#define CVC5__PROP__LEARNED_DB_H
+
+#include "api/cpp/cvc5_types.h"
+#include "context/cdhashset.h"
+#include "context/cdo.h"
+#include "expr/node.h"
+
+namespace cvc5::internal {
+namespace prop {
+
+/**
+ * This class stores high-level information learned during a run of the
+ * PropEngine. This includes the set of learned literals for each category
+ * (modes::LearnedLitType).
+ */
+class LearnedDb
+{
+  using NodeSet = context::CDHashSet<Node>;
+
+ public:
+  LearnedDb(context::Context* c);
+  ~LearnedDb();
+  /** Add learned literal of the given type */
+  void addLearnedLiteral(const Node& lit, modes::LearnedLitType ltype);
+  /** Get the learned literals for the given type */
+  std::vector<Node> getLearnedLiterals(
+      modes::LearnedLitType ltype = modes::LearnedLitType::INPUT) const;
+  /** Get number of learned literals for the given type */
+  size_t getNumLearnedLiterals(
+      modes::LearnedLitType ltype = modes::LearnedLitType::INPUT) const;
+  /** To string debug */
+  std::string toStringDebug() const;
+
+ private:
+  /** Get literal set, const and non-const versions */
+  context::CDHashSet<Node>& getLiteralSet(modes::LearnedLitType ltype);
+  const context::CDHashSet<Node>& getLiteralSet(
+      modes::LearnedLitType ltype) const;
+  /** To string debug for type of literals */
+  std::string toStringDebugType(modes::LearnedLitType ltype) const;
+  /** preprocess solved lits */
+  NodeSet d_preprocessSolvedLits;
+  /** preprocess lits */
+  NodeSet d_preprocessLits;
+  /** Input lits */
+  NodeSet d_inputLits;
+  /** Solvable lits */
+  NodeSet d_solvableLits;
+  /** Constant propagation lits */
+  NodeSet d_cpropLits;
+  /** Internal lits */
+  NodeSet d_internalLits;
+};
+
+}  // namespace prop
+}  // namespace cvc5::internal
+
+#endif