(proof-new) Add interface for trusted substitution and update ppAssert (#5193)

The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.

This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.

This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.

1 files changed, 6 insertions, 5 deletions

diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 417cf0c15..a19af44ac 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -439,9 +439,10 @@ void BVSolverLazy::propagate(Theory::Effort e)
   }
 }
 
-Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
-                                              SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus BVSolverLazy::ppAssert(
+    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 {
+  TNode in = tin.getNode();
   switch (in.getKind())
   {
     case kind::EQUAL:
@@ -449,13 +450,13 @@ Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
       if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
       {
         ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitution(in[0], in[1]);
+        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
         return Theory::PP_ASSERT_STATUS_SOLVED;
       }
       if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
       {
         ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitution(in[1], in[0]);
+        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
         return Theory::PP_ASSERT_STATUS_SOLVED;
       }
       Node node = Rewriter::rewrite(in);
@@ -502,7 +503,7 @@ Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
           Assert(utils::getSize(concat) == utils::getSize(extract[0]));
           if (d_bv.isLegalElimination(extract[0], concat))
           {
-            outSubstitutions.addSubstitution(extract[0], concat);
+            outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
             return Theory::PP_ASSERT_STATUS_SOLVED;
           }
         }