diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 22:38:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-11 22:38:04 -0500 |
| commit | 3a8a27994584ca2168ef71d5eb0ce46ef558ba34 (patch) | |
| tree | efa67475c597a8fdb6664a67dd80e7b022919bd2 /src/smt/assertions.h | |
| parent | 383d061be2bc8162d3379c98ad106555d21e5f86 (diff) | |
(proof-new) Add SMT proof manager (#5054)
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
Diffstat (limited to 'src/smt/assertions.h')
| -rw-r--r-- | src/smt/assertions.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/assertions.h b/src/smt/assertions.h index a74c58bd8..a73cd32d6 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -109,6 +109,12 @@ class Assertions /** Flip the global negation flag. */ void flipGlobalNegated(); + //------------------------------------ for proofs + /** Set proof generator */ + void setProofGenerator(smt::PreprocessProofGenerator* pppg); + /** Is proof enabled? */ + bool isProofEnabled() const; + //------------------------------------ end for proofs private: /** * Fully type-check the argument, and also type-check that it's |