From 7c0191f914405b6f88eba838af101e045de2d933 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 14 Jan 2022 16:17:57 -0600 Subject: [PATCH] Implement -o subs to show learned top-level substitutions (#7944) Also adds substitutions as part of the output of -o learned-lits for completeness. --- src/options/base_options.toml | 5 +++ src/preprocessing/passes/non_clausal_simp.cpp | 2 +- .../preprocessing_pass_context.cpp | 36 +++++++++++++++++-- .../preprocessing_pass_context.h | 12 +++++-- src/theory/substitutions.cpp | 14 ++++++-- src/theory/substitutions.h | 2 ++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/printer/print_subs.smt2 | 9 +++++ 8 files changed, 74 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress0/printer/print_subs.smt2 diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 86ce22c6f..6a34978f5 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -193,6 +193,11 @@ name = "Base" help = "print input literals that hold globally" description = "With ``-o learned-lits``, cvc5 prints input literals that it has learned to hold globally." example-file = "regress0/printer/learned-lit-output.smt2" +[[option.mode.SUBS]] + name = "subs" + help = "print top-level substitutions learned during preprocessing" + description = "With ``-o subs``, cvc5 prints top-level substitutions learned during preprocessing." + example-file = "regress0/printer/subs-output.smt2" # Stores then enabled output tags. [[option]] diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 2924b2dc3..8474cef6a 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -395,7 +395,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // Note that we don't have to keep rhs's in full solved form // because SubstitutionMap::apply does a fixed-point iteration when // substituting - ttls.addSubstitutions(*newSubstitutions.get()); + d_preprocContext->addSubstitutions(*newSubstitutions.get()); if (!learnedLitsToConjoin.empty()) { diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index e316c2f81..7e8a54398 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -16,6 +16,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "expr/node_algorithm.h" +#include "options/base_options.h" #include "smt/env.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -81,11 +82,24 @@ std::vector PreprocessingPassContext::getLearnedLiterals() const return d_llm.getLearnedLiterals(); } +void PreprocessingPassContext::printSubstitution(const Node& lhs, + const Node& rhs) const +{ + Node eq = lhs.eqNode(rhs); + output(OutputTag::LEARNED_LITS) + << "(learned-lit " << eq << " :preprocess-subs)" << std::endl; + output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl; +} + void PreprocessingPassContext::addSubstitution(const Node& lhs, const Node& rhs, ProofGenerator* pg) { - getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg); + if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS)) + { + printSubstitution(lhs, rhs); + } + d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg); } void PreprocessingPassContext::addSubstitution(const Node& lhs, @@ -93,7 +107,25 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, PfRule id, const std::vector& args) { - getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); + if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS)) + { + printSubstitution(lhs, rhs); + } + d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); +} + +void PreprocessingPassContext::addSubstitutions( + theory::TrustSubstitutionMap& tm) +{ + if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS)) + { + std::unordered_map subs = tm.get().getSubstitutions(); + for (const std::pair& s : subs) + { + printSubstitution(s.first, s.second); + } + } + d_env.getTopLevelSubstitutions().addSubstitutions(tm); } } // namespace preprocessing diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index d452e23ff..31c0bbc46 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -79,7 +79,11 @@ class PreprocessingPassContext : protected EnvObj /** Spend resource in the resource manager of the associated Env. */ void spendResource(Resource r); - /** Get a reference to the top-level substitution map */ + /** + * Get a reference to the top-level substitution map. Note that all + * substitutions added to this map should use the addSubstitution methods + * below for the purposes of proper debugging information. + */ theory::TrustSubstitutionMap& getTopLevelSubstitutions() const; /** Record symbols in assertions @@ -116,9 +120,13 @@ class PreprocessingPassContext : protected EnvObj const Node& rhs, PfRule id, const std::vector& args); - + /** Add top level substitutions for a substitution map */ + void addSubstitutions(theory::TrustSubstitutionMap& tm); private: + /** Helper method for printing substitutions */ + void printSubstitution(const Node& lhs, const Node& rhs) const; + /** Pointer to the theory engine associated with this context. */ TheoryEngine* d_theoryEngine; /** Pointer to the prop engine associated with this context. */ diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 279237eb8..71612021e 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -31,6 +31,16 @@ SubstitutionMap::SubstitutionMap(context::Context* context) { } +std::unordered_map SubstitutionMap::getSubstitutions() +{ + std::unordered_map subs; + for (const auto& sub : d_substitutions) + { + subs.emplace(sub.first, sub.second); + } + return subs; +} + struct substitution_stack_element { TNode d_node; bool d_children_added; @@ -181,8 +191,8 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache) { - SubstitutionMap::NodeMap::const_iterator it = subMap.begin(); - SubstitutionMap::NodeMap::const_iterator it_end = subMap.end(); + NodeMap::const_iterator it = subMap.begin(); + NodeMap::const_iterator it_end = subMap.end(); for (; it != it_end; ++ it) { Assert(d_substitutions.find((*it).first) == d_substitutions.end()); d_substitutions[(*it).first] = (*it).second; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index f93a1b892..f6d4bdcf0 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -93,6 +93,8 @@ class SubstitutionMap public: SubstitutionMap(context::Context* context = nullptr); + /** Get substitutions in this object as a raw map */ + std::unordered_map getSubstitutions(); /** * Adds a substitution from x to t. */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3bc0ff9a9..6a09e04cf 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -879,6 +879,7 @@ set(regress_0_tests regress0/printer/empty_symbol_name.smt2 regress0/printer/learned-lit-output.smt2 regress0/printer/let_shadowing.smt2 + regress0/printer/print_subs.smt2 regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc.smt2 regress0/proj-issue307-get-value-re.smt2 diff --git a/test/regress/regress0/printer/print_subs.smt2 b/test/regress/regress0/printer/print_subs.smt2 new file mode 100644 index 000000000..1867537a2 --- /dev/null +++ b/test/regress/regress0/printer/print_subs.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -o subs +; EXPECT: (substitution (= a 3)) +; EXPECT: sat +(set-logic ALL) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (= (* 2 a) 6)) +(assert (> b a)) +(check-sat) -- 2.30.2