summaryrefslogtreecommitdiff
path: root/src/theory/sets/theory_sets.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets/theory_sets.h')
-rw-r--r--src/theory/sets/theory_sets.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 16829bc6d..14f4b5699 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -53,6 +53,8 @@ class TheorySets : public Theory
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
@@ -102,7 +104,7 @@ class TheorySets : public Theory
void eqNotifyNewClass(TNode t) override;
void eqNotifyMerge(TNode t1, TNode t2) override;
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
-
+
private:
TheorySetsPrivate& d_theory;
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback