Home
last modified time | relevance | path

Searched refs:btor_exp_var (Results 1 – 18 of 18) sorted by relevance

/dports/math/boolector/boolector-3.2.2/test/
H A Dtest_unionfind.cpp40 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 Dtest_lambda.cpp773 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 Dtest_nodemap.cpp37 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 Dtest_exp.cpp27 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 Dtest_propinv.cpp93 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 Dtest_normquant.cpp400 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 Dtest_prop.cpp71 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 Dbtorelimslices.c289 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 Dbtorunconstrained.c74 subst = btor_exp_var (btor, btor_node_get_sort_id (exp), 0); in mark_uc()
H A Dbtorskolemize.c121 result = btor_exp_var (btor, real_cur->sort_id, buf); in btor_skolemize_node()
H A Dbtornormquant.c68 result = btor_exp_var (btor, ite->sort_id, buf); in create_skolem_ite()
/dports/math/boolector/boolector-3.2.2/src/
H A Dbtorexp.h27 BtorNode *btor_exp_var (Btor *btor, BtorSortId sort, const char *symbol);
H A Dbtorslvquant.c692 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 Dbtorcore.c1461 lambda = btor_exp_var (btor, sort, 0); in normalize_substitution()
1482 lambda = btor_exp_var (btor, sort, 0); in normalize_substitution()
H A Dbtorclone.c1771 cur_clone = btor_exp_var (clone, sort, symbol); in btor_clone_recursively_rebuild_exp()
H A Dbtorexp.c86 btor_exp_var (Btor *btor, BtorSortId sort, const char *symbol) in btor_exp_var() function
H A Dbtorslvfun.c473 var = btor_exp_var (btor, sort, 0); in create_function_inequality()
H A Dboolector.c1608 res = btor_exp_var (btor, s, symb); in boolector_var()