diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 5 | ||||
| -rw-r--r-- | src/smt/term_formula_removal.h | 10 |
2 files changed, 14 insertions, 1 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 5034119e8..cf7c00e2b 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -552,6 +552,11 @@ void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm) } } +ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() +{ + return d_tpg.get(); +} + bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; } }/* CVC4 namespace */ diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 30972c1cc..25dcd0295 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -107,11 +107,19 @@ class RemoveTermFormulas { /** * Set proof node manager, which signals this class to enable proofs using the - * given checker. + * given proof node manager. */ void setProofNodeManager(ProofNodeManager* pnm); /** + * Get proof generator that is responsible for all proofs for removing term + * formulas from nodes. When proofs are enabled, the returned trust node + * of the run method use this proof generator (the trust nodes in newAsserts + * do not use this generator). + */ + ProofGenerator* getTConvProofGenerator(); + + /** * Get axiom for term n. This returns the axiom that this class uses to * eliminate the term n, which is determined by its top-most symbol. For * example, if n is (ite n1 n2 n3), this returns the formula: |