From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 18 Jan 2022 17:06:41 +0000 (-0600)
Subject: Print original form for substitutions and learned literals (#7959)
X-Git-Tag: cvc5-1.0.0~532
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=388fe59b2ae3d7583bd4ceefca262d336b4b9670;p=cvc5.git

Print original form for substitutions and learned literals (#7959)
---

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 7e8a54398..7d26b4ff0 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 "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "smt/env.h"
 #include "theory/theory_engine.h"
@@ -85,7 +86,7 @@ std::vector<Node> PreprocessingPassContext::getLearnedLiterals() const
 void PreprocessingPassContext::printSubstitution(const Node& lhs,
                                                  const Node& rhs) const
 {
-  Node eq = lhs.eqNode(rhs);
+  Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
   output(OutputTag::LEARNED_LITS)
       << "(learned-lit " << eq << " :preprocess-subs)" << std::endl;
   output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;
diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp
index 1b11662aa..3562545b8 100644
--- a/src/prop/zero_level_learner.cpp
+++ b/src/prop/zero_level_learner.cpp
@@ -84,7 +84,8 @@ void ZeroLevelLearner::notifyInputFormulas(
     for (const Node& lit : ppl)
     {
       output(OutputTag::LEARNED_LITS)
-          << "(learned-lit " << lit << " :preprocess)" << std::endl;
+          << "(learned-lit " << SkolemManager::getOriginalForm(lit)
+          << " :preprocess)" << std::endl;
     }
   }
   for (const Node& a : assertions)