summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r--src/theory/arith/theory_arith.h11
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback