Home
last modified time | relevance | path

Searched refs:btor_exp_bv_ult (Results 1 – 12 of 12) sorted by relevance

/dports/math/boolector/boolector-3.2.2/test/
H A Dtest_normquant.cpp250 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 Dtest_prop.cpp224 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 Dtest_propinv.cpp280 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 Dtest_lambda.cpp538 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 Dtest_exp.cpp638 binary_non_commutative_exp_test (btor_exp_bv_ult); in TEST_F()
/dports/math/boolector/boolector-3.2.2/src/
H A Dbtorexp.c42 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 Dbtorexp.h255 BtorNode *btor_exp_bv_ult (Btor *btor, BtorNode *e0, BtorNode *e1);
H A Dbtorbeta.c385 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 Dbtorsynth.c1281 INIT_OP (2, false, btor_exp_bv_ult); in init_ops()
H A Dbtorclone.c1828 cur_clone = btor_exp_bv_ult (clone, e[0], e[1]); in btor_clone_recursively_rebuild_exp()
H A Dboolector.c2262 res = btor_exp_bv_ult (btor, e0, e1); in boolector_ult()
/dports/math/boolector/boolector-3.2.2/src/utils/
H A Dboolectornodemap.c184 case BTOR_BV_ULT_NODE: res = btor_exp_bv_ult (btor, e[0], e[1]); break; in map_node_internal()