minor code simplifications

Z3Prover · Aug 20, 2022 · d5d77df · d5d77df
1 parent 08bf7a6
commit d5d77df
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 18 deletions.
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
@@ -886,8 +886,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
         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 def_module_params(module_name, export, params, class_name=None, description=
                 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
@@ -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
@@ -115,7 +115,7 @@ class mpq_manager : public mpz_manager<SYNCH> {
     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
@@ -138,21 +138,15 @@ class rational {
         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; }