Implement -o subs to show learned top-level substitutions (#7944)

Also adds substitutions as part of the output of -o learned-lits for completeness.

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 86ce22c6f542b4787c979d6fde7e74fd84dd57b7..6a34978f57b1797ae7534466a41867437d01154a 100644 (file)
--- 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 2924b2dc33967e1a5de0e2580ba8f884dee487a0..8474cef6afde7f71cd0f94cd006533a344d3a505 100644 (file)
--- 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 e316c2f811a7df273a1adf2e9c234712d3c912bc..7e8a543983927319fb5bf1cb6e614c6a9688403b 100644 (file)
--- 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<Node> 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<Node>& 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<Node, Node> subs = tm.get().getSubstitutions();
+    for (const std::pair<const Node, Node>& 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 d452e23ff5b3947d80868d61a4e703bc0f57c4ea..31c0bbc46b9938e7f3ae684bc479a411258e91c3 100644 (file)
--- 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<Node>& 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 279237eb845d5c4d511ead4c0c4539cb6f4f3e34..71612021e3dd65cd9d2dd857346b8f8086901ca4 100644 (file)
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -31,6 +31,16 @@ SubstitutionMap::SubstitutionMap(context::Context* context)
 {
 }
 
+std::unordered_map<Node, Node> SubstitutionMap::getSubstitutions()
+{
+  std::unordered_map<Node, Node> 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 f93a1b892d059829d0b04ed9d6d04ae62f53c6fb..f6d4bdcf01ae7af957c75d740708fbc48dc81ff6 100644 (file)
--- 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<Node, Node> getSubstitutions();
   /**
    * Adds a substitution from x to t.
    */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bc0ff9a931f0e13bc573b970e248c4ec594af34..6a09e04cfee58ff295a435d2191d6a0d1c370aa0 100644 (file)
--- 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 (file)
index 0000000..1867537
--- /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)