fixes

HanielB · Jan 30, 2025 · 57e112b · 57e112b
1 parent 14f54d8
commit 57e112b
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 8 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -2546,7 +2546,7 @@ bool AletheProofPostprocessCallback::ensureFinalStep(
   NodeManager* nm = nodeManager();
   Node res = pf->getResult();
   // Convert if conclusion is (cl false) or
-  // if it's a false assumption
+  // if it's a false assumption.
   //
   //   ...
   // -------------------    ---------------------- false
@@ -2681,10 +2681,17 @@ const std::string& AletheProofPostprocess::getError()
   return d_reasonForConversionFailure;
 }
 
-bool AletheProofPostprocess::processInnerProof(std::shared_ptr<ProofNode> pf)
+bool AletheProofPostprocess::processInnerProof(std::shared_ptr<ProofNode>& pf,
+                                               bool ensureFinalStep)
 {
   ProofNodeUpdater updater(d_env, d_cb, false, false);
   updater.process(pf);
+  if (ensureFinalStep && !d_cb.ensureFinalStep(pf))
+  {
+    std::stringstream ss;
+    ss << "\"Proof unsupported by Alethe: could not process final step\"";
+    d_reasonForConversionFailure = ss.str();
+  }
   return d_reasonForConversionFailure.empty();
 }
 

diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
@@ -169,10 +169,14 @@ class AletheProofPostprocess : protected EnvObj
    * If the conversion is possible, true is returned. Otherwise, false. The
    * conversion may fail if the proof contains unsupported elements in the
    * Alethe proof calculus, such as uncategorized Skolems.
+   *
+   * If `ensureFinalStep` is true, this method will make sure the conclusion of
+   * the final step in the empty clause.
    */
   bool process(std::shared_ptr<ProofNode> pf);
 
-  bool processInnerProof(std::shared_ptr<ProofNode> pf);
+  bool processInnerProof(std::shared_ptr<ProofNode>& pf,
+                         bool ensureFinalStep = false);
 
   /** Retrieve the saved error message, if any. */
   const std::string& getError();

diff --git a/src/proof/alethe/alethe_proof_logger.cpp b/src/proof/alethe/alethe_proof_logger.cpp
@@ -48,14 +48,16 @@ AletheProofLogger::AletheProofLogger(Env& env,
 
 AletheProofLogger::~AletheProofLogger() {}
 
-void AletheProofLogger::printPfNodeAlethe(std::shared_ptr<ProofNode> pfn, bool inner)
+void AletheProofLogger::printPfNodeAlethe(std::shared_ptr<ProofNode> pfn,
+                                          bool inner,
+                                          bool finalStep)
 {
   options::ProofCheckMode oldMode = options().proof.proofCheck;
   d_pnm->getChecker()->setProofCheckMode(options::ProofCheckMode::NONE);
   std::map<Node, std::string> assertionNames;
   if (inner)
   {
-    if (d_appproc.processInnerProof(pfn))
+    if (d_appproc.processInnerProof(pfn, finalStep))
     {
       d_apprinter.printProofNode(d_out, pfn);
     }
@@ -119,7 +121,17 @@ void AletheProofLogger::logCnfPreprocessInputProofs(
     }
     ProofScopeMode m = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS;
     d_ppProof = d_pm->connectProofToAssertions(pfn, d_as, m);
+    if (TraceIsOn("alethe-pf-log-debug"))
+    {
+      d_ppProof->printDebug(d_out, true);
+      d_out << "\n";
+    }
     printPfNodeAlethe(d_ppProof);
+    if (TraceIsOn("alethe-pf-log-debug"))
+    {
+      d_ppProof->printDebug(d_out, true);
+      d_out << "\n";
+    }
   }
   Trace("alethe-pf-log") << "; log: cnf preprocess input proof end" << std::endl;
 }
@@ -169,7 +181,7 @@ void AletheProofLogger::logSatRefutation()
   Node f = nodeManager()->mkConst(false);
   std::shared_ptr<ProofNode> psr =
       d_pnm->mkNode(ProofRule::SAT_REFUTATION, premises, {}, f);
-  printPfNodeAlethe(psr, true);
+  printPfNodeAlethe(psr, true, true);
   Trace("alethe-pf-log") << "; log SAT refutation end" << std::endl;
 }
 
@@ -183,7 +195,7 @@ void AletheProofLogger::logSatRefutationProof(std::shared_ptr<ProofNode>& pfn)
   // connect to preprocessed
   std::shared_ptr<ProofNode> spf =
       d_pm->connectProofToAssertions(pfn, d_as, ProofScopeMode::NONE);
-  printPfNodeAlethe(spf, true);
+  printPfNodeAlethe(spf, true, true);
   Trace("alethe-pf-log") << "; log SAT refutation proof end" << std::endl;
 }
 

diff --git a/src/proof/alethe/alethe_proof_logger.h b/src/proof/alethe/alethe_proof_logger.h
@@ -54,7 +54,9 @@ class AletheProofLogger : public ProofLogger
   void logSatRefutationProof(std::shared_ptr<ProofNode>& pfn) override;
 
   /** Translate the proof node to Alethe and print it. */
-  void printPfNodeAlethe(std::shared_ptr<ProofNode> pfn, bool inner = false);
+  void printPfNodeAlethe(std::shared_ptr<ProofNode> pfn,
+                         bool inner = false,
+                         bool finalStep = false);
 
  private:
   /** The output stream */