From 2016f48dc9e53b0977f3202e0bdefb0e48b5a005 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 28 Nov 2018 19:07:33 +0700 Subject: [PATCH] Avoid const params in decls. Const-qualification of parameters only has an effect in function definitions. --- src/ackermannization/lackr.h | 2 +- src/muz/rel/dl_compiler.h | 2 +- src/muz/rel/dl_instruction.h | 2 +- src/util/mpn.h | 44 ++++++++++++++++++------------------ 4 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h index 98c1988f7..049fb8bb3 100644 --- a/src/ackermannization/lackr.h +++ b/src/ackermannization/lackr.h @@ -102,7 +102,7 @@ class lackr { // // Introduce congruence ackermann lemma for the two given terms. // - bool ackr(app * const t1, app * const t2); + bool ackr(app * t1, app * t2); // // Introduce the ackermann lemma for each pair of terms. diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index d7bdcad34..6bc2a819f 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -148,7 +148,7 @@ namespace datalog { void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, bool reuse_t1, instruction_block & acc); void make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols, - const unsigned min_col, instruction_block & acc); + unsigned min_col, instruction_block & acc); void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc); void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index 6e0b7bfe5..918763a95 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -285,7 +285,7 @@ namespace datalog { const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, reg_idx result); static instruction * mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols, - const unsigned min_col); + unsigned min_col); static instruction * mk_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, reg_idx tgt); static instruction * mk_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt, diff --git a/src/util/mpn.h b/src/util/mpn.h index a5d3c30d8..ea20fc42b 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -37,29 +37,29 @@ public: mpn_manager(); ~mpn_manager(); - int compare(mpn_digit const * a, size_t const lnga, - mpn_digit const * b, size_t const lngb) const; + int compare(mpn_digit const * a, size_t lnga, + mpn_digit const * b, size_t lngb) const; - bool add(mpn_digit const * a, size_t const lnga, - mpn_digit const * b, size_t const lngb, - mpn_digit *c, size_t const lngc_alloc, + bool add(mpn_digit const * a, size_t lnga, + mpn_digit const * b, size_t lngb, + mpn_digit *c, size_t lngc_alloc, size_t * plngc) const; - bool sub(mpn_digit const * a, size_t const lnga, - mpn_digit const * b, size_t const lngb, + bool sub(mpn_digit const * a, size_t lnga, + mpn_digit const * b, size_t lngb, mpn_digit * c, mpn_digit * pborrow) const; - bool mul(mpn_digit const * a, size_t const lnga, - mpn_digit const * b, size_t const lngb, + bool mul(mpn_digit const * a, size_t lnga, + mpn_digit const * b, size_t lngb, mpn_digit * c) const; - bool div(mpn_digit const * numer, size_t const lnum, - mpn_digit const * denom, size_t const lden, + bool div(mpn_digit const * numer, size_t lnum, + mpn_digit const * denom, size_t lden, mpn_digit * quot, mpn_digit * rem); - char * to_string(mpn_digit const * a, size_t const lng, - char * buf, size_t const lbuf) const; + char * to_string(mpn_digit const * a, size_t lng, + char * buf, size_t lbuf) const; private: #ifdef _AMD64_ class mpn_sbuffer : public sbuffer { @@ -88,29 +88,29 @@ private: static const mpn_digit zero; mpn_sbuffer u, v, t_ms, t_ab; - void display_raw(std::ostream & out, mpn_digit const * a, size_t const lng) const; + void display_raw(std::ostream & out, mpn_digit const * a, size_t lng) const; - size_t div_normalize(mpn_digit const * numer, size_t const lnum, - mpn_digit const * denom, size_t const lden, + size_t div_normalize(mpn_digit const * numer, size_t lnum, + mpn_digit const * denom, size_t lden, mpn_sbuffer & n_numer, mpn_sbuffer & n_denom) const; void div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom, - size_t const d, mpn_digit * rem) const; + size_t d, mpn_digit * rem) const; - bool div_1(mpn_sbuffer & numer, mpn_digit const denom, + bool div_1(mpn_sbuffer & numer, mpn_digit denom, mpn_digit * quot) const; bool div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom, mpn_digit * quot, mpn_digit * rem, mpn_sbuffer & ms, mpn_sbuffer & ab) const; - void trace(mpn_digit const * a, size_t const lnga, - mpn_digit const * b, size_t const lngb, + void trace(mpn_digit const * a, size_t lnga, + mpn_digit const * b, size_t lngb, const char * op) const; - void trace(mpn_digit const * a, size_t const lnga) const; - void trace_nl(mpn_digit const * a, size_t const lnga) const; + void trace(mpn_digit const * a, size_t lnga) const; + void trace_nl(mpn_digit const * a, size_t lnga) const; }; #endif