Lines Matching refs:mk_times
14 (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq,
303 return [(x, i, mk_plus (x, y), mk_plus (x, mk_times (i, y)),
305 (x, i, mk_plus (y, x), mk_plus (x, mk_times (i, y)),
307 (x, i, mk_minus (x, y), mk_minus (x, mk_times (i, y)),
310 mk_plus (x, mk_times (i, mk_plus (y, z))),
313 mk_plus (x, mk_times (i, mk_plus (y, z))),
316 mk_plus (x, mk_times (i, mk_plus (y, z))),
319 mk_plus (x, mk_times (i, mk_plus (y, z))),
322 mk_minus (x, mk_times (i, mk_plus (y, z))),
443 sz = mk_times (mk_word32 (typ.size ()), n)
519 return mk_times (num, el_size)
554 size = mk_times (n, el_size)
589 size = mk_times (mk_word32 (typ.size ()), num)
603 size = mk_times (mk_word32 (typ.size ()), num)