diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-12-14 12:40:06 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 20:40:06 +0000 |
| commit | 1bf45579ff7a4af921bb3db159e371623a4bfd63 (patch) | |
| tree | 8bf3632e1ae3cb1f54c834b3efb9894d2266fe6d /src/util/rational_cln_imp.h | |
| parent | 942b1c357a2a635bedcda8e01ce4f934c8a5a2e9 (diff) | |
Fix issues with tracing builds (#7809)
This PR fixes two issues that were revealed when analyzing decreased performance on trace-enabled builds.
hasIntegerModel() turns out to be a rather expensive method and should thus not be called in a Trace output.
Furthermore, the implementation of Rational::isIntegral() was generally bad because it used getDenominator() (which returns a copy of the denominator as an Integer) instead of directly checking the underlying denominator with equality for zero.
Diffstat (limited to 'src/util/rational_cln_imp.h')
| -rw-r--r-- | src/util/rational_cln_imp.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 017fc3cb4..8f8552e9c 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -193,7 +193,7 @@ class CVC5_EXPORT Rational } } - bool isIntegral() const { return getDenominator() == 1; } + bool isIntegral() const { return cln::denominator(d_value) == 1; } Integer floor() const { return Integer(cln::floor1(d_value)); } |