diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-22 17:21:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-22 22:21:02 +0000 |
| commit | 76c6a103fb68f75e65201da5bab572f4630cd207 (patch) | |
| tree | ef5cded3c6f1278995ccd4203cab716e705edc07 /src/theory | |
| parent | d442be84a2e47ccc6b3b91dbcf5ae2c1b891049b (diff) | |
Remove stale pointer to proof node manager from skolemize utility (#7471)
Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/skolemize.h | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 830847b74..ccd9afe3e 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -62,6 +62,7 @@ TrustNode Skolemize::process(Node q) if (isProofEnabled() && !options::dtStcInduction() && !options::intWfInduction()) { + ProofNodeManager * pnm = d_env.getProofNodeManager(); // if using proofs and not using induction, we use the justified // skolemization NodeManager* nm = NodeManager::currentNM(); @@ -71,12 +72,12 @@ TrustNode Skolemize::process(Node q) Node existsq = nm->mkNode(EXISTS, echildren); Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv"); Node qnot = q.notNode(); - CDProof cdp(d_pnm); + CDProof cdp(pnm); cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {}); std::shared_ptr<ProofNode> pf = cdp.getProofFor(res); std::vector<Node> assumps; assumps.push_back(qnot); - std::shared_ptr<ProofNode> pfs = d_pnm->mkScope({pf}, assumps); + std::shared_ptr<ProofNode> pfs = pnm->mkScope({pf}, assumps); lem = nm->mkNode(IMPLIES, qnot, res); d_epg->setProofFor(lem, pfs); pg = d_epg.get(); diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 604bc60e4..f1fb78e8d 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -149,8 +149,6 @@ class Skolemize : protected EnvObj std::unordered_map<Node, std::vector<Node>> d_skolem_constants; /** map from quantified formulas to their skolemized body */ std::unordered_map<Node, Node> d_skolem_body; - /** Pointer to the proof node manager */ - ProofNodeManager* d_pnm; /** Eager proof generator for skolemization lemmas */ std::unique_ptr<EagerProofGenerator> d_epg; }; |