More

src/CMakeLists.txt

@@ -167,6 +167,8 @@ libcvc5_add_sources(
   proof/conv_seq_proof_generator.cpp
   proof/conv_seq_proof_generator.h
   proof/clause_id.h
+  proof/diamonds_proof_generator.cpp
+  proof/diamonds_proof_generator.h
   proof/dot/dot_printer.cpp
   proof/dot/dot_printer.h
   proof/eager_proof_generator.cpp

src/preprocessing/passes/static_learning.cpp

@@ -60,7 +60,7 @@ PreprocessingPassResult StaticLearning::applyInternal(
     // add the lemmas to the end
     for (const TrustNode& trn : tlems)
     {
-      assertionsToPreprocess->pushBackTrusted(trn);
+      assertionsToPreprocess->pushBackTrusted(trn, TrustId::PREPROCESS_STATIC_LEARNING_LEMMA);
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;

src/proof/diamonds_proof_generator.cpp

@@ -0,0 +1,42 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 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.
+ * ****************************************************************************
+ *
+ * Valid witness proof generator utility.
+ */
+
+#include "proof/diamonds_proof_generator.h"
+
+#include "proof/proof.h"
+
+namespace cvc5::internal {
+
+DiamondsProofGenerator::DiamondsProofGenerator(Env& env) : EnvObj(env)
+{
+}
+
+DiamondsProofGenerator::~DiamondsProofGenerator() {}
+
+std::shared_ptr<ProofNode> DiamondsProofGenerator::getProofFor(Node fact)
+{
+  Trace("valid-witness") << "Prove " << fact << std::endl;
+  // proofs not yet supported
+  CDProof cdp(d_env);
+  cdp.addTrustedStep(fact, TrustId::DIAMONDS, {}, {});
+  return cdp.getProofFor(fact);
+}
+
+std::string DiamondsProofGenerator::identify() const
+{
+  return "DiamondsProofGenerator";
+}
+
+}  // namespace cvc5::internal

src/proof/diamonds_proof_generator.h

@@ -0,0 +1,52 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 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.
+ * ****************************************************************************
+ *
+ * Diamonds proof generator utility.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__DIAMONDS_PROOF_GENERATOR_H
+#define CVC5__PROOF__DIAMONDS_PROOF_GENERATOR_H
+
+#include "proof/method_id.h"
+#include "proof/proof_generator.h"
+#include "smt/env_obj.h"
+
+namespace cvc5::internal {
+
+class ProofNode;
+class ProofNodeManager;
+
+/**
+ * Proof generator expected to prove (exists x. P) for all witness terms
+ * (witness x. P) introduced.
+ */
+class DiamondsProofGenerator : protected EnvObj, public ProofGenerator
+{
+ public:
+  /**
+   * @param env Reference to the environment
+   */
+  DiamondsProofGenerator(Env& env);
+  virtual ~DiamondsProofGenerator();
+  /**
+   * Get proof for fact.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
+  /** identify */
+  std::string identify() const override;
+};
+
+}  // namespace cvc5::internal
+
+#endif /* CVC5__PROOF__DIAMONDS_PROOF_GENERATOR_H */

src/proof/trust_id.cpp

@@ -43,8 +43,8 @@ const char* toString(TrustId id)
     case TrustId::PREPROCESS_ACKERMANN: return "PREPROCESS_ACKERMANN";
     case TrustId::PREPROCESS_ACKERMANN_LEMMA:
       return "PREPROCESS_ACKERMANN_LEMMA";
-    case TrustId::PREPROCESS_STATIC_LEARNING:
-      return "PREPROCESS_STATIC_LEARNING";
+    case TrustId::PREPROCESS_STATIC_LEARNING_LEMMA:
+      return "PREPROCESS_STATIC_LEARNING_LEMMA";
     case TrustId::PREPROCESS_HO_ELIM: return "PREPROCESS_HO_ELIM";
     case TrustId::PREPROCESS_HO_ELIM_LEMMA: return "PREPROCESS_HO_ELIM_LEMMA";
     case TrustId::PREPROCESS_BITVECTOR_EAGER_ATOMS:
@@ -71,6 +71,7 @@ const char* toString(TrustId id)
     case TrustId::ARITH_DIO_LEMMA: return "ARITH_DIO_LEMMA";
     case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM:
       return "ARITH_NL_COMPARE_LIT_TRANSFORM";
+    case TrustId::DIAMONDS: return "DIAMONDS";
     case TrustId::EXT_THEORY_REWRITE: return "EXT_THEORY_REWRITE";
     case TrustId::REWRITE_NO_ELABORATE: return "REWRITE_NO_ELABORATE";
     case TrustId::FLATTENING_REWRITE: return "FLATTENING_REWRITE";

src/proof/trust_id.h

@@ -53,7 +53,7 @@ enum class TrustId : uint32_t
   PREPROCESS_ACKERMANN,
   PREPROCESS_ACKERMANN_LEMMA,
   /** StaticLearning preprocessing pass */
-  PREPROCESS_STATIC_LEARNING,
+  PREPROCESS_STATIC_LEARNING_LEMMA,
   /** HoElim preprocessing pass */
   PREPROCESS_HO_ELIM,
   PREPROCESS_HO_ELIM_LEMMA,
@@ -133,6 +133,8 @@ enum class TrustId : uint32_t
    * values as used by ProofRule::ARITH_MULT_ABS_COMPARISON.
    */
   ARITH_NL_COMPARE_LIT_TRANSFORM,
+  /** Diamonds */
+  DIAMONDS,
   /** An extended theory rewrite */
   EXT_THEORY_REWRITE,
   /** A rewrite whose proof could not be elaborated */

src/theory/uf/theory_uf.cpp

@@ -63,6 +63,11 @@ TheoryUF::TheoryUF(Env& env,
   // indicate we are using the default theory state and inference managers
   d_theoryState = &d_state;
   d_inferManager = &d_im;
+
+  if (env.isTheoryProofProducing())
+  {
+    d_dpfgen.reset(new DiamondsProofGenerator(env));
+  }
 }
 
 TheoryUF::~TheoryUF() {
@@ -548,7 +553,7 @@ void TheoryUF::ppStaticLearn(TNode n, std::vector<TrustNode>& learned)
         Node newEquality = a.eqNode(d);
         Trace("diamonds") << "  ==> " << newEquality << endl;
         Node lem = n.impNode(newEquality);
-        TrustNode trn = TrustNode::mkTrustLemma(lem, nullptr);
+        TrustNode trn = TrustNode::mkTrustLemma(lem, d_dpfgen.get());
         learned.emplace_back(trn);
       } else {
         Trace("diamonds") << "+ C fails" << endl;

src/theory/uf/theory_uf.h

@@ -26,6 +26,7 @@
 #include "theory/uf/proof_checker.h"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
+#include "proof/diamonds_proof_generator.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -80,6 +81,8 @@ class TheoryUF : public Theory {
   std::unique_ptr<HoExtension> d_ho;
   /** the conversions solver */
   std::unique_ptr<ConversionsSolver> d_csolver;
+  /** Diamonds proof generator */
+  std::unique_ptr<DiamondsProofGenerator> d_dpfgen;
 
   /** node for true */
   Node d_true;