| /dports/math/boolector/boolector-3.2.2/test/ |
| H A D | test_propinv.cpp | 569 srl = btor_exp_bv_srl (d_btor, e[0], e[1]); in check_conf_srl()
581 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "00", "01", 1); in check_conf_srl()
583 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "00", "10", 0); in check_conf_srl()
585 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "00", "11", 0); in check_conf_srl()
588 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "01", "10", 0); in check_conf_srl()
590 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "01", "11", 0); in check_conf_srl()
593 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "10", "11", 0); in check_conf_srl()
596 1, srl, e, btor_exp_bv_srl, inv_srl_bv, "11", "10", 0); in check_conf_srl()
701 0, srl, e, btor_exp_bv_srl, inv_srl_bv, "01", "10", 0); in check_conf_srl()
703 0, srl, e, btor_exp_bv_srl, inv_srl_bv, "01", "11", 0); in check_conf_srl()
[all …]
|
| H A D | test_prop.cpp | 238 prop_complete_binary (1, btor_exp_bv_srl, btor_bv_srl, inv_srl_bv); in TEST_F()
310 prop_complete_binary (2, btor_exp_bv_srl, btor_bv_srl, inv_srl_bv); in TEST_F()
|
| H A D | test_lambda.cpp | 592 binary_param_exp_test (0, btor_exp_bv_srl); in TEST_F()
593 binary_param_exp_test (1, btor_exp_bv_srl); in TEST_F()
|
| H A D | test_exp.cpp | 765 shift_exp_test (5, 5, btor_exp_bv_srl); in TEST_F()
|
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorexp.c | 48 return btor_exp_bv_srl (btor, e[0], e[1]); in btor_exp_create()
1132 btor_exp_bv_srl (Btor *btor, BtorNode *e0, BtorNode *e1) in btor_exp_bv_srl() function
1167 srl1 = btor_exp_bv_srl (btor, e0, e1); in btor_exp_bv_sra()
1168 srl2 = btor_exp_bv_srl (btor, btor_node_invert (e0), e1); in btor_exp_bv_sra()
1209 rshift = btor_exp_bv_srl (btor, e0, dbits); in exp_rotate()
1214 rshift = btor_exp_bv_srl (btor, e0, nbits); in exp_rotate()
|
| H A D | btorexp.h | 320 BtorNode *btor_exp_bv_srl (Btor *btor, BtorNode *e0, BtorNode *e1);
|
| H A D | btorbeta.c | 395 result = btor_exp_bv_srl (btor, e[1], e[0]); in beta_reduce()
740 result = btor_exp_bv_srl (btor, e[1], e[0]); in beta_reduce_partial_aux()
|
| H A D | btorclone.c | 1834 cur_clone = btor_exp_bv_srl (clone, e[0], e[1]); in btor_clone_recursively_rebuild_exp()
|
| H A D | boolector.c | 2525 res = btor_exp_bv_srl (btor, e0, e1); in boolector_srl()
2534 res = btor_exp_bv_srl (btor, e0, tmp_e1); in boolector_srl()
|
| /dports/math/boolector/boolector-3.2.2/src/utils/ |
| H A D | boolectornodemap.c | 186 case BTOR_BV_SRL_NODE: res = btor_exp_bv_srl (btor, e[0], e[1]); break; in map_node_internal()
|