From bedba8e500fabeb0ac8f4f6e93af245f750a1850 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Jul 2021 19:48:03 -0500 Subject: [PATCH] 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. --- src/theory/bags/theory_bags.cpp | 2 +- src/theory/sep/theory_sep.cpp | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) 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()); } -- 2.30.2