[alethe] Post-processing ProofRule::TRUST

src/proof/alethe/alethe_post_processor.cpp

@@ -383,13 +383,60 @@ bool AletheProofPostprocessCallback::update(Node res,
 
       return success;
     }
-    case ProofRule::TRUST_THEORY_REWRITE:
-    {
-      return addAletheStep(AletheRule::ALL_SIMPLIFY,
+    // If the trusted rule is a theory lemma from arithmetic, we try to phrase
+    // it with "lia_generic".
+    case ProofRule::TRUST:
+    {
+      // check for case where the trust step is introducing an equality between
+      // a term and another whose Alethe conversion is itself, in which case we
+      // justify this as a REFL step. This happens with trusted purification
+      // steps, for example.
+      Node resConv = d_anc.maybeConvert(res);
+      if (!resConv.isNull() && resConv.getKind() == Kind::EQUAL && resConv[0] == resConv[1])
+      {
+        return addAletheStep(AletheRule::REFL,
+                             res,
+                             nm->mkNode(Kind::SEXPR, d_cl, res),
+                             children,
+                             {},
+                             *cdp);
+      }
+      TrustId tid;
+      if (getTrustId(args[0], tid) && tid == TrustId::THEORY_LEMMA)
+      {
+        // if we are in the arithmetic case, we rather add a LIA_GENERIC step
+        if (res.getKind() == Kind::NOT && res[0].getKind() == Kind::AND)
+        {
+          Trace("alethe-proof") << "... test each arg if ineq\n";
+          bool allIneqs = true;
+          for (const Node& arg : res[0])
+          {
+            Node toTest = arg.getKind() == Kind::NOT ? arg[0] : arg;
+            Kind k = toTest.getKind();
+            if (k != Kind::LT && k != Kind::LEQ && k != Kind::GT
+                && k != Kind::GEQ && k != Kind::EQUAL)
+            {
+              Trace("alethe-proof") << "... arg " << arg << " not ineq\n";
+              allIneqs = false;
+              break;
+            }
+          }
+          if (allIneqs)
+          {
+            return addAletheStep(AletheRule::LIA_GENERIC,
+                                 res,
+                                 nm->mkNode(Kind::SEXPR, d_cl, res),
+                                 children,
+                                 {},
+                                 *cdp);
+          }
+        }
+      }
+      return addAletheStep(AletheRule::HOLE,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {},
+                           args,
                            *cdp);
     }
     // ======== Resolution and N-ary Resolution