diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index bfe30db61..6adf8f66a 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -18,7 +18,6 @@ #pragma once #include "expr/node.h" -#include "proof/arith_proof_recorder.h" #include "theory/arith/arith_state.h" #include "theory/arith/theory_arith_private_forward.h" #include "theory/theory.h" @@ -41,11 +40,6 @@ class TheoryArith : public Theory { TimerStat d_ppRewriteTimer; - /** - * @brief Where to store Farkas proofs of lemmas - */ - proof::ArithProofRecorder * d_proofRecorder; - public: TheoryArith(context::Context* c, context::UserContext* u, @@ -110,11 +104,6 @@ class TheoryArith : public Theory { std::pair<bool, Node> entailmentCheck(TNode lit) override; - void setProofRecorder(proof::ArithProofRecorder* proofRecorder) - { - d_proofRecorder = proofRecorder; - } - private: /** The state object wrapping TheoryArithPrivate */ ArithState d_astate; |