From 1bf45579ff7a4af921bb3db159e371623a4bfd63 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 14 Dec 2021 12:40:06 -0800 Subject: [PATCH] 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 | 4 +--- src/util/rational_cln_imp.h | 2 +- src/util/rational_gmp_imp.h | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bf8798485..9b4623d37 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1839,7 +1839,6 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em << " " << effortLevel << " " << d_lastContextIntegerAttempted << " " << level - << " " << hasIntegerModel() << endl; if(d_qflraStatus == Result::UNSAT){ return false; } @@ -3372,8 +3371,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) Debug("arith") << "integer? " << " conf/split " << emmittedConflictOrSplit - << " fulleffort " << Theory::fullEffort(effortLevel) - << " hasintmodel " << hasIntegerModel() << endl; + << " fulleffort " << Theory::fullEffort(effortLevel) << endl; if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){ Node possibleConflict = Node::null(); 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)); } diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index b3c876533..de3fcd03d 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -286,7 +286,7 @@ class CVC5_EXPORT Rational return (*this); } - bool isIntegral() const { return getDenominator() == 1; } + bool isIntegral() const { return mpz_cmp_ui(d_value.get_den_mpz_t(), 1) == 0; } /** Returns a string representing the rational in the given base. */ std::string toString(int base = 10) const { return d_value.get_str(base); } -- 2.30.2