Add default proof logger to log cpc proofs (cvc5#11511)

This adds the default implementation of a proof logger (for cpc proofs).

It also adds some logic to ensure proof logging is used only in valid
configurations.

src/options/proof_options.toml

@@ -245,3 +245,11 @@ name   = "Proof"
   type       = "bool"
   default    = "true"
   help       = "Whether to allow trust in the proof printer (when applicable)"
+
+[[option]]
+  name       = "proofLog"
+  category   = "expert"
+  long       = "proof-log"
+  type       = "bool"
+  default    = "false"
+  help       = "Proof logging mode"

src/proof/trust_id.cpp

@@ -27,6 +27,7 @@ const char* toString(TrustId id)
   switch (id)
   {
     case TrustId::NONE: return "NONE";
+    case TrustId::PREPROCESSED_INPUT: return "PREPROCESSED_INPUT";
     // core
     case TrustId::THEORY_LEMMA: return "THEORY_LEMMA";
     case TrustId::THEORY_INFERENCE_ARITH: return "THEORY_INFERENCE_ARITH";

src/proof/trust_id.h

@@ -28,6 +28,8 @@ namespace cvc5::internal {
 enum class TrustId : uint32_t
 {
   NONE,
+  /** Assertions of the preprocessed input clauses */
+  PREPROCESSED_INPUT,
   /** A lemma sent by a theory without a proof */
   THEORY_LEMMA,
   /**

src/smt/proof_logger.cpp

@@ -21,5 +21,116 @@
 
 namespace cvc5::internal {
 
+ProofLoggerCpc::ProofLoggerCpc(Env& env,
+                               std::ostream& out,
+                               smt::PfManager* pm,
+                               smt::Assertions& as,
+                               smt::ProofPostprocess* ppp)
+    : ProofLogger(env),
+      d_pm(pm),
+      d_pnm(pm->getProofNodeManager()),
+      d_as(as),
+      d_ppp(ppp),
+      d_atp(nodeManager()),
+      // we use thresh 1 since terms may come incrementally and would benefit
+      // from previous eager letification
+      d_alfp(env, d_atp, pm->getRewriteDatabase(), 1),
+      d_aout(out, d_alfp.getLetBinding(), "@t", false)
+{
+  Trace("pf-log-debug") << "Make proof logger" << std::endl;
+  // global options on out
+  options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
+  options::ioutils::applyPrintArithLitToken(out, true);
+  options::ioutils::applyPrintSkolemDefinitions(out, true);
+}
+
+ProofLoggerCpc::~ProofLoggerCpc() {}
+
+void ProofLoggerCpc::logCnfPreprocessInputs(const std::vector<Node>& inputs)
+{
+  d_aout.getOStream() << "; log start" << std::endl;
+  Trace("pf-log") << "; log: cnf preprocess input proof start" << std::endl;
+  CDProof cdp(d_env);
+  Node conc = nodeManager()->mkAnd(inputs);
+  cdp.addTrustedStep(conc, TrustId::PREPROCESSED_INPUT, inputs, {});
+  std::shared_ptr<ProofNode> pfn = cdp.getProofFor(conc);
+  ProofScopeMode m = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS;
+  d_ppProof = d_pm->connectProofToAssertions(pfn, d_as, m);
+  d_alfp.print(d_aout, d_ppProof, m);
+  Trace("pf-log") << "; log: cnf preprocess input proof end" << std::endl;
+}
+
+void ProofLoggerCpc::logCnfPreprocessInputProofs(
+    std::vector<std::shared_ptr<ProofNode>>& pfns)
+{
+  Trace("pf-log") << "; log: cnf preprocess input proof start" << std::endl;
+  // if the assertions are empty, we do nothing. We will answer sat.
+  std::shared_ptr<ProofNode> pfn;
+  if (!pfns.empty())
+  {
+    if (pfns.size() == 1)
+    {
+      pfn = pfns[0];
+    }
+    else
+    {
+      pfn = d_pnm->mkNode(ProofRule::AND_INTRO, pfns, {});
+    }
+    ProofScopeMode m = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS;
+    d_ppProof = d_pm->connectProofToAssertions(pfn, d_as, m);
+    d_alfp.print(d_aout, d_ppProof, m);
+  }
+  Trace("pf-log") << "; log: cnf preprocess input proof end" << std::endl;
+}
+
+void ProofLoggerCpc::logTheoryLemmaProof(std::shared_ptr<ProofNode>& pfn)
+{
+  Trace("pf-log") << "; log theory lemma proof start " << pfn->getResult()
+                  << std::endl;
+  d_lemmaPfs.emplace_back(pfn);
+  d_alfp.printNext(d_aout, pfn);
+  Trace("pf-log") << "; log theory lemma proof end" << std::endl;
+}
+
+void ProofLoggerCpc::logTheoryLemma(const Node& n)
+{
+  Trace("pf-log") << "; log theory lemma start " << n << std::endl;
+  std::shared_ptr<ProofNode> ptl =
+      d_pnm->mkTrustedNode(TrustId::THEORY_LEMMA, {}, {}, n);
+  d_lemmaPfs.emplace_back(ptl);
+  d_alfp.printNext(d_aout, ptl);
+  Trace("pf-log") << "; log theory lemma end" << std::endl;
+}
+
+void ProofLoggerCpc::logSatRefutation()
+{
+  Trace("pf-log") << "; log SAT refutation start" << std::endl;
+  std::vector<std::shared_ptr<ProofNode>> premises;
+  Assert(d_ppProof->getRule() == ProofRule::SCOPE);
+  Assert(d_ppProof->getChildren()[0]->getRule() == ProofRule::SCOPE);
+  std::shared_ptr<ProofNode> ppBody =
+      d_ppProof->getChildren()[0]->getChildren()[0];
+  premises.emplace_back(ppBody);
+  premises.insert(premises.end(), d_lemmaPfs.begin(), d_lemmaPfs.end());
+  Node f = nodeManager()->mkConst(false);
+  std::shared_ptr<ProofNode> psr =
+      d_pnm->mkNode(ProofRule::SAT_REFUTATION, premises, {}, f);
+  d_alfp.printNext(d_aout, psr);
+  Trace("pf-log") << "; log SAT refutation end" << std::endl;
+  // for now, to avoid checking failure
+  d_aout.getOStream() << "(exit)" << std::endl;
+}
+
+void ProofLoggerCpc::logSatRefutationProof(std::shared_ptr<ProofNode>& pfn)
+{
+  Trace("pf-log") << "; log SAT refutation proof start" << std::endl;
+  // connect to preprocessed
+  std::shared_ptr<ProofNode> spf =
+      d_pm->connectProofToAssertions(pfn, d_as, ProofScopeMode::NONE);
+  d_alfp.printNext(d_aout, spf);
+  Trace("pf-log") << "; log SAT refutation proof end" << std::endl;
+  // for now, to avoid checking failure
+  d_aout.getOStream() << "(exit)" << std::endl;
+}
 
 }  // namespace cvc5::internal

src/smt/proof_logger.h

@@ -18,11 +18,19 @@
 #ifndef CVC5__SMT__PROOF_LOGGER_H
 #define CVC5__SMT__PROOF_LOGGER_H
 
+#include "proof/alf/alf_node_converter.h"
+#include "proof/alf/alf_printer.h"
 #include "proof/proof_node.h"
 #include "smt/env_obj.h"
 
 namespace cvc5::internal {
 
+namespace smt {
+class Assertions;
+class PfManager;
+class ProofPostprocess;
+}  // namespace smt
+
 /**
  * The purpose of this class is to output proofs for all reasoning the solver
  * does on-the-fly. It is enabled when proof logging is enabled.
@@ -88,6 +96,58 @@ class ProofLogger : protected EnvObj
   virtual void logSatRefutationProof(std::shared_ptr<ProofNode>& pfn) {}
 };
 
+/**
+ * The default implementation of a proof logger, which prints proofs in the
+ * CPC format.
+ */
+class ProofLoggerCpc : public ProofLogger
+{
+ public:
+  /** */
+  ProofLoggerCpc(Env& env,
+                 std::ostream& out,
+                 smt::PfManager* pm,
+                 smt::Assertions& as,
+                 smt::ProofPostprocess* ppp);
+  ~ProofLoggerCpc();
+  /** Log preprocessing input */
+  void logCnfPreprocessInputs(const std::vector<Node>& inputs) override;
+  /** Log preprocessing input proof */
+  void logCnfPreprocessInputProofs(
+      std::vector<std::shared_ptr<ProofNode>>& pfns) override;
+  /** Log theory lemma */
+  void logTheoryLemma(const Node& n) override;
+  /** Log theory lemma proof */
+  void logTheoryLemmaProof(std::shared_ptr<ProofNode>& pfn) override;
+  /** Log SAT refutation */
+  void logSatRefutation() override;
+  /** Log SAT refutation proof */
+  void logSatRefutationProof(std::shared_ptr<ProofNode>& pfn) override;
+
+ private:
+  /** Pointer to the proof manager, for connecting proofs to inputsw */
+  smt::PfManager* d_pm;
+  /** Pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
+  /** Reference to the assertions of SMT solver */
+  smt::Assertions& d_as;
+  /** Pointer to the proof post-processor */
+  smt::ProofPostprocess* d_ppp;
+  /** The node converter, used for printing */
+  proof::AlfNodeConverter d_atp;
+  /** The proof printer */
+  proof::AlfPrinter d_alfp;
+  /** The output channel we are using */
+  proof::AlfPrintChannelOut d_aout;
+  /** The preprocessing proof we were notified of, which we may have created */
+  std::shared_ptr<ProofNode> d_ppProof;
+  /**
+   * The list of theory lemma proofs we were notified of, which we may have
+   * created.
+   */
+  std::vector<std::shared_ptr<ProofNode>> d_lemmaPfs;
+};
+
 }  // namespace cvc5::internal
 
 #endif /* CVC5__PROOF__PROOF_LOGGER_H */

src/smt/proof_manager.cpp

@@ -166,7 +166,8 @@ constexpr typename std::vector<T, Alloc>::size_type erase_if(
 
 void PfManager::startProofLogging(std::ostream& out, Assertions& as)
 {
-  Unimplemented() << "Not yet implemented" << std::endl;
+  // by default, CPC proof logger
+  d_plog.reset(new ProofLoggerCpc(d_env, out, this, as, d_pfpp.get()));
 }
 
 std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(

src/smt/set_defaults.cpp

@@ -212,6 +212,11 @@ void SetDefaults::setDefaultsPre(Options& opts)
         options::ProofGranularityMode::DSL_REWRITE,
         "check-proof-steps");
   }
+  if (opts.driver.dumpProofs)
+  {
+    // should not combine this with proof logging
+    OPTION_EXCEPTION_IF_NOT(proof, proofLog, false, "dump proofs");
+  }
   // if check-proofs, dump-proofs, dump-unsat-cores-lemmas, or proof-mode=full,
   // then proofs being fully enabled is implied
   if (opts.smt.checkProofs || opts.driver.dumpProofs
@@ -315,6 +320,16 @@ void SetDefaults::setDefaultsPre(Options& opts)
             smt, proofMode, options::ProofMode::PP_ONLY, "produce difficulty");
       }
     }
+    if (opts.proof.proofLog)
+    {
+      SET_AND_NOTIFY(smt, produceProofs, true, "proof logging");
+      // ensure at least preprocessing proofs are enabled
+      if (opts.smt.proofMode == options::ProofMode::OFF)
+      {
+        SET_AND_NOTIFY_VAL_SYM(
+            smt, proofMode, options::ProofMode::PP_ONLY, "proof logging");
+      }
+    }
     // if proofs weren't enabled by user, and we are producing unsat cores
     if (opts.smt.produceUnsatCores)
     {
@@ -356,6 +371,14 @@ void SetDefaults::setDefaultsPre(Options& opts)
           smt, proofMode, options::ProofMode::FULL_STRICT, "safe options");
     }
   }
+  if (opts.proof.proofLog)
+  {
+    // incompatible with sygus-inst
+    if (opts.quantifiers.sygusInst)
+    {
+      throw OptionException(std::string("Cannot log proofs with sygus-inst"));
+    }
+  }
 
   // if unsat cores are disabled, then unsat cores mode should be OFF. Similarly
   // for proof mode.
@@ -1250,6 +1273,13 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
     reason << "compute partitions";
     return true;
   }
+  // proof logging not yet supported in incremental mode, which requires
+  // managing how new assertions are printed.
+  if (opts.proof.proofLog)
+  {
+    reason << "proof logging";
+    return true;
+  }
 
   // disable modes not supported by incremental
   SET_AND_NOTIFY(smt, sortInference, false, "incremental solving");
@@ -1890,6 +1920,7 @@ void SetDefaults::disableChecking(Options& opts)
   opts.write_smt().debugCheckModels = false;
   opts.write_smt().checkModels = false;
   opts.write_proof().checkProofSteps = false;
+  opts.write_proof().proofLog = false;
 }
 
 }  // namespace smt

src/smt/smt_solver.cpp

@@ -83,6 +83,16 @@ void SmtSolver::finishInit()
   d_theoryEngine->finishInit();
   d_propEngine->finishInit();
   finishInitPreprocessor();
+
+  if (options().proof.proofLog)
+  {
+    smt::PfManager* pm = d_env.getProofManager();
+    if (pm != nullptr)
+    {
+      // Logs proofs on the base output stream of the solver
+      pm->startProofLogging(options().base.out, d_asserts);
+    }
+  }
 }
 
 void SmtSolver::resetAssertions()