summaryrefslogtreecommitdiff
path: root/src/theory/arith/delta_rational.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/delta_rational.h')
-rw-r--r--src/theory/arith/delta_rational.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index c8a5e39a7..fdc3bee3b 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -54,6 +54,15 @@ public:
return c;
}
+ int sgn() const {
+ int x = getNoninfinitesimalPart().sgn();
+ if(x == 0){
+ return getInfinitesimalPart().sgn();
+ }else{
+ return x;
+ }
+ }
+
DeltaRational operator+(const DeltaRational& other) const{
CVC4::Rational tmpC = c+other.c;
CVC4::Rational tmpK = k+other.k;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback