From ac44a43e5e678cb556f8ce3bb4e611858817c78a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Apr 2022 09:10:44 -0500 Subject: [PATCH] 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. --- src/CMakeLists.txt | 10 ++-- src/api/cpp/cvc5_types.cpp | 19 +++++++ src/api/cpp/cvc5_types.h | 55 ++++++++++++++++++ src/prop/learned_db.cpp | 113 +++++++++++++++++++++++++++++++++++++ src/prop/learned_db.h | 76 +++++++++++++++++++++++++ 5 files changed, 269 insertions(+), 4 deletions(-) create mode 100644 src/prop/learned_db.cpp create mode 100644 src/prop/learned_db.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 740436229..60627c4e8 100644 --- 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 06095f3cf..5915860dd 100644 --- 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 6579f64bc..87944905d 100644 --- 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 index 000000000..e2ae01a96 --- /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 + +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 LearnedDb::getLearnedLiterals( + modes::LearnedLitType ltype) const +{ + const NodeSet& lset = getLiteralSet(ltype); + std::vector 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& 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& 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 index 000000000..c60a27a7b --- /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; + + 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 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& getLiteralSet(modes::LearnedLitType ltype); + const context::CDHashSet& 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 -- 2.30.2