From 1967722d29bf1f4811f52210c4da84091365f333 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 6 Oct 2021 20:03:17 -0700
Subject: [PATCH] Replace doubles by rationals in C++ quickstart (#7317)

This PR removes the conversion of rationals to double in favour of properly handling them as rationals (as pairs of integers) in the C++ quickstart example.
---
 docs/api/cpp/quickstart.rst     | 16 ++++++++--------
 examples/api/cpp/quickstart.cpp | 26 +++++++++++++++++---------
 2 files changed, 25 insertions(+), 17 deletions(-)

diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst
index e639e3972..dec07c5f0 100644
--- a/docs/api/cpp/quickstart.rst
+++ b/docs/api/cpp/quickstart.rst
@@ -107,20 +107,20 @@ This will print the following:
   value for y: 1/6
   value for x - y: 0.0
 
-We can convert these values to C++ types using standard conversion functions.
+We can convert these values to C++ types.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
-     :lines: 119-121
+     :lines: 117-124
 
 Another way to independently compute the value of ``x - y`` would be to
-use the C++ minus operator instead of asking the solver.
+perform the (rational) arithmetic manually.
 However, for more complex terms, it is easier to let the solver do the
 evaluation.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
-     :lines: 127-135
+     :lines: 130-143
 
 This will print:
 
@@ -134,7 +134,7 @@ For this, we first reset the assertions added to the solver.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
-     :lines: 141
+     :lines: 149
 
 Next, we assert the same assertions as above, but with integers.
 This time, we inline the construction of terms
@@ -142,13 +142,13 @@ to the assertion command.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
-     :lines: 146-150
+     :lines: 154-158
 
 Now, we check whether the revised assertion is satisfiable.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
-     :lines: 153, 156-157
+     :lines: 161, 164-165
 
 This time the asserted formula is unsatisfiable:
 
@@ -162,7 +162,7 @@ of the assertions that is already unsatisfiable.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
-     :lines: 161-167
+     :lines: 169-175
 
 This will print:
 
diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp
index 6bd661554..7758c5f79 100644
--- a/examples/api/cpp/quickstart.cpp
+++ b/examples/api/cpp/quickstart.cpp
@@ -17,8 +17,8 @@
 #include <cvc5/cvc5.h>
 
 #include <iostream>
+#include <numeric>
 
-using namespace std;
 using namespace cvc5::api;
 
 int main()
@@ -114,18 +114,26 @@ int main()
   std::cout << "value for y: " << yStr << std::endl;
   std::cout << "value for x - y: " << xMinusYStr << std::endl;
 
-  // Further, we can convert the values to cpp types,
-  // using standard cpp conversion functions.
-  double xDouble = std::stod(xStr);
-  double yDouble = std::stod(yStr);
-  double xMinusYDouble = std::stod(xMinusYStr);
+  // Further, we can convert the values to cpp types
+  std::pair<int64_t, uint64_t> xPair = xVal.getReal64Value();
+  std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
+  std::pair<int64_t, uint64_t> xMinusYPair = xMinusYVal.getReal64Value();
+
+  std::cout << "value for x: " << xPair.first << "/" << xPair.second << std::endl;
+  std::cout << "value for y: " << yPair.first << "/" << yPair.second << std::endl;
+  std::cout << "value for x - y: " << xMinusYPair.first << "/" << xMinusYPair.second << std::endl;
 
   // Another way to independently compute the value of x - y would be
-  // to use the cpp minus operator instead of asking the solver.
+  // to perform the (rational) arithmetic manually.
   // However, for more complex terms,
   // it is easier to let the solver do the evaluation.
-  double xMinusYComputed = xDouble - yDouble;
-  if (xMinusYComputed == xMinusYDouble)
+  std::pair<int64_t, uint64_t> xMinusYComputed = {
+    xPair.first * yPair.second - xPair.second * yPair.first,
+    xPair.second * yPair.second
+  };
+  uint64_t g = std::gcd(xMinusYComputed.first, xMinusYComputed.second);
+  xMinusYComputed = { xMinusYComputed.first / g, xMinusYComputed.second / g };
+  if (xMinusYComputed == xMinusYPair)
   {
     std::cout << "computed correctly" << std::endl;
   }
-- 
2.30.2