diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2017-08-21 15:50:56 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-25 16:40:27 -0700 |
| commit | a013c33fa72cdc6ce84b1ea596c44acc9a56b754 (patch) | |
| tree | f8899e4901b040a09642a07a47863b9377bb240a /src/proof/proof_manager.h | |
| parent | 53cade050e191c7c0dc0ebfae716a21162bd9b22 (diff) | |
Support for quantifier proofsquantifier_proofs_
Diffstat (limited to 'src/proof/proof_manager.h')
| -rw-r--r-- | src/proof/proof_manager.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 0d3250b12..2d6967c52 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -69,6 +69,7 @@ class TheoryProof; class UFProof; class ArithProof; class ArrayProof; +class QuantifiersProof; namespace proof { class ResolutionBitVectorProof; @@ -194,6 +195,7 @@ public: static proof::ResolutionBitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); static ArithProof* getArithProof(); + static QuantifiersProof* getQuantifiersProof(); static SkolemizationManager *getSkolemizationManager(); |