From: Lachnitt <lachnitt@stanford.edu>
Date: Thu, 17 Feb 2022 18:08:46 +0000 (-0800)
Subject: [proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100)
X-Git-Tag: cvc5-1.0.0~420
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e97f9447ed646d4a15ba1c107fa8a0f94165353b;p=cvc5.git

[proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100)

Instead of printing "trust" in the case of a simplification rule that cannot be translated to an Alethe simplify rule print "all_simplify". This also replaces the heuristic in THEORY_REWRITE to determine which simplify rule is needed.
---

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 759974687..24d17676f 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -324,170 +324,14 @@ 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::RELATION_PRODUCT:
-            {
-              vrule = AletheRule::PROD_SIMPLIFY;
-              break;
-            }
-            case kind::SUB:
-            {
-              vrule = AletheRule::MINUS_SIMPLIFY;
-              break;
-            }
-            case kind::NEG:
-            {
-              vrule = AletheRule::UNARY_MINUS_SIMPLIFY;
-              break;
-            }
-            case kind::ADD:
-            {
-              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->mkConstInt(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);
+    { 
+       return addAletheStep(AletheRule::ALL_SIMPLIFY,
+                           res,
+                           nm->mkNode(kind::SEXPR, d_cl, res),
+                           children,
+                           {},
+                           *cdp);
     }
     // ======== Resolution and N-ary Resolution
     // See proof_rule.h for documentation on the RESOLUTION and CHAIN_RESOLUTION
diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp
index 52a47fe37..313839dec 100644
--- a/src/proof/alethe/alethe_proof_rule.cpp
+++ b/src/proof/alethe/alethe_proof_rule.cpp
@@ -114,6 +114,7 @@ const char* aletheRuleToString(AletheRule id)
     case AletheRule::QNT_SIMPLIFY: return "qnt_simplify";
     case AletheRule::SKO_EX: return "sko_ex";
     case AletheRule::SKO_FORALL: return "sko_forall";
+    case AletheRule::ALL_SIMPLIFY: return "all_simplify";
     case AletheRule::SYMM: return "symm";
     case AletheRule::NOT_SYMM: return "not_symm";
     case AletheRule::REORDERING: return "reordering";
diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h
index 331e38ac6..d9515bd44 100644
--- a/src/proof/alethe/alethe_proof_rule.h
+++ b/src/proof/alethe/alethe_proof_rule.h
@@ -368,6 +368,7 @@ enum class AletheRule : uint32_t
   COMP_SIMPLIFY,
   NARY_ELIM,
   QNT_SIMPLIFY,
+  ALL_SIMPLIFY,
   // ======== let
   // G,x1->F1,...,xn->Fn > j. (= G G')
   // ---------------------------------