mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Avoid const params in decls.
Const-qualification of parameters only has an effect in function definitions.
This commit is contained in:
parent
eea9b79035
commit
2016f48dc9
|
@ -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.
|
||||
|
|
|
@ -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,
|
||||
|
|
|
@ -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,
|
||||
|
|
|
@ -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<mpn_digit> {
|
||||
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue