/dports/math/boolector/boolector-3.2.2/test/ |
H A D | test_unionfind.cpp | 40 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 59 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 60 BtorNode *y = btor_exp_var (d_btor, d_sort, "y"); in TEST_F() 77 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 78 BtorNode *y = btor_exp_var (d_btor, d_sort, "y"); in TEST_F() 79 BtorNode *z = btor_exp_var (d_btor, d_sort, "z"); in TEST_F() 97 BtorNode *w = btor_exp_var (d_btor, d_sort, "w"); in TEST_F() 98 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 99 BtorNode *y = btor_exp_var (d_btor, d_sort, "y"); in TEST_F() 100 BtorNode *z = btor_exp_var (d_btor, d_sort, "z"); in TEST_F() [all …]
|
H A D | test_lambda.cpp | 773 v1 = btor_exp_var (d_btor, sort, "v1"); in TEST_F() 805 v1 = btor_exp_var (d_btor, sort, "v1"); in TEST_F() 837 v1 = btor_exp_var (d_btor, sort, "v1"); in TEST_F() 920 v = btor_exp_var (d_btor, d_index_sort, "v"); in TEST_F() 1090 i = btor_exp_var (d_btor, d_index_sort, "i"); in TEST_F() 1270 i = btor_exp_var (d_btor, sort, 0); in TEST_F() 1271 e = btor_exp_var (d_btor, sort, 0); in TEST_F() 1295 i = btor_exp_var (d_btor, sort, 0); in TEST_F() 1296 e = btor_exp_var (d_btor, sort, 0); in TEST_F() 1327 v = btor_exp_var (d_btor, sort, 0); in TEST_F() [all …]
|
H A D | test_nodemap.cpp | 37 s = btor_exp_var (btor_a, sort, "s"); in TEST_F() 41 d = btor_exp_var (btor_b, sort, "d"); in TEST_F() 65 s = btor_exp_var (btor_a, sort, "0"); in TEST_F() 66 t = btor_exp_var (btor_a, sort, "1"); in TEST_F()
|
H A D | test_exp.cpp | 27 exp1 = btor_exp_var (d_btor, sort, "v1"); in unary_exp_test() 67 exp1 = btor_exp_var (d_btor, sort, "v1"); in ext_exp_test() 88 exp1 = btor_exp_var (d_btor, sort, "v1"); in binary_commutative_exp_test() 89 exp2 = btor_exp_var (d_btor, sort, "v2"); in binary_commutative_exp_test() 128 exp1 = btor_exp_var (d_btor, sort, "v1"); in binary_non_commutative_exp_test() 129 exp2 = btor_exp_var (d_btor, sort, "v2"); in binary_non_commutative_exp_test() 172 exp1 = btor_exp_var (d_btor, sort, "v1"); in mulo_exp_test() 173 exp2 = btor_exp_var (d_btor, sort, "v2"); in mulo_exp_test() 203 exp1 = btor_exp_var (d_btor, sort, "v1"); in shift_exp_test() 470 exp1 = btor_exp_var (d_btor, sort, "v1"); in TEST_F() [all …]
|
H A D | test_propinv.cpp | 93 e[0] = btor_exp_var (d_btor, sort, 0); in check_binary() 94 e[1] = btor_exp_var (d_btor, sort, 0); in check_binary() 135 e[0] = btor_exp_var (d_btor, sort, 0); in check_shift() 136 e[1] = btor_exp_var (d_btor, sort, 0); in check_shift() 170 e[0] = btor_exp_var (d_btor, sort, 0); in check_conf_and() 171 e[1] = btor_exp_var (d_btor, sort, 0); in check_conf_and() 277 e[0] = btor_exp_var (d_btor, sort, 0); in check_conf_ult() 278 e[1] = btor_exp_var (d_btor, sort, 0); in check_conf_ult() 369 e[0] = btor_exp_var (d_btor, sort, 0); in check_conf_sll() 370 e[1] = btor_exp_var (d_btor, sort, 0); in check_conf_sll() [all …]
|
H A D | test_normquant.cpp | 400 v = btor_exp_var (d_btor, sort, "v"); in TEST_F() 401 v0 = btor_exp_var (d_btor, sort, "v0"); in TEST_F() 402 v1 = btor_exp_var (d_btor, sort, "v1"); in TEST_F() 490 v0 = btor_exp_var (d_btor, sort, "v0"); in TEST_F() 491 v1 = btor_exp_var (d_btor, sort, "v1"); in TEST_F() 590 v0 = btor_exp_var (d_btor, 32, "v0"); 591 v1 = btor_exp_var (d_btor, 32, "v1"); 592 v2 = btor_exp_var (d_btor, 32, "v2");
|
H A D | test_prop.cpp | 71 e[0] = btor_exp_var (d_btor, sort, 0); in prop_complete_binary_eidx() 72 e[1] = btor_exp_var (d_btor, sort, 0); in prop_complete_binary_eidx() 363 e = btor_exp_var (d_btor, sort, 0); in TEST_F()
|
/dports/math/boolector/boolector-3.2.2/src/preprocess/ |
H A D | btorelimslices.c | 289 result = btor_exp_var (btor, sort, 0); in btor_eliminate_slices_on_bv_vars() 296 lambda_var = btor_exp_var (btor, sort, 0); in btor_eliminate_slices_on_bv_vars()
|
H A D | btorunconstrained.c | 74 subst = btor_exp_var (btor, btor_node_get_sort_id (exp), 0); in mark_uc()
|
H A D | btorskolemize.c | 121 result = btor_exp_var (btor, real_cur->sort_id, buf); in btor_skolemize_node()
|
H A D | btornormquant.c | 68 result = btor_exp_var (btor, ite->sort_id, buf); in create_skolem_ite()
|
/dports/math/boolector/boolector-3.2.2/src/ |
H A D | btorexp.h | 27 BtorNode *btor_exp_var (Btor *btor, BtorSortId sort, const char *symbol);
|
H A D | btorslvquant.c | 692 var = btor_exp_var (res->forall, cur->sort_id, 0); in setup_solvers() 712 var = btor_exp_var (res->forall, cur->sort_id, 0); in setup_solvers() 763 var = btor_exp_var (res->exists, dsortid, sym); in setup_solvers()
|
H A D | btorcore.c | 1461 lambda = btor_exp_var (btor, sort, 0); in normalize_substitution() 1482 lambda = btor_exp_var (btor, sort, 0); in normalize_substitution()
|
H A D | btorclone.c | 1771 cur_clone = btor_exp_var (clone, sort, symbol); in btor_clone_recursively_rebuild_exp()
|
H A D | btorexp.c | 86 btor_exp_var (Btor *btor, BtorSortId sort, const char *symbol) in btor_exp_var() function
|
H A D | btorslvfun.c | 473 var = btor_exp_var (btor, sort, 0); in create_function_inequality()
|
H A D | boolector.c | 1608 res = btor_exp_var (btor, s, symb); in boolector_var()
|