diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-26 19:48:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-27 00:48:03 +0000 |
| commit | bedba8e500fabeb0ac8f4f6e93af245f750a1850 (patch) | |
| tree | 5e81376490d020e4b14e7218f309ab4544358aa6 | |
| parent | 4640dd5d09d65761ab96ea7f6848d823a3a43278 (diff) | |
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.
| -rw-r--r-- | src/theory/bags/theory_bags.cpp | 2 | ||||
| -rw-r--r-- | 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()); } |