diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-22 23:09:03 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-22 23:09:03 +0000 |
commit | 1a99b24c49f9b865a70fa626efcb96571499917e (patch) | |
tree | cb3c85e9c439925b74cb4f2e5782a5c19d32fe94 /src/theory/arith/delta_rational.h | |
parent | c0324db3ac7e5984c632f46690f58c333b9a42b2 (diff) |
* improving arithmetic getEqualityStatus
* some sharing improvements based on model
Diffstat (limited to 'src/theory/arith/delta_rational.h')
-rw-r--r-- | src/theory/arith/delta_rational.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index c004a681f..a46dde1cf 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -89,6 +89,18 @@ public: return *(this) + (a * negOne); } + DeltaRational operator/(const Rational& a) const{ + CVC4::Rational tmpC = c/a; + CVC4::Rational tmpK = k/a; + return DeltaRational(tmpC, tmpK); + } + + DeltaRational operator/(const Integer& a) const{ + CVC4::Rational tmpC = c/a; + CVC4::Rational tmpK = k/a; + return DeltaRational(tmpC, tmpK); + } + bool operator==(const DeltaRational& other) const{ return (k == other.k) && (c == other.c); } |