From: Lachnitt Date: Thu, 3 Mar 2022 12:57:14 +0000 (-0800) Subject: [proofs] Alethe: Removed Steps that are Double-Printed (#7754) X-Git-Tag: cvc5-1.0.0~331 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f3ae76033f2a8697aca5f92fed7d98c99c6c6265;p=cvc5.git [proofs] Alethe: Removed Steps that are Double-Printed (#7754) This PR fixes that some steps are printed more than once. To this end, it deletes that the reference maps in which the steps are stored are constant and optimizes where the steps are added to the maps. It also stores ProofNodes instead of Nodes in the maps. Co-authored-by: Haniel Barbosa --- diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp index cb4696af9..2fd898bfd 100644 --- a/src/proof/alethe/alethe_printer.cpp +++ b/src/proof/alethe/alethe_printer.cpp @@ -43,22 +43,20 @@ void AletheProofPrinter::print(std::ostream& out, // Then, print the rest of the proof node uint32_t start_t = 1; - printInternal(out, pfn->getChildren()[0], assumptions, {}, "", start_t); + std::unordered_map, std::string> steps = {}; + printInternal(out, pfn->getChildren()[0], assumptions, steps, "", start_t); } std::string AletheProofPrinter::printInternal( std::ostream& out, std::shared_ptr pfn, - const std::unordered_map& assumptions, - const std::unordered_map& steps, + std::unordered_map& assumptions, + std::unordered_map, std::string>& steps, std::string current_prefix, uint32_t& current_step_id) { 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 @@ -74,20 +72,43 @@ std::string AletheProofPrinter::printInternal( // Get the alethe proof rule AletheRule arule = getAletheRule(args[0]); + // Assumptions are printed at the anchor and therefore have to be in the list + // of assumptions when an assume is reached. + if (arule == AletheRule::ASSUME) + { + Trace("alethe-printer") + << "... reached assumption " << pfn->getResult() << " " << arule << " " + << " / " << args << " " << std::endl; + + auto it = assumptions.find(args[2]); + Assert(it != assumptions.end()) + << "Assumption has not been printed yet! " << args[2] << "/" + << assumptions << std::endl; + Trace("alethe-printer") + << "... found assumption in list " << it->second << ": " << args[2] + << "/" << assumptions << std::endl; + return it->second; + } + + // If the current step is already printed return its id + auto it = steps.find(pfn); + if (it != steps.end()) + { + Trace("alethe-printer") + << "... step is already printed " << it->second << " " + << pfn->getResult() << " " << arule << " / " << args << std::endl; + return it->second; + } + std::vector current_assumptions; + std::unordered_map assumptions_before_subproof = + assumptions; + std::unordered_map, std::string> + steps_before_subproof = steps; + // 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 + // Print anchor std::string current_t = current_prefix + "t" + std::to_string(current_step_id); Trace("alethe-printer") @@ -129,48 +150,19 @@ std::string AletheProofPrinter::printInternal( Trace("alethe-printer") << "... print assumption " << args[i] << std::endl; out << "(assume " << assumption_name << " " << args[i] << ")\n"; - new_assumptions[args[i]] = assumption_name; + 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; + std::string child_prefix = printInternal( + out, child, assumptions, steps, current_prefix, current_step_id); child_prefixes.push_back(child_prefix); } @@ -183,7 +175,15 @@ std::string AletheProofPrinter::printInternal( current_prefix.pop_back(); out << "(step " << current_prefix << " " << args[2] << " :rule " << arule; - new_steps[args[2]] = current_prefix; + // Reset steps array to the steps before the subproof since steps inside the + // subproof cannot be accessed anymore + steps = steps_before_subproof; + assumptions = assumptions_before_subproof; + + // Add to map of printed steps + steps[pfn] = current_prefix; + Trace("alethe-printer") << "... add to steps " << pfn->getArguments()[2] + << " " << current_prefix << std::endl; // Reset step id to the number before the subproof + 1 current_step_id = step_id + 1; @@ -204,23 +204,21 @@ std::string AletheProofPrinter::printInternal( 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; - } - + // Otherwise, the step is a normal step // 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; + Trace("alethe-printer") << "... print node " << current_t << " " + << pfn->getResult() << " " << arule << " / " << args + << std::endl; + + // Add to map of printed steps + steps[pfn] = current_t; + Trace("alethe-printer") << "... add to steps " << pfn->getArguments()[2] + << " " << current_t << std::endl; current_step_id++; + + out << "(step " << current_t << " " << args[2] << " :rule " << arule; if (args.size() > 3) { out << " :args ("; diff --git a/src/proof/alethe/alethe_printer.h b/src/proof/alethe/alethe_printer.h index 22fcb6499..f96c5f7d9 100644 --- a/src/proof/alethe/alethe_printer.h +++ b/src/proof/alethe/alethe_printer.h @@ -69,8 +69,8 @@ class AletheProofPrinter std::string printInternal( std::ostream& out, std::shared_ptr pfn, - const std::unordered_map& assumptions, - const std::unordered_map& steps, + std::unordered_map& assumptions, + std::unordered_map, std::string>& steps, std::string current_prefix, uint32_t& current_step_id); };