Default equality proofs for bags and separation logic (#6932)

This is the last 2 remaining theories not to use the default handling of equality proofs.

In preparation for proofs in central equality engine.

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index c2aa9eb1e82c001d7de027a89b249bdc4761dd88..580d26c080e2c7a957e9f46e021c818e5b0bb6f8 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -35,7 +35,7 @@ TheoryBags::TheoryBags(context::Context* c,
                        ProofNodeManager* pnm)
     : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
       d_state(c, u, valuation),
-      d_im(*this, d_state, nullptr),
+      d_im(*this, d_state, pnm),
       d_ig(&d_state, &d_im),
       d_notify(*this, d_im),
       d_statistics(),

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index efede77ba54cc6d3fad7739b751f7dd0a338da8d..98130beb5263100b1f9fb87b79d3f43631d6c9ff 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -52,7 +52,7 @@ TheorySep::TheorySep(context::Context* c,
       d_lemmas_produced_c(u),
       d_bounds_init(false),
       d_state(c, u, valuation),
-      d_im(*this, d_state, nullptr, "theory::sep::"),
+      d_im(*this, d_state, pnm, "theory::sep::"),
       d_notify(*this),
       d_reduce(u),
       d_spatial_assertions(c)
@@ -1785,11 +1785,12 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, InferenceId id,
       if( conc==d_false ){
         Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << id
                            << std::endl;
-        d_im.conflictExp(id, ant, nullptr);
+        d_im.conflictExp(id, PfRule::THEORY_INFERENCE, ant, {conc});
       }else{
         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant
                            << " by " << id << std::endl;
-        TrustNode trn = d_im.mkLemmaExp(conc, ant, {});
+        TrustNode trn =
+            d_im.mkLemmaExp(conc, PfRule::THEORY_INFERENCE, ant, {}, {conc});
         d_im.addPendingLemma(
             trn.getNode(), id, LemmaProperty::NONE, trn.getGenerator());
       }