summaryrefslogtreecommitdiff
path: root/src/theory/fp/theory_fp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
-rw-r--r--src/theory/fp/theory_fp.cpp9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 38444c7af..f647450c0 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -132,6 +132,8 @@ TheoryFp::TheoryFp(context::Context* c,
TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryFp::getProofChecker() { return nullptr; }
+
bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notification;
@@ -940,12 +942,11 @@ void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2)
d_im.conflictEqConstantMerge(t1, t2);
}
-
-bool TheoryFp::needsCheckLastEffort()
-{
+bool TheoryFp::needsCheckLastEffort()
+{
// only need to check if we have added to the abstraction map, otherwise
// postCheck below is a no-op.
- return !d_abstractionMap.empty();
+ return !d_abstractionMap.empty();
}
void TheoryFp::postCheck(Effort level)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback