| /dports/math/z3/z3-z3-4.8.13/src/test/ |
| H A D | dl_relation.cpp | 34 sig.push_back(int_sort); in test_interval_relation()
35 sig.push_back(int_sort); in test_interval_relation()
36 sig.push_back(int_sort); in test_interval_relation()
37 sig.push_back(int_sort); in test_interval_relation()
139 sig.push_back(int_sort); in test_bound_relation()
140 sig.push_back(int_sort); in test_bound_relation()
157 cond3 = autil.mk_lt(ast_m.mk_var(2, int_sort), ast_m.mk_var(3, int_sort)); in test_bound_relation()
163 lt_x0x1 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(1, int_sort)); in test_bound_relation()
164 lt_x1x2 = autil.mk_lt(ast_m.mk_var(1, int_sort), ast_m.mk_var(2, int_sort)); in test_bound_relation()
165 lt_x0x2 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(2, int_sort)); in test_bound_relation()
[all …]
|
| H A D | value_sweep.cpp | 14 sort_ref int_sort(a.mk_int(), m); in tst_value_sweep() local
17 sort_ref ilist = dt.mk_list_datatype(int_sort, symbol("ilist"), in tst_value_sweep()
20 expr_ref n(m.mk_const("n", int_sort), m); in tst_value_sweep()
|
| H A D | value_generator.cpp | 22 sort_ref int_sort(a.mk_int(), m); in tst1_vg() local
29 sort_ref ilist = dt.mk_list_datatype(int_sort, symbol("ilist"), in tst1_vg()
|
| H A D | qe_arith.cpp | 456 sort* int_sort = a.mk_int(); in test_project() local
457 f = m.mk_func_decl(symbol("f"), 1, &int_sort, int_sort); in test_project()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
| H A D | dl_relation.cpp | 34 sig.push_back(int_sort); in test_interval_relation()
35 sig.push_back(int_sort); in test_interval_relation()
36 sig.push_back(int_sort); in test_interval_relation()
37 sig.push_back(int_sort); in test_interval_relation()
139 sig.push_back(int_sort); in test_bound_relation()
140 sig.push_back(int_sort); in test_bound_relation()
157 cond3 = autil.mk_lt(ast_m.mk_var(2, int_sort), ast_m.mk_var(3, int_sort)); in test_bound_relation()
163 lt_x0x1 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(1, int_sort)); in test_bound_relation()
164 lt_x1x2 = autil.mk_lt(ast_m.mk_var(1, int_sort), ast_m.mk_var(2, int_sort)); in test_bound_relation()
165 lt_x0x2 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(2, int_sort)); in test_bound_relation()
[all …]
|
| H A D | value_sweep.cpp | 14 sort_ref int_sort(a.mk_int(), m); in tst_value_sweep() local
17 sort_ref ilist = dt.mk_list_datatype(int_sort, symbol("ilist"), in tst_value_sweep()
20 expr_ref n(m.mk_const("n", int_sort), m); in tst_value_sweep()
|
| H A D | value_generator.cpp | 22 sort_ref int_sort(a.mk_int(), m); in tst1_vg() local
29 sort_ref ilist = dt.mk_list_datatype(int_sort, symbol("ilist"), in tst1_vg()
|
| H A D | qe_arith.cpp | 456 sort* int_sort = a.mk_int(); in test_project() local
457 f = m.mk_func_decl(symbol("f"), 1, &int_sort, int_sort); in test_project()
|
| /dports/math/z3/z3-z3-4.8.13/examples/c/ |
| H A D | test_capi.c | 926 Z3_sort int_sort; in prove_example2() local
943 g_domain[0] = int_sort; in prove_example2()
1004 Z3_sort int_sort; in push_pop_example1() local
1085 Z3_sort int_sort; in quantifier_example1() local
1112 f_domain[0] = int_sort; in quantifier_example1()
1113 f_domain[1] = int_sort; in quantifier_example1()
1160 Z3_sort int_sort, array_sort; in array_example1() local
1172 array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort); in array_example1()
1690 Z3_sort int_sort; in parser_example3() local
1709 g_domain[0] = int_sort; in parser_example3()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/c/ |
| H A D | test_capi.c | 927 Z3_sort int_sort; in prove_example2() local
944 g_domain[0] = int_sort; in prove_example2()
1005 Z3_sort int_sort; in push_pop_example1() local
1086 Z3_sort int_sort; in quantifier_example1() local
1113 f_domain[0] = int_sort; in quantifier_example1()
1114 f_domain[1] = int_sort; in quantifier_example1()
1161 Z3_sort int_sort, array_sort; in array_example1() local
1173 array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort); in array_example1()
1691 Z3_sort int_sort; in parser_example3() local
1710 g_domain[0] = int_sort; in parser_example3()
[all …]
|
| /dports/archivers/dact/dact-0.8.42/ |
| H A D | sort.h | 24 void int_sort (uint32_t array[], unsigned int listsize, int mode);
|
| H A D | AUTHORS | 24 int_sort:sort.[ch]
|
| H A D | comp_snibble.c | 100 int_sort(freq,4,1); in comp_snibble_compress()
|
| H A D | sort.c | 36 void int_sort (uint32_t array[], unsigned int listsize, int mode) { in int_sort() function
|
| /dports/x11-toolkits/fltk/fltk-1.3.8/src/ |
| H A D | fl_set_fonts_xft.cxx | 343 static int int_sort(const void *aa, const void *bb) { in int_sort() function
376 qsort(array+1, j-1, sizeof(int), int_sort); in get_font_sizes()
|
| /dports/x11-toolkits/ntk/ntk/src/ |
| H A D | fl_set_fonts_xft.cxx | 343 static int int_sort(const void *aa, const void *bb) { in int_sort() function
376 qsort(array+1, j-1, sizeof(int), int_sort); in get_font_sizes()
|
| /dports/math/giacxcas/fltk-1.3.0/src/ |
| H A D | fl_set_fonts_xft.cxx | 343 static int int_sort(const void *aa, const void *bb) { in int_sort() function
376 qsort(array+1, j-1, sizeof(int), int_sort); in get_font_sizes()
|
| /dports/devel/py-buildbot/buildbot-3.4.1/buildbot/worker/ |
| H A D | ec2.py | 300 alpha_sort = int_sort = None
309 int_sort = int(alpha_sort)
312 options.append([int_sort, alpha_sort,
|
| /dports/math/z3/z3-z3-4.8.13/examples/c++/ |
| H A D | example.cpp | 81 sort I = c.int_sort(); in prove_example1()
122 sort I = c.int_sort(); in prove_example2()
372 sort I = c.int_sort(); in quantifier_example()
949 sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() }; in tuple_example()
1241 sort I = c.int_sort(); in recfun_example()
1298 sort I = c.int_sort(); in iterate_args()
|
| /dports/lang/solidity/solidity_0.8.11/libsmtutil/ |
| H A D | Z3Interface.cpp | 387 return m_context.int_sort(); in z3Sort()
422 return m_context.int_sort(); in z3Sort()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/c++/ |
| H A D | example.cpp | 81 sort I = c.int_sort(); in prove_example1()
122 sort I = c.int_sort(); in prove_example2()
372 sort I = c.int_sort(); in quantifier_example()
949 sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() }; in tuple_example()
1241 sort I = c.int_sort(); in recfun_example()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | array_decl_plugin.cpp | 453 sort * int_sort = arith.mk_int(); in mk_set_card() local
454 return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort, in mk_set_card()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | array_decl_plugin.cpp | 453 sort * int_sort = arith.mk_int(); in mk_set_card() local
454 return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort, in mk_set_card()
|
| /dports/devel/py-qutip/qutip-4.6.2/qutip/cy/ |
| H A D | graph_utils.pyx | 60 cdef int int_sort(int_pair x, int_pair y): function
68 cdef cfptr cfptr_ = &int_sort
|
| /dports/math/vampire/vampire-4.5.1/z3/api/ |
| H A D | z3++.h | 238 sort int_sort();
2836 …inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*t… in int_sort() function
3015 inline expr context::int_const(char const * name) { return constant(name, int_sort()); } in int_const()
3025 …inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); r… in int_val()
3026 …inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); ch… in int_val()
3027 …inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_erro… in int_val()
3028 …inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); … in int_val()
3029 …inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); che… in int_val()
|