diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 14:48:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-12 14:48:31 -0500 |
| commit | 2174ab36023326cd998565bbf35d31c38bc10594 (patch) | |
| tree | a61a1cb1cc00faa1339adf315fd4037b0ca08b1a /src/smt/term_formula_removal.h | |
| parent | 27413a45e28001f6155d529a59d679556cdc011e (diff) | |
(proof-new) Improve interfaces to proof generators (#4803)
This includes configurable naming and a caching policy for term conversion proof generator.
Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
Diffstat (limited to 'src/smt/term_formula_removal.h')
| -rw-r--r-- | src/smt/term_formula_removal.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index d4c22b78b..78d5899d0 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -106,10 +106,10 @@ class RemoveTermFormulas { void garbageCollect(); /** - * Set proof checker, which signals this class to enable proofs using the + * Set proof node manager, which signals this class to enable proofs using the * given checker. */ - void setProofChecker(ProofChecker* pc); + void setProofNodeManager(ProofNodeManager* pnm); /** * Get axiom for term n. This returns the axiom that this class uses to @@ -166,7 +166,7 @@ class RemoveTermFormulas { static bool hasNestedTermChildren( TNode node ); /** A proof node manager */ - std::unique_ptr<ProofNodeManager> d_pnm; + ProofNodeManager* d_pnm; /** * A proof generator for the term conversion. */ |