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 <diegodellarocc@gmail.com>
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
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"
--- /dev/null
+/********************* */
+/*! \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 <sstream>
+#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<std::shared_ptr<ProofNode>>& 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<ProofNode>& 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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#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
#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"
std::shared_ptr<ProofNode> 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<ProofNode> pfn,
Assertions& as,
DefinedFunctionMap& df)
projects / cvc5.git / commitdiff