From c5f96858234d6634b744ef8e4250316c62196430 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Tue, 30 Nov 2021 09:45:31 -0800 Subject: [PATCH] Alethe: Further Printer Implementation (#7675) Adds implementation of PrintInternal a function to print a proof node after the first step has been printed. Should be merged after PR #7674. Co-authored-by: Haniel Barbosa hanielbbarbosa@gmail.com --- src/proof/alethe/alethe_printer.cpp | 202 +++++++++++++++++++++++++++- 1 file changed, 201 insertions(+), 1 deletion(-) diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp index 49b2716f3..cb4696af9 100644 --- a/src/proof/alethe/alethe_printer.cpp +++ b/src/proof/alethe/alethe_printer.cpp @@ -54,7 +54,207 @@ std::string AletheProofPrinter::printInternal( std::string current_prefix, uint32_t& current_step_id) { - return ""; + int step_id = current_step_id; + std::vector current_assumptions; + const std::vector& args = pfn->getArguments(); + std::unordered_map new_assumptions = assumptions; + std::unordered_map new_steps = steps; + + // If the proof node is untranslated a problem might have occured during + // postprocessing + if (args.size() < 3 || pfn->getRule() != PfRule::ALETHE_RULE) + { + Trace("alethe-printer") + << "... printing failed! Encountered untranslated Node. " + << pfn->getResult() << " " << pfn->getRule() << " " + << " / " << args << std::endl; + return ""; + } + + // Get the alethe proof rule + AletheRule arule = getAletheRule(args[0]); + + // In case the rule is an anchor it is printed before its children. + if (arule == AletheRule::ANCHOR_SUBPROOF || arule == AletheRule::ANCHOR_BIND) + { + // Look up if subproof has already been printed + auto it = steps.find(args[2]); + if (it != steps.end()) + { + Trace("alethe-printer") + << "... subproof is already printed " << pfn->getResult() << " " + << arule << " / " << args << std::endl; + return it->second; + } + + // Otherwise, print anchor + std::string current_t = + current_prefix + "t" + std::to_string(current_step_id); + Trace("alethe-printer") + << "... print anchor " << pfn->getResult() << " " << arule << " " + << " / " << args << std::endl; + out << "(anchor :step " << current_t; + + // Append index of anchor to prefix so that all steps in the subproof use it + current_prefix.append("t" + std::to_string(current_step_id) + "."); + + // Reset the current step id s.t. the numbering inside the subproof starts + // with 1 + current_step_id = 1; + + // If the subproof is a bind the arguments need to be printed as + // assignments, i.e. args=[(= v0 v1)] is printed as (:= (v0 Int) v1). + if (arule == AletheRule::ANCHOR_BIND) + { + out << " :args ("; + for (size_t j = 3, size = args.size(); j < size; j++) + { + out << "(:= (" << args[j][0] << " " << args[j][0].getType() << ") " + << args[j][1] << ")" << (j != args.size() - 1 ? " " : ""); + } + out << ")"; + } + // In all other cases there are no arguments + out << ")\n"; + + // If the subproof is a genuine subproof the arguments are printed as + // assumptions. To be able to discharge the assumptions afterwards we need + // to store them. + if (arule == AletheRule::ANCHOR_SUBPROOF) + { + for (size_t i = 3, size = args.size(); i < size; i++) + { + std::string assumption_name = + current_prefix + "a" + std::to_string(i - 3); + Trace("alethe-printer") + << "... print assumption " << args[i] << std::endl; + out << "(assume " << assumption_name << " " << args[i] << ")\n"; + new_assumptions[args[i]] = assumption_name; + current_assumptions.push_back(assumption_name); + } + } + } + + // Assumptions are printed at the anchor and therefore have to be in the list + // of assumptions when an assume is reached. + else if (arule == AletheRule::ASSUME) + { + Trace("alethe-printer") + << "... reached assumption " << pfn->getResult() << " " << arule << " " + << " / " << args << " " << std::endl; + + auto it = assumptions.find(args[2]); + if (it != assumptions.end()) + { + Trace("alethe-printer") << "... found assumption in list " + << ": " << args[2] << "/" << assumptions + << " " << it->second << std::endl; + return it->second; + } + + Trace("alethe-printer") << "... printing failed! Encountered assumption " + "that has not been printed! " + << args[2] << "/" << assumptions << std::endl; + return ""; + } + + // Print children + std::vector child_prefixes; + + const std::vector>& children = pfn->getChildren(); + for (const std::shared_ptr& child : children) + { + std::string child_prefix = printInternal(out, + child, + new_assumptions, + new_steps, + current_prefix, + current_step_id); + new_steps[args[2]] = child_prefix; + child_prefixes.push_back(child_prefix); + } + + // If the rule is a subproof a final subproof step needs to be printed + if (arule == AletheRule::ANCHOR_SUBPROOF || arule == AletheRule::ANCHOR_BIND) + { + Trace("alethe-printer") << "... print anchor node " << pfn->getResult() + << " " << arule << " / " << args << std::endl; + + current_prefix.pop_back(); + out << "(step " << current_prefix << " " << args[2] << " :rule " << arule; + + new_steps[args[2]] = current_prefix; + + // Reset step id to the number before the subproof + 1 + current_step_id = step_id + 1; + + // Discharge assumptions in the case of subproof + // The assumptions of this level have been stored in current_assumptions + if (arule == AletheRule::ANCHOR_SUBPROOF) + { + out << " :discharge ("; + for (size_t j = 0, size = current_assumptions.size(); j < size; j++) + { + out << current_assumptions[j] + << (j != current_assumptions.size() - 1 ? " " : ""); + } + out << ")"; + } + out << ")\n"; + return current_prefix; + } + + // If the current step is already printed return its id + auto it = new_steps.find(args[2]); + if (it != new_steps.end()) + { + Trace("alethe-printer") + << "... step is already printed " << pfn->getResult() << " " << arule + << " / " << args << std::endl; + return it->second; + } + + // Print current step + Trace("alethe-printer") << "... print node " << pfn->getResult() << " " + << arule << " / " << args << std::endl; + std::string current_t = + current_prefix + "t" + std::to_string(current_step_id); + out << "(step " << current_t << " " << args[2] << " :rule " << arule; + current_step_id++; + if (args.size() > 3) + { + out << " :args ("; + for (size_t i = 3, size = args.size(); i < size; i++) + { + if (arule == AletheRule::FORALL_INST) + { + out << "(:= " << args[i][0] << " " << args[i][1] << ")"; + } + else + { + out << args[i]; + } + if (i != args.size() - 1) + { + out << " "; + } + } + out << ")"; + } + if (pfn->getChildren().size() >= 1) + { + out << " :premises ("; + for (size_t i = 0, size = child_prefixes.size(); i < size; i++) + { + out << child_prefixes[i] << (i != size - 1? " " : ""); + } + out << "))\n"; + } + else + { + out << ")\n"; + } + return current_t; } } // namespace proof -- 2.30.2