more

HanielB · Feb 26, 2024 · 01ca065 · 01ca065
1 parent e33a21b
commit 01ca065
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 5 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -2511,6 +2511,12 @@ bool AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf,
   ProofNodeUpdater updater(d_env, d_cb, false, false);
   updater.process(internalProof);
 
+  if (!d_reasonForConversionFailure.empty())
+  {
+    reasonForConversionFailure = d_reasonForConversionFailure;
+    return false;
+  }
+
   // In the Alethe proof format the final step has to be (cl). However, after
   // the translation it might be (cl false). In that case additional steps are
   // required.
@@ -2536,11 +2542,6 @@ bool AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf,
     d_env.getProofNodeManager()->updateNode(pf.get(), npn.get());
     Trace("pf-process-debug") << "...update node finished." << std::endl;
   }
-  if (!d_reasonForConversionFailure.empty())
-  {
-    reasonForConversionFailure = d_reasonForConversionFailure;
-    return false;
-  }
   return true;
 }
 

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
@@ -141,6 +141,11 @@ Node ProofChecker::checkDebug(ProofRule id,
   return res;
 }
 
+void ProofChecker::setProofCheckMode(options::ProofCheckMode pcMode)
+{
+  d_pcMode = pcMode;
+}
+
 Node ProofChecker::checkInternal(ProofRule id,
                                  const std::vector<Node>& cchildren,
                                  const std::vector<Node>& args,

diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h
@@ -125,6 +125,9 @@ class ProofChecker
    */
   bool isPedanticFailure(ProofRule id, std::ostream* out) const;
 
+  /** Assigns argument pcMode to d_pcMode. */
+  void setProofCheckMode(options::ProofCheckMode pcMode);
+
  private:
   /** statistics class */
   ProofCheckerStatistics d_stats;

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
@@ -17,6 +17,7 @@
 
 #include "options/base_options.h"
 #include "options/main_options.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "proof/alethe/alethe_node_converter.h"
 #include "proof/alethe/alethe_post_processor.h"
@@ -286,6 +287,8 @@ void PfManager::printProof(std::ostream& out,
   }
   else if (mode == options::ProofFormatMode::ALETHE)
   {
+    options::ProofCheckMode oldMode =options().proof.proofCheck;
+    d_pnm->getChecker()->setProofCheckMode(options::ProofCheckMode::NONE);
     std::string reasonForConversionFailure;
     proof::AletheNodeConverter anc;
     proof::AletheProofPostprocess vpfpp(
@@ -299,6 +302,7 @@ void PfManager::printProof(std::ostream& out,
     {
       out << "(error " << reasonForConversionFailure << ")";
     }
+    d_pnm->getChecker()->setProofCheckMode(oldMode);
   }
   else if (mode == options::ProofFormatMode::LFSC)
   {

diff --git a/test/regress/cli/regress0/proofs/open-pf-datatypes.smt2 b/test/regress/cli/regress0/proofs/open-pf-datatypes.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-datatypes ((C 0)) (((r) (b))))
 (declare-datatypes ((P 0)) (((a (f C) (s C)))))

diff --git a/test/regress/cli/regress0/proofs/proj-issue528-ufpfchecker.smt2 b/test/regress/cli/regress0/proofs/proj-issue528-ufpfchecker.smt2
@@ -1,3 +1,5 @@
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_ALL)
 (set-info :status unsat)
 (set-option :check-proofs true)

diff --git a/test/regress/cli/regress0/proofs/proj-issue554.smt2 b/test/regress/cli/regress0/proofs/proj-issue554.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :proof-check eager)
 (set-option :unsat-cores-mode sat-proof)