From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 00:48:03 +0000 (-0500)
Subject: Default equality proofs for bags and separation logic (#6932)
X-Git-Tag: cvc5-1.0.0~1451
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bedba8e500fabeb0ac8f4f6e93af245f750a1850;p=cvc5.git

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 c2aa9eb1e..580d26c08 100644
--- 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 efede77ba..98130beb5 100644
--- 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());
       }