| /dports/math/gnumeric/gnumeric-1.12.50/src/ |
| H A D | stf-parse.c | 1506 int_sort (void const *a, void const *b) in int_sort() function
1543 qsort (counts, cno, sizeof (counts[0]), int_sort); in count_character()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/c++/ |
| H A D | z3++.h | 246 sort int_sort();
2993 …inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*t… in int_sort() function
3172 inline expr context::int_const(char const * name) { return constant(name, int_sort()); } in int_const()
3182 …inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); r… in int_val()
3183 …inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); ch… in int_val()
3184 …inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_erro… in int_val()
3185 …inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); … in int_val()
3186 …inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); che… in int_val()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_bv.cpp | 606 sort * int_sort = n->get_sort(); in assert_bv2int_axiom() local
614 expr_ref zero(m_autil.mk_numeral(numeral(0), int_sort), m); in assert_bv2int_axiom()
633 expr_ref n(m_autil.mk_numeral(num, int_sort), m); in assert_bv2int_axiom()
|
| H A D | theory_str.cpp | 484 sort * int_sort = m.mk_sort(m_autil.get_family_id(), INT_SORT); in mk_int_var() local
485 app * a = mk_fresh_const(name.c_str(), int_sort); in mk_int_var()
6666 sort * int_sort = m.mk_sort(m_arith_fid, INT_SORT); in set_up_axioms() local
6739 } else if (ex_sort == int_sort) { in set_up_axioms()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_bv.cpp | 605 sort * int_sort = m.get_sort(n); in assert_bv2int_axiom() local
613 expr_ref zero(m_autil.mk_numeral(numeral(0), int_sort), m); in assert_bv2int_axiom()
632 expr_ref n(m_autil.mk_numeral(num, int_sort), m); in assert_bv2int_axiom()
|
| H A D | theory_str.cpp | 560 sort * int_sort = m.mk_sort(m_autil.get_family_id(), INT_SORT); in mk_int_var() local
561 app * a = mk_fresh_const(name.c_str(), int_sort); in mk_int_var()
6872 sort * int_sort = m.mk_sort(m_arith_fid, INT_SORT); in set_up_axioms() local
6941 } else if (ex_sort == int_sort) { in set_up_axioms()
|
| /dports/math/z3/z3-z3-4.8.13/src/api/c++/ |
| H A D | z3++.h | 247 sort int_sort();
3265 …inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*t… in int_sort() function
3434 inline expr context::int_const(char const * name) { return constant(name, int_sort()); } in int_const()
3458 …inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); r… in int_val()
3459 …inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); ch… in int_val()
3460 …inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_erro… in int_val()
3461 …inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); … in int_val()
3462 …inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); che… in int_val()
|
| /dports/math/vampire/vampire-4.5.1/SAT/ |
| H A D | Z3Interfacing.cpp | 314 if(s==Sorts::SRT_INTEGER) return _context.int_sort(); in getz3sort()
|
| /dports/math/z3/z3-z3-4.8.13/src/api/julia/ |
| H A D | z3jl.cpp | 612 .MM(context, int_sort) in define_julia_module()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/julia/ |
| H A D | z3jl.cpp | 614 .MM(context, int_sort) in define_julia_module()
|
| /dports/math/z3/z3-z3-4.8.13/examples/tptp/ |
| H A D | tptp5.cpp | 1123 m_defined_sorts.insert(symbol("$int"), m_context.int_sort()); in env()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/tptp/ |
| H A D | tptp5.cpp | 1123 m_defined_sorts.insert(symbol("$int"), m_context.int_sort()); in env()
|