From: Tim King <taking@cs.nyu.edu>
Date: Tue, 14 Aug 2012 17:55:33 +0000 (+0000)
Subject: Adds substituteDelta() to DeltaRational which given a value for delta returns the... 
X-Git-Tag: cvc5-1.0.0~7871
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a6a08df0838b7fb70275a70ddc942c3ac802081;p=cvc5.git

Adds substituteDelta() to DeltaRational which given a value for delta returns the corresponding rational value.
---

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);