#include "proof/dot/dot_printer.h"
+#include <algorithm>
#include <sstream>
#include "options/expr_options.h"
+#include "options/printer_options.h"
#include "options/proof_options.h"
#include "printer/smt2/smt2_printer.h"
#include "proof/proof_checker.h"
: 0),
d_ruleID(0)
{
+ const std::string acronyms[5] = {"SAT", "CNF", "TL", "PP", "IN"};
+ const std::string colors[5] = {"purple", "yellow", "green", "brown", "blue"};
+
+ for (unsigned i = 0; i < 5; i++)
+ {
+ d_subgraphsStr.push_back(std::ostringstream());
+ d_subgraphsStr[i] << "\n\tsubgraph cluster_" << acronyms[i]
+ << " {\n\t\tlabel=\"" << acronyms[i]
+ << "\"\n\t\tbgcolor=\"" << colors[i] << "\"\n\t\t";
+ }
}
DotPrinter::~DotPrinter() {}
}
std::map<size_t, uint64_t> proofLet;
- DotPrinter::printInternal(out, pn, proofLet, 0, false);
- out << "}\n";
+ DotPrinter::printInternal(
+ out, pn, proofLet, ProofNodeClusterType::NOT_DEFINED);
+
+ if (options::printDotClusters())
+ {
+ // Print the sub-graphs
+ for (unsigned i = 0; i < 5; i++)
+ {
+ out << d_subgraphsStr[i].str() << "\n\t};";
+ }
+ }
+ out << "\n}\n";
}
uint64_t DotPrinter::printInternal(std::ostream& out,
const ProofNode* pn,
std::map<size_t, uint64_t>& pfLet,
- uint64_t scopeCounter,
- bool inPropositionalView)
+ ProofNodeClusterType parentType)
{
uint64_t currentRuleID = d_ruleID;
pfLet[currentHash] = currentRuleID;
}
+
+ ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED;
+ if (options::printDotClusters())
+ {
+ // Define the type of this node
+ proofNodeType = defineProofNodeType(pn, parentType);
+ if (proofNodeType != ProofNodeClusterType::FIRST_SCOPE
+ && proofNodeType != ProofNodeClusterType::NOT_DEFINED)
+ {
+ d_subgraphsStr[static_cast<int>(proofNodeType) - 1] << d_ruleID << " ";
+ }
+ }
+
+ printProofNodeInfo(out, pn);
+
d_ruleID++;
+ PfRule r = pn->getRule();
+
+ const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
+ for (const std::shared_ptr<ProofNode>& c : children)
+ {
+ uint64_t childId = printInternal(out, c.get(), pfLet, proofNodeType);
+ out << "\t" << childId << " -> " << currentRuleID << ";\n";
+ }
+
+ // If it's a scope, then remove from the stack
+ if (isSCOPE(r) && options::printDotClusters())
+ {
+ d_scopesArgs.pop_back();
+ }
+
+ return currentRuleID;
+}
+
+void DotPrinter::printProofNodeInfo(std::ostream& out, const ProofNode* pn)
+{
std::ostringstream currentArguments, resultStr, classes, colors;
- out << "\t" << currentRuleID << " [ label = \"{";
+ out << "\t" << d_ruleID << " [ label = \"{";
resultStr << d_lbind.convert(pn->getResult(), "let");
std::string astring = resultStr.str();
DotPrinter::ruleArguments(currentArguments, pn);
astring = currentArguments.str();
out << "|" << r << sanitizeString(astring) << "}\"";
- classes << ", class = \"";
- colors << "";
- // set classes and colors, based on the view that the rule belongs
- switch (r)
- {
- case PfRule::SCOPE:
- if (scopeCounter < 1)
- {
- classes << " basic";
- colors << ", color = blue ";
- inPropositionalView = true;
- }
- scopeCounter++;
- break;
- case PfRule::ASSUME:
- // a node can belong to more than one view, so these if's must not be
- // exclusive
- if (scopeCounter < 2)
- {
- classes << " basic";
- colors << ", color = blue ";
- }
- if (inPropositionalView)
- {
- classes << " propositional";
- colors << ", fillcolor = aquamarine4, style = filled ";
- }
- break;
- case PfRule::CHAIN_RESOLUTION:
- case PfRule::FACTORING:
- case PfRule::REORDERING:
- if (inPropositionalView)
- {
- classes << " propositional";
- colors << ", fillcolor = aquamarine4, style = filled ";
- }
- break;
- default: inPropositionalView = false;
- }
- classes << " \"";
- out << classes.str() << colors.str();
// add number of subchildren
std::map<const ProofNode*, size_t>::const_iterator it =
d_subpfCounter.find(pn);
- out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\"";
- out << " ];\n";
+ out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\" ];\n";
+}
- const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
- for (const std::shared_ptr<ProofNode>& c : children)
+ProofNodeClusterType DotPrinter::defineProofNodeType(const ProofNode* pn,
+ ProofNodeClusterType last)
+{
+ PfRule rule = pn->getRule();
+ if (isSCOPE(rule))
{
- uint64_t childId =
- printInternal(out, c.get(), pfLet, scopeCounter, inPropositionalView);
- out << "\t" << childId << " -> " << currentRuleID << ";\n";
+ d_scopesArgs.push_back(pn->getArguments());
}
- return currentRuleID;
+ // If is the first node
+ if (!d_ruleID)
+ {
+ return ProofNodeClusterType::FIRST_SCOPE;
+ }
+ // If the rule is in the SAT range and the last node was: FF or SAT
+ if (isSat(rule) && last <= ProofNodeClusterType::SAT)
+ {
+ return ProofNodeClusterType::SAT;
+ }
+ // If is a ASSUME
+ if (isASSUME(rule))
+ {
+ if (isInput(pn))
+ {
+ return ProofNodeClusterType::INPUT;
+ }
+ return last;
+ }
+ // the last node was: FS, SAT or CNF
+ if (last <= ProofNodeClusterType::CNF)
+ {
+ // If the rule is in the CNF range
+ if (isCNF(rule))
+ {
+ return ProofNodeClusterType::CNF;
+ }
+ // If the first rule after a CNF is a scope
+ if (isSCOPE(rule))
+ {
+ return ProofNodeClusterType::THEORY_LEMMA;
+ }
+ // Is not a scope
+ return ProofNodeClusterType::PRE_PROCESSING;
+ }
+ // If the last rule was pre processing
+ if (last == ProofNodeClusterType::PRE_PROCESSING)
+ {
+ return ProofNodeClusterType::PRE_PROCESSING;
+ }
+ // If the last rule was theory lemma
+ if (last == ProofNodeClusterType::THEORY_LEMMA)
+ {
+ return ProofNodeClusterType::THEORY_LEMMA;
+ }
+
+ return ProofNodeClusterType::NOT_DEFINED;
+}
+
+inline bool DotPrinter::isInput(const ProofNode* pn)
+{
+ const TNode& thisAssumeArg = pn->getArguments()[0];
+ auto& firstScope = d_scopesArgs[0].get();
+
+ // Verifies if the arg of this assume are in the first scope
+ if (std::find(firstScope.begin(), firstScope.end(), thisAssumeArg)
+ == firstScope.end())
+ {
+ return false;
+ }
+
+ // Verifies if the arg of this assume is at any of the other scopes
+ for (size_t i = d_scopesArgs.size() - 1; i > 0; i--)
+ {
+ auto& args = d_scopesArgs[i].get();
+
+ if (std::find(args.begin(), args.end(), thisAssumeArg) != args.end())
+ {
+ return false;
+ }
+ }
+
+ return true;
+}
+
+inline bool DotPrinter::isSat(const PfRule& rule)
+{
+ return PfRule::CHAIN_RESOLUTION <= rule
+ && rule <= PfRule::MACRO_RESOLUTION_TRUST;
+}
+
+inline bool DotPrinter::isCNF(const PfRule& rule)
+{
+ return PfRule::NOT_NOT_ELIM <= rule && rule <= PfRule::CNF_ITE_NEG3;
+}
+
+inline bool DotPrinter::isSCOPE(const PfRule& rule)
+{
+ return PfRule::SCOPE == rule;
+}
+
+inline bool DotPrinter::isASSUME(const PfRule& rule)
+{
+ return PfRule::ASSUME == rule;
}
void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
#define CVC5__PROOF__DOT__DOT_PRINTER_H
#include <iostream>
+#include <stack>
#include "printer/let_binding.h"
#include "proof/proof_node.h"
namespace cvc5::internal {
namespace proof {
+/**
+ * An enumeration for proof nodes cluster type. Each type defines in which
+ * cluster the proof node will be inserted when printed.
+ */
+enum class ProofNodeClusterType : uint8_t
+{
+ // ======== FIRST_SCOPE
+ // Type of proof node cluster that is always in the root of the graph.
+ // The rule is always SCOPE.
+ FIRST_SCOPE = 0,
+ // ======== SAT
+ // Type of proof node cluster that is between FIRST_SCOPE and CNF.
+ // The rules are: CHAIN_RESOLUTION, FACTORING, REORDERING, MACRO_RESOLUTION
+ // and MACRO_RESOLUTION_TRUST.
+ SAT,
+ // ======== CNF
+ // Type of proof node cluster that is below SAT and above THEORY_LEMMA or
+ // PRE_PROCESSING.
+ // The rules, that are described by the PfRule enumeration, are in the range
+ // between NOT_NOT_ELIM and CNF_ITE_NEG3.
+ CNF,
+ // ======== THEORY_LEMMA
+ // Proof nodes contained in a SCOPE which starts just after a SAT or CNF proof
+ // cluster.
+ THEORY_LEMMA,
+ // ======== PRE_PROCESSING
+ // Type of proof node cluster that is in the middle of the proof.
+ // The rules can be of any type. The proof nodes that aren't THEORY_LEMMA
+ // after CNF are PRE_PROCESSING. Therefore, the root of this cluster type
+ // can't be a SCOPE proof node.
+ PRE_PROCESSING,
+ // ======== INPUT
+ // Type of proof node that is always a leaf with regard to the FIRST_SCOPE.
+ // The rules are always ASSUME and the argument assumed by it was only scoped
+ // by the FIRST_SCOPE and no other SCOPE, i.e., it was not shadowed by an
+ // inner scope.
+ INPUT,
+ // ======== NOT_DEFINED
+ NOT_DEFINED
+};
+
class DotPrinter
{
public:
private:
/**
* Print the nodes of the proof in the format:
- * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}",
- * $COLORS_AND_CLASSES_RELATED_TO_THE_RULE ]; and then for each child of the
+ * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", comment =
+ * "{\"subProofQty\":$SUB_PROOF_QUANTITY}" ]; and then for each child of the
* node $CHILD_ID -> $NODE_ID; and then recursively calls the function with
* the child as argument.
* @param out the output stream
* @param pn the proof node to print
- * @param pfLet the map of the hashs of proof nodes already printed to their ids
- * @param scopeCounter counter of how many SCOPE were already depth-first
- * traversed in the proof up to this point
- * @param inPropositionalView flag used to mark the proof node being traversed
- * was generated by the SAT solver and thus belong to the propositional view
+ * @param pfLet the map of the hashs of proof nodes already printed to their
+ * ids
+ * @param parentType the type of the parent node
* @return the id of the proof node printed
*/
uint64_t printInternal(std::ostream& out,
const ProofNode* pn,
std::map<size_t, uint64_t>& pfLet,
- uint64_t scopeCounter,
- bool inPropositionalView);
+ ProofNodeClusterType parentType);
+
+ /**
+ * Print the nodes of the proof in the format:
+ * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", comment =
+ * "{\"subProofQty\":$SUB_PROOF_QUANTITY}" ];
+ * @param out the output stream
+ * @param pn the proof node to print
+ */
+ inline void printProofNodeInfo(std::ostream& out, const ProofNode* pn);
/**
* Return the arguments of a ProofNode
/** Traverse proof node and populate d_lbind
*
- * @param pn the proof node to be traversed
+ * @param pn The proof node to be traversed
*/
void letifyResults(const ProofNode* pn);
+ /** Define the proof node type and populate d_nodesClusterType and
+ * d_scopesArgs.
+ * @param pn The proof node to categorize.
+ * @param last The type of the parent of the current proof node
+ * @return the current node type
+ */
+ ProofNodeClusterType defineProofNodeType(const ProofNode* pn,
+ ProofNodeClusterType last);
+
+ /** Whether the proof node is an input node or not. An input is a proof node
+ * that has an ASSUME rule and the argument assumed by it must be scoped only
+ * by the FIRST SCOPE. In other words, if there is at least one SCOPE (other
+ * than the FIRST SCOPE) that is an ancestor of this ASSUME proof node and its
+ * argument is scoped by this ancestor, then the ASSUME is no longer an input.
+ * @param pn The proof node to be verified.
+ * @return The bool indicating if the proof node is or not an input.
+ */
+ inline bool isInput(const ProofNode* pn);
+
+ /** Verify if the rule is in the SAT range (i.e. a PfRule that is
+ * CHAIN_RESOLUTION, FACTORING, REORDERING, MACRO_RESOLUTION or
+ * MACRO_RESOLUTION_TRUST).
+ * @param pn The rule to be verified.
+ * @return The bool indicating if the rule is or not in the SAT range.
+ */
+ inline bool isSat(const PfRule& rule);
+
+ /** Verify if the rule is in the CNF range (between NOT_NOT_ELIM and
+ * CNF_ITE_NEG3) in the PfRule enumeration.
+ * @param pn The rule to be verified.
+ * @return The bool indicating if the rule is or not in the CNF range.
+ */
+ inline bool isCNF(const PfRule& rule);
+
+ /** Verify if the rule is a SCOPE
+ * @param pn The rule to be verified.
+ * @return The bool indicating if the rule is or not a SCOPE.
+ */
+ inline bool isSCOPE(const PfRule& rule);
+
+ /** Verify if the rule is an ASSUME
+ * @param pn The rule to be verified.
+ * @return The bool indicating if the rule is or not an ASSUME.
+ */
+ inline bool isASSUME(const PfRule& rule);
+
/** All unique subproofs of a given proof node (counting itself). */
std::map<const ProofNode*, size_t> d_subpfCounter;
/** Counter that indicates the current rule ID */
uint64_t d_ruleID;
+
+ /** The arguments (assumptions), per level, of all scopes under which the
+ * traversal is currently under. */
+ std::vector<std::reference_wrapper<const std::vector<Node>>> d_scopesArgs;
+
+ /** All the subgraph description strings */
+ std::vector<std::ostringstream> d_subgraphsStr;
};
} // namespace proof
projects / cvc5.git / commitdiff