Add unsat core lemma output tag (cvc5#11113)

Allows one to see the inference id associated with a theory lemma that
appears in an unsat core.

This PR also removes a previous (more complicated) way of achieving this
functionality (--proof-annotate).

include/cvc5/cvc5_proof_rule.h

@@ -338,18 +338,6 @@ enum ENUM(ProofRule)
    * \endverbatim
    */
   EVALUE(THEORY_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Builtin theory -- Annotation**
-   *
-   * .. math::
-   *   \inferrule{F \mid a_1 \dots a_n}{F}
-   *
-   * The terms :math:`a_1 \dots a_n` can be anything used to annotate the proof
-   * node, one example is where :math:`a_1` is a theory::InferenceId.
-   * \endverbatim
-   */
-  EVALUE(ANNOTATION),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Processing rules -- If-then-else equivalence**

src/CMakeLists.txt

@@ -158,8 +158,6 @@ libcvc5_add_sources(
   proof/alf/alf_print_channel.h
   proof/alf/alf_printer.cpp
   proof/alf/alf_printer.h
-  proof/annotation_proof_generator.cpp
-  proof/annotation_proof_generator.h
   proof/assumption_proof_generator.cpp
   proof/assumption_proof_generator.h
   proof/buffered_proof_generator.cpp
@@ -759,8 +757,6 @@ libcvc5_add_sources(
   theory/incomplete_id.h
   theory/inference_id.cpp
   theory/inference_id.h
-  theory/inference_id_proof_annotator.cpp
-  theory/inference_id_proof_annotator.h
   theory/inference_manager_buffered.cpp
   theory/inference_manager_buffered.h
   theory/lemma_property.cpp

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -35,7 +35,6 @@ const char* toString(ProofRule rule)
     case ProofRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
     case ProofRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
     case ProofRule::ENCODE_EQ_INTRO: return "ENCODE_EQ_INTRO";
-    case ProofRule::ANNOTATION: return "ANNOTATION";
     case ProofRule::DSL_REWRITE: return "DSL_REWRITE";
     case ProofRule::THEORY_REWRITE: return "THEORY_REWRITE";
     case ProofRule::ITE_EQ: return "ITE_EQ";

src/options/base_options.toml

@@ -250,6 +250,11 @@ name   = "Base"
   help = "print the corresponding benchmark when successfully computing an unsat core with theory lemmas."
   description = "With ``-o unsat-core-lemmas-benchmark``, cvc5 prints the corresponding benchmark when it successfully computes an unsat core that includes the theory lemmas used."
   example-file = "regress0/printer/print_unsat_core_lemmas.smt2"
+[[option.mode.UNSAT_CORE_LEMMAS]]
+  name = "unsat-core-lemmas"
+  help = "print diagnostic information on lemmas that appear in an unsat core with theory lemmas"
+  description = "With ``-o unsat-core-lemmas``, cvc5 prints diagnostic information on lemmas that appear in an unsat core with theory lemmas."
+  example-file = "regress0/printer/print_unsat_core_lemmas.smt2"
 [[option.mode.PORTFOLIO]]
   name = "portfolio"
   help = "prints the option strings tried in portfolio mode."

src/options/proof_options.toml

@@ -135,14 +135,6 @@ name   = "Proof"
   default    = "1000"
   help       = "the limit of steps considered for reconstructing proofs of theory rewrites"
 
-[[option]]
-  name       = "proofAnnotate"
-  category   = "expert"
-  long       = "proof-annotate"
-  type       = "bool"
-  default    = "false"
-  help       = "add optional annotations to proofs, which enables statistics for inference ids for lemmas and conflicts appearing in final proof"
-
 [[option]]
   name       = "optResReconSize"
   category   = "regular"

src/proof/proof_node_to_sexpr.cpp

@@ -347,12 +347,6 @@ ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
       }
     }
     break;
-    case ProofRule::ANNOTATION:
-      if (i == 0)
-      {
-        return ArgFormat::INFERENCE_ID;
-      }
-      break;
     case ProofRule::TRUST:
     {
       if (i == 0)

src/prop/prop_engine.cpp

@@ -773,7 +773,27 @@ void PropEngine::getUnsatCore(std::vector<Node>& core)
 std::vector<Node> PropEngine::getUnsatCoreLemmas()
 {
   Assert(d_env.isSatProofProducing());
-  return d_ppm->getUnsatCoreLemmas();
+  std::vector<Node> lems = d_ppm->getUnsatCoreLemmas();
+  if (isOutputOn(OutputTag::UNSAT_CORE_LEMMAS))
+  {
+    output(OutputTag::UNSAT_CORE_LEMMAS)
+        << ";; unsat core lemmas start" << std::endl;
+    for (const Node& lem : lems)
+    {
+      output(OutputTag::UNSAT_CORE_LEMMAS) << "(unsat-core-lemma ";
+      output(OutputTag::UNSAT_CORE_LEMMAS)
+          << SkolemManager::getOriginalForm(lem);
+      theory::InferenceId id = d_ppm->getInferenceIdFor(lem);
+      if (id != theory::InferenceId::NONE)
+      {
+        output(OutputTag::UNSAT_CORE_LEMMAS) << " :source " << id;
+      }
+      output(OutputTag::UNSAT_CORE_LEMMAS) << ")" << std::endl;
+    }
+    output(OutputTag::UNSAT_CORE_LEMMAS)
+        << ";; unsat core lemmas end" << std::endl;
+  }
+  return lems;
 }
 
 std::vector<Node> PropEngine::getLearnedZeroLevelLiterals(

src/prop/prop_proof_manager.cpp

@@ -16,6 +16,7 @@
 #include "prop/prop_proof_manager.h"
 
 #include "expr/skolem_manager.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "printer/printer.h"
 #include "proof/proof_ensure_closed.h"
@@ -63,6 +64,9 @@ PropPfManager::PropPfManager(Env& env,
       d_assumptions(assumptions),
       d_inputClauses(userContext()),
       d_lemmaClauses(userContext()),
+      d_trackLemmaClauseIds(false),
+      d_lemmaClauseIds(userContext()),
+      d_currLemmaId(theory::InferenceId::NONE),
       d_satPm(nullptr)
 {
   // add trivial assumption. This is so that we can check the that the prop
@@ -72,6 +76,7 @@ PropPfManager::PropPfManager(Env& env,
   // literal), which leads to adding True as its explanation, since for creating
   // a learned clause we need at least two literals.
   d_assertions.push_back(nodeManager()->mkConst(true));
+  d_trackLemmaClauseIds = isOutputOn(OutputTag::UNSAT_CORE_LEMMAS);
 }
 
 void PropPfManager::ensureLiteral(TNode n) { d_pfCnfStream.ensureLiteral(n); }
@@ -83,7 +88,9 @@ void PropPfManager::convertAndAssert(theory::InferenceId id,
                                      bool input,
                                      ProofGenerator* pg)
 {
+  d_currLemmaId = id;
   d_pfCnfStream.convertAndAssert(node, negated, removable, input, pg);
+  d_currLemmaId = theory::InferenceId::NONE;
   // if input, register the assertion in the proof manager
   if (input)
   {
@@ -139,6 +146,17 @@ std::vector<Node> PropPfManager::getUnsatCoreLemmas()
   return usedLemmas;
 }
 
+theory::InferenceId PropPfManager::getInferenceIdFor(const Node& lem) const
+{
+  context::CDHashMap<Node, theory::InferenceId>::const_iterator it =
+      d_lemmaClauseIds.find(lem);
+  if (it != d_lemmaClauseIds.end())
+  {
+    return it->second;
+  }
+  return theory::InferenceId::NONE;
+}
+
 std::vector<Node> PropPfManager::getMinimizedAssumptions()
 {
   std::vector<Node> minAssumptions;
@@ -444,6 +462,10 @@ Node PropPfManager::normalizeAndRegister(TNode clauseNode,
   else
   {
     d_lemmaClauses.insert(normClauseNode);
+    if (d_trackLemmaClauseIds)
+    {
+      d_lemmaClauseIds[normClauseNode] = d_currLemmaId;
+    }
   }
   if (d_satPm)
   {

src/prop/prop_proof_manager.h

@@ -118,6 +118,14 @@ class PropPfManager : protected EnvObj
   /** Return lemmas used in the SAT proof. */
   std::vector<Node> getUnsatCoreLemmas();
 
+  /**
+   * Get inference id for a lemma, e.g. one that appears in the return of
+   * getUnsatCoreLemmas. Note that the inference id will be InferenceId::NONE
+   * if lem is not an unsat core lemma, or if it corresponded e.g. to a lemma
+   * learned via theory propagation.
+   */
+  theory::InferenceId getInferenceIdFor(const Node& lem) const;
+
   /**
    * Checks that the prop engine proof is closed w.r.t. the given assertions and
    * previously registered assertions in d_assertions.
@@ -270,6 +278,12 @@ class PropPfManager : protected EnvObj
   context::CDHashSet<Node> d_inputClauses;
   /** Asserted clauses derived from lemmas */
   context::CDHashSet<Node> d_lemmaClauses;
+  /** Are we tracking inference identifiers? */
+  bool d_trackLemmaClauseIds;
+  /** Mapping lemma clauses to inference identifiers */
+  context::CDHashMap<Node, theory::InferenceId> d_lemmaClauseIds;
+  /** The current identifier */
+  theory::InferenceId d_currLemmaId;
   /** The current propagation being processed via this class. */
   Node d_currPropagationProcessed;
   /** Temporary, pointer to SAT proof manager */