From: vinciusb <65973642+vinciusb@users.noreply.github.com>
Date: Fri, 20 May 2022 13:36:04 +0000 (-0300)
Subject: New way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)
X-Git-Tag: cvc5-1.0.1~114
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5bee1ec55d125db9980a669af694642f483593a5;p=cvc5.git

New way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)

Change the way cvc5 identifies THEORY_LEMMA clusters when --print-dot-clusters option is used. Previously, only proof nodes with SCOPE rule after a CNF cluster could identify a THEORY_LEMMA cluster. Now, any of the following rules, after a CNF cluster, can identify it:

1. SCOPE
2. THEORY_LEMMA
3. Any rule R in the following range: CNF_ITE_NEG3 < R < LFSC_RULE

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
---

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 8d648140e..b99dab2c1 100644
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -341,7 +341,7 @@ ProofNodeClusterType DotPrinter::defineProofNodeType(const ProofNode* pn,
     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)
+  if (last <= ProofNodeClusterType::SAT && isSat(rule))
   {
     return ProofNodeClusterType::SAT;
   }
@@ -362,8 +362,8 @@ ProofNodeClusterType DotPrinter::defineProofNodeType(const ProofNode* pn,
     {
       return ProofNodeClusterType::CNF;
     }
-    // If the first rule after a CNF is a scope
-    if (isSCOPE(rule))
+    // If the first rule after a CNF is in the TL range
+    if (isTheoryLemma(rule))
     {
       return ProofNodeClusterType::THEORY_LEMMA;
     }
@@ -426,6 +426,12 @@ inline bool DotPrinter::isSCOPE(const PfRule& rule)
   return PfRule::SCOPE == rule;
 }
 
+inline bool DotPrinter::isTheoryLemma(const PfRule& rule)
+{
+  return rule == PfRule::SCOPE || rule == PfRule::THEORY_LEMMA
+         || (PfRule::CNF_ITE_NEG3 < rule && rule < PfRule::LFSC_RULE);
+}
+
 inline bool DotPrinter::isASSUME(const PfRule& rule)
 {
   return PfRule::ASSUME == rule;
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index 70d89e17e..7b4b26485 100644
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -166,26 +166,34 @@ class DotPrinter
   /** 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.
+   * @param rule 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.
+   * @param rule 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.
+   * @param rule 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 in the theory lemma range (open interval between
+   * CNF_ITE_NEG3 and LFSC_RULE) or if the rule is a SCOPE or THEORY_LEMMA.
+   * @param rule The rule to be verified.
+   * @return The bool indicating whether the rule is for a theory lemma
+   * range.
+   */
+  inline bool isTheoryLemma(const PfRule& rule);
+
   /** Verify if the rule is an ASSUME
-   * @param pn The rule to be verified.
+   * @param rule The rule to be verified.
    * @return The bool indicating if the rule is or not an ASSUME.
    */
   inline bool isASSUME(const PfRule& rule);