From: Diego Della Rocca de Camargos Date: Sun, 14 Mar 2021 14:55:55 +0000 (-0300) Subject: [proof-new] Adding a dot printer for proof nodes (#6144) X-Git-Tag: cvc5-1.0.0~2083 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5fccede7df78196c6153300d956236ac28daa8f9;p=cvc5.git [proof-new] Adding a dot printer for proof nodes (#6144) Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode). Signed-off-by: Diego Della Rocca de Camargos --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 005911ca8..e65e06da3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -140,6 +140,8 @@ libcvc4_add_sources( proof/clause_id.h proof/cnf_proof.cpp proof/cnf_proof.h + proof/dot/dot_printer.cpp + proof/dot/dot_printer.h proof/proof_manager.cpp proof/proof_manager.h proof/sat_proof.h diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 631a27604..ff03e70f5 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -2,6 +2,21 @@ id = "PROOF" name = "Proof" header = "options/proof_options.h" +[[option]] + name = "proofFormatMode" + category = "regular" + long = "proof-format-mode=MODE" + type = "ProofFormatMode" + default = "NONE" + help = "select language of proof output" + help_mode = "Proof format modes." +[[option.mode.NONE]] + name = "none" + help = "Do not translate proof output" +[[option.mode.DOT]] + name = "dot" + help = "Output DOT proof" + [[option]] name = "proofPrintConclusion" category = "regular" diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp new file mode 100644 index 000000000..f542924b1 --- /dev/null +++ b/src/proof/dot/dot_printer.cpp @@ -0,0 +1,94 @@ +/********************* */ +/*! \file dot_printer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Diego Camargos + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implemantation of the module for printing dot proofs + **/ + +#include "proof/dot/dot_printer.h" + +#include +#include "expr/proof_node_manager.h" + +namespace CVC4 { +namespace proof { + +void DotPrinter::cleanQuotes(std::string& s) +{ + std::string rep("\\\""); + for (size_t pos = 0; (pos = s.find("\"", pos)) != std::string::npos; + pos += rep.length()) + { + s.replace(pos, rep.length() - 1, rep); + } +} + +void DotPrinter::print(std::ostream& out, const ProofNode* pn) +{ + uint64_t ruleID = 0; + + out << "digraph proof {\n"; + DotPrinter::printInternal(out, pn, ruleID); + out << "}\n"; +} + +void DotPrinter::printInternal(std::ostream& out, + const ProofNode* pn, + uint64_t& ruleID) +{ + uint64_t currentRuleID = ruleID; + std::ostringstream currentArguments, resultStr; + DotPrinter::ruleArguments(currentArguments, pn); + const std::vector>& children = pn->getChildren(); + + out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \"" + << pn->getRule() << "("; + + // guarantee that arguments do not have unescaped quotes + std::string astring = currentArguments.str(); + cleanQuotes(astring); + + out << astring << ")\"];\n\t\"" << currentRuleID + << "c\" [ shape = \"ellipse\", label = \""; + + // guarantee that conclusion does not have unescaped quotes + resultStr << pn->getResult(); + astring = resultStr.str(); + cleanQuotes(astring); + + out << astring << "\" ];\n\t\"" << currentRuleID << "\" -> \"" + << currentRuleID << "c\";\n"; + + for (const std::shared_ptr& c : children) + { + ++ruleID; + out << "\t\"" << ruleID << "c\" -> \"" << currentRuleID << "\";\n"; + printInternal(out, c.get(), ruleID); + } +} + +void DotPrinter::ruleArguments(std::ostringstream& currentArguments, + const ProofNode* pn) +{ + const std::vector& args = pn->getArguments(); + + if (args.size()) + { + currentArguments << args[0]; + } + + for (size_t i = 1, size = args.size(); i < size; i++) + { + currentArguments << ", " << args[i]; + } +} + +} // namespace proof +} // namespace CVC4 diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h new file mode 100644 index 000000000..4b7d7660c --- /dev/null +++ b/src/proof/dot/dot_printer.h @@ -0,0 +1,74 @@ +/********************* */ +/*! \file dot_printer.h + ** \verbatim + ** Top contributors (to current version): + ** Diego Camargos + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The module for printing dot proofs + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PROOF__DOT__DOT_PRINTER_H +#define CVC4__PROOF__DOT__DOT_PRINTER_H + +#include + +#include "expr/proof_node.h" + +namespace CVC4 { +namespace proof { + +class DotPrinter +{ + public: + DotPrinter(); + ~DotPrinter() {} + + /** + * Print the full proof of assertions => false by pn using the dot format. + * @param out the output stream + * @param pn the root node of the proof to print + */ + static void print(std::ostream& out, const ProofNode* pn); + + private: + /** + * Print the rule in the format: + * "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)" [ shape = "box"]; + * "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)" -> "$RULE_ID $RULE_CONCLUSION"; + * and then for each child of the rule print + * "$CHILD_ID $CHILD_CONCLUSION" -> "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)"; + * and then recursively call the function with the child as argument. + * @param out the output stream + * @param pn the proof node to print + * @param ruleID the id of the rule to print + */ + static void printInternal(std::ostream& out, + const ProofNode* pn, + uint64_t& ruleID); + + /** + * Return the arguments of a ProofNode + * @param currentArguments an ostringstream that will store the arguments of + * pn formatted as "$ARG[0], $ARG[1], ..., $ARG[N-1]" + * @param pn a ProofNode + */ + static void ruleArguments(std::ostringstream& currentArguments, + const ProofNode* pn); + + /** Replace all quotes but escaped quotes in given string + * @param s The string to have the quotes processed. + */ + static void cleanQuotes(std::string& s); +}; + +} // namespace proof +} // namespace CVC4 + +#endif \ No newline at end of file diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 0ae65967f..765beb9a2 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -19,6 +19,7 @@ #include "expr/proof_node_manager.h" #include "options/base_options.h" #include "options/proof_options.h" +#include "proof/dot/dot_printer.h" #include "smt/assertions.h" #include "smt/defined_function.h" #include "smt/preprocess_proof_generator.h" @@ -122,11 +123,18 @@ void PfManager::printProof(std::ostream& out, std::shared_ptr fp = getFinalProof(pfn, as, df); // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node - out << "(proof\n"; - out << *fp; - out << "\n)\n"; + + if (options::proofFormatMode() == options::ProofFormatMode::DOT) + { + proof::DotPrinter::print(out, fp.get()); + } + else + { + out << "(proof\n"; + out << *fp; + out << "\n)\n"; + } } - void PfManager::checkProof(std::shared_ptr pfn, Assertions& as, DefinedFunctionMap& df)