Searched refs:bvconst_lshr (Results 1 – 7 of 7) sorted by relevance
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_bvconst_shifts.c | 79 bvconst_lshr(lshr, x, y, n); in test_shift()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
| H A D | bv_utils.h | 236 bvconst_lshr(out_value->data, children_values[0]->data, children_values[1]->data, bitsize); in bv_term_compute_value()
|
| H A D | bv_evaluator.c | 235 bvconst_lshr(out_value->data, t_arg_val[0].data, t_arg_val[1].data, t_arg_val[0].bitsize); in bv_evaluator_run_composite_term()
|
| /dports/math/yices/yices-2.6.2/src/terms/ |
| H A D | bv_constants.h | 343 extern void bvconst_lshr(uint32_t *bv, uint32_t *a, uint32_t *b, uint32_t n);
|
| H A D | bv_constants.c | 1099 void bvconst_lshr(uint32_t *bv, uint32_t *a, uint32_t *b, uint32_t n) { in bvconst_lshr() function
|
| /dports/math/yices/yices-2.6.2/src/solvers/bv/ |
| H A D | new_bvsolver.c | 5696 bvconst_lshr(aux->data, bvvar_val(vtbl, x), bvvar_val(vtbl, y), n); in bv_solver_create_bvlshr()
8143 bvconst_lshr(c, a1, a2, n); in bv_solver_binop_value()
|
| H A D | bvsolver.c | 5874 bvconst_lshr(aux->data, bvvar_val(vtbl, x), bvvar_val(vtbl, y), n); in bv_solver_create_bvlshr()
8335 bvconst_lshr(c, a1, a2, n); in bv_solver_binop_value()
|