From 5a6a08df0838b7fb70275a70ddc942c3ac802081 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 14 Aug 2012 17:55:33 +0000
Subject: Adds substituteDelta() to DeltaRational which given a value for delta
 returns the corresponding rational value.

---
 src/theory/arith/delta_rational.h | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/theory')

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);
-- 
cgit v1.2.3