From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 14 Dec 2021 20:40:06 +0000 (-0800)
Subject: Fix issues with tracing builds (#7809)
X-Git-Tag: cvc5-1.0.0~666
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1bf45579ff7a4af921bb3db159e371623a4bfd63;p=cvc5.git

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.
---

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); }