(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.

2 files changed, 16 insertions, 7 deletions

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 4c91297a1..3d7fd120a 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -23,6 +23,7 @@
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -187,6 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   const booleans::CircuitPropagator::BackEdgesMap& backEdges =
       propagator->getBackEdges();
   unordered_set<unsigned long> removeAssertions;
+
   SubstitutionMap& top_level_substs =
       d_preprocContext->getTopLevelSubstitutions();
 
@@ -519,6 +521,8 @@ PreprocessingPassResult MipLibTrick::applyInternal(
                   NodeManager::SKOLEM_EXACT_NAME);
               Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
               Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
+              TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr);
+              TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr);
 
               Node n = Rewriter::rewrite(geq.andNode(leq));
               assertionsToPreprocess->push_back(n);
@@ -526,14 +530,15 @@ PreprocessingPassResult MipLibTrick::applyInternal(
               {
                 ProofManager::currentPM()->addDependence(n, Node::null());
               }
-              SubstitutionMap nullMap(&fakeContext);
+              TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
+              CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get();
               Theory::PPAssertStatus status CVC4_UNUSED;  // just for assertions
-              status = te->solve(geq, nullMap);
+              status = te->solve(tgeq, tnullMap);
               Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
                   << "unexpected solution from arith's ppAssert()";
               Assert(nullMap.empty())
                   << "unexpected substitution from arith's ppAssert()";
-              status = te->solve(leq, nullMap);
+              status = te->solve(tleq, tnullMap);
               Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
                   << "unexpected solution from arith's ppAssert()";
               Assert(nullMap.empty())
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index fcb6dd171..823e93f52 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -21,6 +21,7 @@
 #include "context/cdo.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -116,7 +117,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   SubstitutionMap& top_level_substs =
       d_preprocContext->getTopLevelSubstitutions();
   SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
-  SubstitutionMap newSubstitutions(d_preprocContext->getUserContext());
+  TrustSubstitutionMap tnewSubstituions(d_preprocContext->getUserContext(),
+                                        nullptr);
+  SubstitutionMap& newSubstitutions = tnewSubstituions.get();
   SubstitutionMap::iterator pos;
   size_t j = 0;
   std::vector<Node>& learned_literals = propagator->getLearnedLiterals();
@@ -178,10 +181,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
     // Solve it with the corresponding theory, possibly adding new
     // substitutions to newSubstitutions
     Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
-
+    TrustNode tlearnedLiteral =
+        TrustNode::mkTrustLemma(learnedLiteral, nullptr);
     Theory::PPAssertStatus solveStatus =
-        d_preprocContext->getTheoryEngine()->solve(learnedLiteral,
-                                                   newSubstitutions);
+        d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
+                                                   tnewSubstituions);
 
     switch (solveStatus)
     {