Fix issues with tracing builds (#7809)
authorGereon Kremer <gkremer@stanford.edu>
Tue, 14 Dec 2021 20:40:06 +0000 (12:40 -0800)
committerGitHub <noreply@github.com>
Tue, 14 Dec 2021 20:40:06 +0000 (20:40 +0000)
commit1bf45579ff7a4af921bb3db159e371623a4bfd63
tree8bf3632e1ae3cb1f54c834b3efb9894d2266fe6d
parent942b1c357a2a635bedcda8e01ce4f934c8a5a2e9
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.
src/theory/arith/theory_arith_private.cpp
src/util/rational_cln_imp.h
src/util/rational_gmp_imp.h