summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-08-14 17:55:33 +0000
committerTim King <taking@cs.nyu.edu>2012-08-14 17:55:33 +0000
commit5a6a08df0838b7fb70275a70ddc942c3ac802081 (patch)
tree672a1b44d4b489390e8973980c250812de0afabc /src
parent8d6589fee6583ee7036c83a25d7e71471f6f5fd5 (diff)
Adds substituteDelta() to DeltaRational which given a value for delta returns the corresponding rational value.
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/delta_rational.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index ed256faa1..ca182a844 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -181,6 +181,10 @@ public:
std::string toString() const;
+ Rational substituteDelta(const Rational& d) const{
+ return getNoninfinitesimalPart() + (d * getInfinitesimalPart());
+ }
+
};
std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback