From: Lachnitt <lachnitt@stanford.edu>
Date: Wed, 10 Nov 2021 12:16:55 +0000 (-0800)
Subject: [proofs] Alethe: Translate INSTANTIATE rule  (#7607)
X-Git-Tag: cvc5-1.0.0~835
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f8d59391ecf0272db184624e4e44ee13241c6bd;p=cvc5.git

[proofs] Alethe: Translate INSTANTIATE rule  (#7607)

Implementation of the translation of INSTANTIATE rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index c97dc2313..01278134f 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -1363,6 +1363,41 @@ bool AletheProofPostprocessCallback::update(Node res,
                               {},
                               *cdp);
     }
+    //================================================= Quantifiers rules
+    // ======== Instantiate
+    // See proof_rule.h for documentation on the INSTANTIATE rule. This
+    // comment uses variable names as introduced there.
+    //
+    // ----- FORALL_INST, (= x1 t1) ... (= xn tn)
+    //  VP1
+    // ----- OR
+    //  VP2              P
+    // -------------------- RESOLUTION
+    //     (cl F*sigma)^
+    //
+    // VP1: (cl (or (not (forall ((x1 T1) ... (xn Tn)) F*sigma)
+    // VP2: (cl (not (forall ((x1 T1) ... (xn Tn)) F)) F*sigma)
+    //
+    // ^ the corresponding proof node is F*sigma
+    case PfRule::INSTANTIATE:
+    {
+      for (size_t i = 0, size = children[0][0].getNumChildren(); i < size; i++)
+      {
+        new_args.push_back(children[0][0][i].eqNode(args[i]));
+      }
+      Node vp1 = nm->mkNode(
+          kind::SEXPR, d_cl, nm->mkNode(kind::OR, children[0].notNode(), res));
+      Node vp2 = nm->mkNode(kind::SEXPR, d_cl, children[0].notNode(), res);
+      return addAletheStep(
+                 AletheRule::FORALL_INST, vp1, vp1, {}, new_args, *cdp)
+             && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp)
+             && addAletheStep(AletheRule::RESOLUTION,
+                              res,
+                              nm->mkNode(kind::SEXPR, d_cl, res),
+                              {vp2, children[0]},
+                              {},
+                              *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,