[proofs] Alethe: Add Alethe Files to be Compiled (#7241)

Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled.
During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3113f03aba3f5594e2930b333e220fa6872bd170..8f574dc82be36435ba2aedb94c734c3e1b52af3f 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -221,6 +221,10 @@ libcvc5_add_sources(
   proof/unsat_core.h
   proof/alethe/alethe_node_converter.cpp
   proof/alethe/alethe_node_converter.h
+  proof/alethe/alethe_post_processor.cpp
+  proof/alethe/alethe_post_processor.h
+  proof/alethe/alethe_proof_rule.cpp
+  proof/alethe/alethe_proof_rule.h
   prop/bv_sat_solver_notify.h
   prop/bvminisat/bvminisat.cpp
   prop/bvminisat/bvminisat.h

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 0225cf24cd5d536cc2525e498913910bddd01006..0ba3ae4137a64dc6d0ba3d53bef82c592ef7d86c 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -15,9 +15,9 @@ name   = "Proof"
 [[option.mode.DOT]]
   name       = "dot"
   help       = "Output DOT proof"
-[[option.mode.VERIT]]
-  name       = "verit"
-  help       = "Output veriT proof"
+[[option.mode.ALETHE]]
+  name       = "alethe"
+  help       = "Output Alethe proof"
 [[option.mode.TPTP]]
   name       = "tptp"
   help       = "Output TPTP proof (work in progress)"

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 312921db42c8e9f93e517466c0be38af3da0eedd..9b94175fa292cd53ec4302db2e4300b100993129 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -150,12 +150,16 @@ bool AletheProofPostprocessCallback::update(Node res,
                                sanitized_args,
                                *cdp);
 
-      Node vp3 = vp1;
-
-      if (args.size() != 1)
+      Node andNode, vp3;
+      if (args.size() == 1)
+      {
+        vp3 = vp1;
+        andNode = args[0];  // F1
+      }
+      else
       {
         // Build vp2i
-        Node andNode = nm->mkNode(kind::AND, args);  // (and F1 ... Fn)
+        andNode = nm->mkNode(kind::AND, args);  // (and F1 ... Fn)
         std::vector<Node> premisesVP2 = {vp1};
         std::vector<Node> notAnd = {d_cl, children[0]};  // cl F
         Node vp2_i;
@@ -178,8 +182,7 @@ bool AletheProofPostprocessCallback::update(Node res,
         success &=
             addAletheStep(AletheRule::REORDER, vp2b, vp2b, {vp2a}, {}, *cdp);
 
-        Node vp3 =
-            nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]);
+        vp3 = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]);
         success &= addAletheStep(
             AletheRule::DUPLICATED_LITERALS, vp3, vp3, {vp2b}, {}, *cdp);
       }
@@ -288,6 +291,43 @@ bool AletheProofPostprocessCallback::addAletheStepFromOr(
   return addAletheStep(rule, res, conclusion, children, args, cdp);
 }
 
+AletheProofPostprocessFinalCallback::AletheProofPostprocessFinalCallback(
+    ProofNodeManager* pnm, AletheNodeConverter& anc)
+    : d_pnm(pnm), d_anc(anc)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  d_cl = nm->mkBoundVar("cl", nm->sExprType());
+}
+
+bool AletheProofPostprocessFinalCallback::shouldUpdate(
+    std::shared_ptr<ProofNode> pn,
+    const std::vector<Node>& fa,
+    bool& continueUpdate)
+{
+  return false;
+}
+
+bool AletheProofPostprocessFinalCallback::update(
+    Node res,
+    PfRule id,
+    const std::vector<Node>& children,
+    const std::vector<Node>& args,
+    CDProof* cdp,
+    bool& continueUpdate)
+{
+  return true;
+}
+
+AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm,
+                                               AletheNodeConverter& anc)
+    : d_pnm(pnm), d_cb(d_pnm, anc), d_fcb(d_pnm, anc)
+{
+}
+
+AletheProofPostprocess::~AletheProofPostprocess() {}
+
+void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {}
+
 }  // namespace proof
 
 }  // namespace cvc5

diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
index d8fae8a5543de68a5a7534ce5d5ff8c05ab26d15..4a7d8cf61ad661b08c7a3f50d6691c23ecb4d6ce 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.h
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -16,9 +16,9 @@
 #ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
 #define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
 
-#include "proof/proof_node_updater.h"
 #include "proof/alethe/alethe_node_converter.h"
 #include "proof/alethe/alethe_proof_rule.h"
+#include "proof/proof_node_updater.h"
 
 namespace cvc5 {
 
@@ -118,8 +118,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 {
  public:
-   AletheProofPostprocessFinalCallback(ProofNodeManager* pnm,
-                                       AletheNodeConverter& anc);
+  AletheProofPostprocessFinalCallback(ProofNodeManager* pnm,
+                                      AletheNodeConverter& anc);
   ~AletheProofPostprocessFinalCallback() {}
   /** Should proof pn be updated? It should, if the last step is printed as (cl
    * false) or if it is an assumption (in that case it is printed as false).
@@ -159,7 +159,7 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocess
 {
  public:
-   AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
+  AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
   ~AletheProofPostprocess();
   /** post-process */
   void process(std::shared_ptr<ProofNode> pf);

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 5cf5dc0f8b12eed41867afae876699b1bb3e7379..d4e763fe675b3818f2108b80fb82effca272ebbd 100644 (file)
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -202,6 +202,7 @@ const char* toString(PfRule id)
     case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
     //================================================= External rules
     case PfRule::LFSC_RULE: return "LFSC_RULE";
+    case PfRule::ALETHE_RULE: return "ALETHE_RULE";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index bb677bdb97622e7398924a3f4713715b9e3aeeba..25bbf3d344bc059be472227561bc52c5684dbf02 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -1406,6 +1406,15 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (Q)
   LFSC_RULE,
+  //================================================ Place holder for Alethe
+  // rules
+  // ======== Alethe rule
+  // Children: (P1 ... Pn)
+  // Arguments: (id, Q, Q', A1, ..., Am)
+  // ---------------------
+  // Conclusion: (Q)
+  // where Q' is the representation of Q to be printed by the Alethe printer.
+  ALETHE_RULE,
 
   //================================================= Unknown rule
   UNKNOWN,

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 4d6e2b4958a55a606a7e7c40699417f336613232..d5e07991a520faa9eaed2b82bce4c2d86e259428 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -19,6 +19,8 @@
 #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"
 #include "proof/dot/dot_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_algorithm.h"
@@ -60,13 +62,13 @@ PfManager::PfManager(Env& env)
   // where A is an available assumption from outside the scope (note
   // that B1 was an assumption of this SCOPE subproof but since it could
   // be inferred from A, it was updated). This shape is problematic for
-  // the veriT reconstruction, so we disable the update of scoped
+  // the Alethe reconstruction, so we disable the update of scoped
   // assumptions (which would disable the update of B1 in this case).
   d_pfpp.reset(new ProofPostproccess(
       env,
       d_pppg.get(),
       nullptr,
-      options::proofFormatMode() != options::ProofFormatMode::VERIT));
+      options::proofFormatMode() != options::ProofFormatMode::ALETHE));
 
   // add rules to eliminate here
   if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
@@ -171,6 +173,12 @@ void PfManager::printProof(std::ostream& out,
     proof::DotPrinter dotPrinter;
     dotPrinter.print(out, fp.get());
   }
+  else if (options::proofFormatMode() == options::ProofFormatMode::ALETHE)
+  {
+    proof::AletheNodeConverter anc;
+    proof::AletheProofPostprocess vpfpp(d_pnm.get(), anc);
+    vpfpp.process(fp);
+  }
   else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
   {
     out << "% SZS output start Proof for " << options().driver.filename