From 388fe59b2ae3d7583bd4ceefca262d336b4b9670 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 18 Jan 2022 11:06:41 -0600 Subject: [PATCH] Print original form for substitutions and learned literals (#7959) --- src/preprocessing/preprocessing_pass_context.cpp | 3 ++- src/prop/zero_level_learner.cpp | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) 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 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) -- 2.30.2