summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl/nonlinear_extension.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.h')
-rw-r--r--src/theory/arith/nl/nonlinear_extension.h9
1 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index a6b68d644..fba9e8e87 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -193,15 +193,6 @@ class NonlinearExtension
/** compute relevant assertions */
void computeRelevantAssertions(const std::vector<Node>& assertions,
std::vector<Node>& keep);
- /**
- * Potentially adds lemmas to the set out and clears lemmas. Returns
- * the number of lemmas added to out. We do not add lemmas that have already
- * been sent on the output channel of TheoryArith.
- */
- unsigned filterLemmas(std::vector<NlLemma>& lemmas,
- std::vector<NlLemma>& out);
- /** singleton version of above */
- unsigned filterLemma(NlLemma lem, std::vector<NlLemma>& out);
/** run check strategy
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback