Add option proof-elim-subtypes (cvc5#10407)

Enables a post-processing step that eliminates mixed arithmetic from proofs.

src/options/proof_options.toml

@@ -41,6 +41,14 @@ name   = "Proof"
   default    = "true"
   help       = "Dagify terms in proofs using global definitions"
 
+[[option]]
+  name       = "proofElimSubtypes"
+  category   = "expert"
+  long       = "proof-elim-subtypes"
+  type       = "bool"
+  default    = "false"
+  help       = "Eliminate subtypes (mixed arithmetic) in proofs"
+
 [[option]]
   name       = "proofPedantic"
   category   = "expert"

src/proof/subtype_elim_proof_converter.cpp

@@ -180,12 +180,14 @@ Node SubtypeElimConverterCallback::convert(Node res,
     break;
     default: break;
   }
-  if (success)
+  if (!success)
   {
-    return resc;
+    // if we did not succeed, just add a trust step
+    Trace("pf-subtype-elim-warn")
+        << "WARNING: Introduction of subtyping via rule " << id;
+    cdp->addTrustedStep(resc, TrustId::SUBTYPE_ELIMINATION, children, {});
   }
-  AlwaysAssert(false) << "Introduction of subtyping via rule " << id;
-  return Node::null();
+  return resc;
 }
 
 bool SubtypeElimConverterCallback::tryWith(ProofRule id,
@@ -310,7 +312,6 @@ bool SubtypeElimConverterCallback::prove(const Node& src,
     // where conv is (to_real src[0]) = (to_real src[1]).
     // Note that we assume a theory rewrite step for proving e.g.
     // (< t s) = (< (to_real t) (to_real s)).
-    return true;
   }
   return true;
 }

src/proof/trust_id.cpp

@@ -42,6 +42,7 @@ const char* toString(TrustId id)
     case TrustId::SUBS_EQ: return "SUBS_EQ";
     case TrustId::ARITH_PRED_CAST_TYPE: return "ARITH_PRED_CAST_TYPE";
     case TrustId::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS";
+    case TrustId::SUBTYPE_ELIMINATION: return "SUBTYPE_ELIMINATION";
     default: return "TrustId::Unknown";
   };
 }

src/proof/trust_id.h

@@ -60,6 +60,8 @@ enum class TrustId : uint32_t
   ARITH_PRED_CAST_TYPE,
   /** A quantifiers preprocessing step that was given without a proof */
   QUANTIFIERS_PREPROCESS,
+  /** A subtype elimination step that could not be processed */
+  SUBTYPE_ELIMINATION,
 };
 /** Converts a trust id to a string. */
 const char* toString(TrustId id);

src/smt/proof_post_processor.cpp

@@ -21,6 +21,7 @@
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "proof/resolution_proofs_util.h"
+#include "proof/subtype_elim_proof_converter.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/bv/bitblast/bitblast_proof_generator.h"
@@ -1148,6 +1149,15 @@ void ProofPostprocess::process(std::shared_ptr<ProofNode> pf,
   // now, process
   d_updater.process(pf);
 
+  // eliminate subtypes if option is specified
+  if (options().proof.proofElimSubtypes)
+  {
+    SubtypeElimConverterCallback secc(d_env);
+    ProofNodeConverter subtypeConvert(d_env, secc);
+    std::shared_ptr<ProofNode> pfc = subtypeConvert.process(pf);
+    AlwaysAssert(pfc != nullptr);
+  }
+
   // take stats and check pedantic
   d_finalCb.initializeUpdate();
   d_finalizer.process(pf);