From d5d77dfe642181d61f033be508daba2fc88bb286 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sat, 20 Aug 2022 12:56:45 +0100
Subject: [PATCH] minor code simplifications

---
 scripts/mk_genfile_common.py |  4 +---
 src/util/mpq.cpp             |  4 ----
 src/util/mpq.h               |  2 +-
 src/util/rational.h          | 14 ++++----------
 4 files changed, 6 insertions(+), 18 deletions(-)

diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index f4b54cba0..3b19b8c25 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -886,8 +886,7 @@ def mk_hpp_from_pyg(pyg_file, output_dir):
         hpp = os.path.join(dirname, '%s.hpp' % class_name)
         out = open(hpp, 'w')
         out.write('// Automatically generated file\n')
-        out.write('#ifndef __%s_HPP_\n' % class_name.upper())
-        out.write('#define __%s_HPP_\n' % class_name.upper())
+        out.write('#pragma once\n')
         out.write('#include "util/params.h"\n')
         if export:
             out.write('#include "util/gparams.h"\n')
@@ -919,7 +918,6 @@ def mk_hpp_from_pyg(pyg_file, output_dir):
                 out.write('  %s %s() const { return p.%s("%s", %s); }\n' %
                           (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
         out.write('};\n')
-        out.write('#endif\n')
         out.close()
         OUTPUT_HPP_FILE.append(hpp)
 
diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp
index ed73e21f0..324750cfa 100644
--- a/src/util/mpq.cpp
+++ b/src/util/mpq.cpp
@@ -20,10 +20,6 @@ Revision History:
 #include "util/warning.h"
 #include "util/z3_exception.h"
 
-template<bool SYNCH>
-mpq_manager<SYNCH>::mpq_manager() {
-}
-
 template<bool SYNCH>
 mpq_manager<SYNCH>::~mpq_manager() {
     del(m_tmp1);
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 1b97b6ece..f1afcbe50 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -115,7 +115,7 @@ public:
     static bool precise() { return true; }
     static bool field() { return true; }
 
-    mpq_manager();
+    mpq_manager() = default;
 
     ~mpq_manager();
 
diff --git a/src/util/rational.h b/src/util/rational.h
index cffd0083c..4203a54ea 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -138,21 +138,15 @@ public:
         m().set(m_val, r.m_val);
         return *this;
     }
-private:
-    rational & operator=(bool) {
-        UNREACHABLE(); return *this;
-    }
-    inline rational operator*(bool  r1) const {
-        UNREACHABLE();
-        return *this;
-    }
 
-public:
+    rational & operator=(bool) = delete;
+    rational operator*(bool  r1) const = delete;
+
     rational & operator=(int v) {
         m().set(m_val, v);
         return *this;
     }
-    rational & operator=(double v) { UNREACHABLE(); return *this; }
+    rational & operator=(double v) = delete;
 
     friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }