From: Tim King <taking@cs.nyu.edu>
Date: Wed, 23 Aug 2017 22:49:32 +0000 (-0700)
Subject: Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)
X-Git-Tag: cvc5-1.0.0~5670
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c57139b1e0ddd918eea5f9b77dae7d3a04b3860a;p=cvc5.git

Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)
---

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 3427edbd3..15f82d82b 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -438,18 +438,14 @@ ConstraintP Constraint::getCeiling() {
   Debug("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
   Assert(getValue().getInfinitesimalPart().sgn() > 0);
 
-  DeltaRational ceiling(getValue().ceiling());
-
-  // TODO: "Optimize via the iterator"
+  const DeltaRational ceiling(getValue().ceiling());
   return d_database->getConstraint(getVariable(), getType(), ceiling);
 }
 
 ConstraintP Constraint::getFloor() {
   Assert(getValue().getInfinitesimalPart().sgn() < 0);
 
-  DeltaRational floor(Rational(getValue().floor()));
-
-  // TODO: "Optimize via the iterator"
+  const DeltaRational floor(Rational(getValue().floor()));
   return d_database->getConstraint(getVariable(), getType(), floor);
 }