Searched refs:btor_exp_bv_ult (Results 1 – 12 of 12) sorted by relevance
/dports/math/boolector/boolector-3.2.2/test/ |
H A D | test_normquant.cpp | 250 ult = btor_exp_bv_ult (d_btor, x, y[1]); in TEST_F() 260 ugte = btor_exp_bv_ult (d_btor, X, Y[1]); in TEST_F() 405 ult = btor_exp_bv_ult (d_btor, xy[0], xy[1]); in TEST_F() 418 ultXY = btor_exp_bv_ult (d_btor, XY[0], XY[1]); in TEST_F() 494 ult = btor_exp_bv_ult (d_btor, x, y); in TEST_F() 515 ultY = btor_exp_bv_ult (d_btor, X, Y[0]); in TEST_F() 516 ultY1 = btor_exp_bv_ult (d_btor, X, Y[1]); in TEST_F() 594 ult = btor_exp_bv_ult (d_btor, v2, y); 611 ultY = btor_exp_bv_ult (d_btor, V[2], Y[0]);
|
H A D | test_prop.cpp | 224 prop_complete_binary (1, btor_exp_bv_ult, btor_bv_ult, inv_ult_bv); in TEST_F() 296 prop_complete_binary (2, btor_exp_bv_ult, btor_bv_ult, inv_ult_bv); in TEST_F()
|
H A D | test_propinv.cpp | 280 ult = btor_exp_bv_ult (d_btor, e[0], e[1]); in check_conf_ult() 296 cult = btor_exp_bv_ult (d_btor, ce, e[1]); in check_conf_ult() 318 cult = btor_exp_bv_ult (d_btor, e[0], ce); in check_conf_ult() 1472 check_binary (btor_exp_bv_ult, btor_bv_ult, inv_ult_bv); in TEST_F()
|
H A D | test_lambda.cpp | 538 binary_param_exp_test (0, btor_exp_bv_ult); in TEST_F() 539 binary_param_exp_test (1, btor_exp_bv_ult); in TEST_F()
|
H A D | test_exp.cpp | 638 binary_non_commutative_exp_test (btor_exp_bv_ult); in TEST_F()
|
/dports/math/boolector/boolector-3.2.2/src/ |
H A D | btorexp.c | 42 return btor_exp_bv_ult (btor, e[0], e[1]); in btor_exp_create() 953 btor_exp_bv_ult (Btor *btor, BtorNode *e0, BtorNode *e1) in btor_exp_bv_ult() function 994 ult = btor_exp_bv_ult (btor, r0, r1); in btor_exp_bv_slt() 1026 ult = btor_exp_bv_ult (btor, e1, e0); in btor_exp_bv_ulte() 1059 return btor_exp_bv_ult (btor, e1, e0); in btor_exp_bv_ugt() 1086 ult = btor_exp_bv_ult (btor, e0, e1); in btor_exp_bv_ugte()
|
H A D | btorexp.h | 255 BtorNode *btor_exp_bv_ult (Btor *btor, BtorNode *e0, BtorNode *e1);
|
H A D | btorbeta.c | 385 result = btor_exp_bv_ult (btor, e[1], e[0]); in beta_reduce() 730 result = btor_exp_bv_ult (btor, e[1], e[0]); in beta_reduce_partial_aux()
|
H A D | btorsynth.c | 1281 INIT_OP (2, false, btor_exp_bv_ult); in init_ops()
|
H A D | btorclone.c | 1828 cur_clone = btor_exp_bv_ult (clone, e[0], e[1]); in btor_clone_recursively_rebuild_exp()
|
H A D | boolector.c | 2262 res = btor_exp_bv_ult (btor, e0, e1); in boolector_ult()
|
/dports/math/boolector/boolector-3.2.2/src/utils/ |
H A D | boolectornodemap.c | 184 case BTOR_BV_ULT_NODE: res = btor_exp_bv_ult (btor, e[0], e[1]); break; in map_node_internal()
|