From 1e9c3deaf16c1fefd7d8344b9e6b6ddb9a19756e Mon Sep 17 00:00:00 2001
From: Lachnitt <lachnitt@stanford.edu>
Date: Thu, 23 Sep 2021 15:08:31 -0700
Subject: [PATCH] [proofs] Alethe: Translate THEORY_REWRITE (#7236)

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

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---
 src/proof/alethe/alethe_post_processor.cpp | 167 ++++++++++++++++++++-
 src/theory/builtin/proof_checker.cpp       |   1 +
 2 files changed, 167 insertions(+), 1 deletion(-)

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 9b94175fa..97afbdab0 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -19,6 +19,7 @@
 #include "proof/proof.h"
 #include "proof/proof_checker.h"
 #include "util/rational.h"
+#include "theory/builtin/proof_checker.h"
 
 namespace cvc5 {
 
@@ -149,7 +150,6 @@ bool AletheProofPostprocessCallback::update(Node res,
                                children,
                                sanitized_args,
                                *cdp);
-
       Node andNode, vp3;
       if (args.size() == 1)
       {
@@ -239,6 +239,171 @@ bool AletheProofPostprocessCallback::update(Node res,
 
       return success;
     }
+    // The rule is translated according to the theory id tid and the outermost
+    // connective of the first term in the conclusion F, since F always has the
+    // form (= t1 t2) where t1 is the term being rewritten. This is not an exact
+    // translation but should work in most cases.
+    //
+    // E.g. if F is (= (* 0 d) 0) and tid = THEORY_ARITH, then prod_simplify
+    // is correctly guessed as the rule.
+    case PfRule::THEORY_REWRITE:
+    {
+      AletheRule vrule = AletheRule::UNDEFINED;
+      Node t = res[0];
+
+      theory::TheoryId tid;
+      if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid))
+      {
+        return addAletheStep(
+            vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp);
+      }
+      switch (tid)
+      {
+        case theory::TheoryId::THEORY_BUILTIN:
+        {
+          switch (t.getKind())
+          {
+            case kind::ITE:
+            {
+              vrule = AletheRule::ITE_SIMPLIFY;
+              break;
+            }
+            case kind::EQUAL:
+            {
+              vrule = AletheRule::EQ_SIMPLIFY;
+              break;
+            }
+            case kind::AND:
+            {
+              vrule = AletheRule::AND_SIMPLIFY;
+              break;
+            }
+            case kind::OR:
+            {
+              vrule = AletheRule::OR_SIMPLIFY;
+              break;
+            }
+            case kind::NOT:
+            {
+              vrule = AletheRule::NOT_SIMPLIFY;
+              break;
+            }
+            case kind::IMPLIES:
+            {
+              vrule = AletheRule::IMPLIES_SIMPLIFY;
+              break;
+            }
+            case kind::WITNESS:
+            {
+              vrule = AletheRule::QNT_SIMPLIFY;
+              break;
+            }
+            default:
+            {
+              // In this case the rule is undefined
+            }
+          }
+          break;
+        }
+        case theory::TheoryId::THEORY_BOOL:
+        {
+          vrule = AletheRule::BOOL_SIMPLIFY;
+          break;
+        }
+        case theory::TheoryId::THEORY_UF:
+        {
+          if (t.getKind() == kind::EQUAL)
+          {
+            // A lot of these seem to be symmetry rules but not all...
+            vrule = AletheRule::EQUIV_SIMPLIFY;
+          }
+          break;
+        }
+        case theory::TheoryId::THEORY_ARITH:
+        {
+          switch (t.getKind())
+          {
+            case kind::DIVISION:
+            {
+              vrule = AletheRule::DIV_SIMPLIFY;
+              break;
+            }
+            case kind::PRODUCT:
+            {
+              vrule = AletheRule::PROD_SIMPLIFY;
+              break;
+            }
+            case kind::MINUS:
+            {
+              vrule = AletheRule::MINUS_SIMPLIFY;
+              break;
+            }
+            case kind::UMINUS:
+            {
+              vrule = AletheRule::UNARY_MINUS_SIMPLIFY;
+              break;
+            }
+            case kind::PLUS:
+            {
+              vrule = AletheRule::SUM_SIMPLIFY;
+              break;
+            }
+            case kind::MULT:
+            {
+              vrule = AletheRule::PROD_SIMPLIFY;
+              break;
+            }
+            case kind::EQUAL:
+            {
+              vrule = AletheRule::EQUIV_SIMPLIFY;
+              break;
+            }
+            case kind::LT:
+            {
+              [[fallthrough]];
+            }
+            case kind::GT:
+            {
+              [[fallthrough]];
+            }
+            case kind::GEQ:
+            {
+              [[fallthrough]];
+            }
+            case kind::LEQ:
+            {
+              vrule = AletheRule::COMP_SIMPLIFY;
+              break;
+            }
+            case kind::CAST_TO_REAL:
+            {
+              return addAletheStep(AletheRule::LA_GENERIC,
+                                   res,
+                                   nm->mkNode(kind::SEXPR, d_cl, res),
+                                   children,
+                                   {nm->mkConst(Rational(1))},
+                                   *cdp);
+            }
+            default:
+            {
+              // In this case the rule is undefined
+            }
+          }
+          break;
+        }
+        case theory::TheoryId::THEORY_QUANTIFIERS:
+        {
+          vrule = AletheRule::QUANTIFIER_SIMPLIFY;
+          break;
+        }
+        default:
+        {
+          // In this case the rule is undefined
+        };
+      }
+      return addAletheStep(
+          vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 1309a05f9..d5b856456 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -57,6 +57,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3);
   pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3);
+  pc->registerChecker(PfRule::ALETHE_RULE, this);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
-- 
2.30.2