Home
last modified time | relevance | path

Searched refs:yices_bv_type (Results 1 – 14 of 14) sorted by relevance

/dports/math/yices/yices-2.6.2/tests/unit/
H A Dtest_api1.c216 bv1 = yices_bv_type(1); in test_base_types()
219 bv2 = yices_bv_type(2); in test_base_types()
222 bv32 = yices_bv_type(32); in test_base_types()
225 bv54 = yices_bv_type(54); in test_base_types()
228 bv65 = yices_bv_type(65); in test_base_types()
355 test = yices_bv_type(0); in test_type_errors()
358 test = yices_bv_type(YICES_MAX_BVSIZE); in test_type_errors()
361 test = yices_bv_type(UINT32_MAX); in test_type_errors()
H A Dtest_api10.c101 t_bv = yices_bv_type(32); in init_domain()
166 range[27].type = yices_bv_type(32); in init_range()
168 range[28].type = yices_bv_type(32); in init_range()
170 range[29].type = yices_bv_type(32); in init_range()
H A Dtest_api11.c130 type[1] = yices_bv_type(123); in init_types()
155 tau = yices_bv_type(123); in init_terms()
H A Dtest_api9.c145 type[1] = yices_bv_type(123); in init_types()
170 tau = yices_bv_type(123); in init_terms()
H A Dtest_api3.c518 bv1 = yices_bv_type(1); in init_base_types()
519 bv2 = yices_bv_type(2); in init_base_types()
520 bv12 = yices_bv_type(12); in init_base_types()
521 bv32 = yices_bv_type(32); in init_base_types()
522 bv64 = yices_bv_type(64); in init_base_types()
523 bv65 = yices_bv_type(65); in init_base_types()
524 bv100 = yices_bv_type(100); in init_base_types()
H A Dtest_check_formulas.c17 type_t bv = yices_bv_type(20); in build_formulas()
H A Dtest_bvbounds.c118 bv = yices_bv_type(n); in all_tests()
H A Dtest_export_formulas.c22 type_t bv = yices_bv_type(20); in build_formulas()
H A Dtest_intern_table.c165 ivector_push(&s->types, yices_bv_type(1)); in add_base_types()
166 ivector_push(&s->types, yices_bv_type(32)); in add_base_types()
167 ivector_push(&s->types, yices_bv_type(65)); in add_base_types()
349 add_variables_of_type(s, n, yices_bv_type(1), "u", 0); in add_variables()
350 add_variables_of_type(s, n, yices_bv_type(32), "v", 0); in add_variables()
351 add_variables_of_type(s, n, yices_bv_type(65), "w", 0); in add_variables()
H A Dtest_term_stack.c136 printf("*** yices_bv_type(5) = %"PRId32"\n", yices_bv_type(5)); in main()
/dports/math/yices/yices-2.6.2/examples/
H A Dcheck_formula_examples.c17 type_t bv = yices_bv_type(20); in build_formulas()
/dports/math/py-pysmt/pysmt-0.9.0/pysmt/solvers/
H A Dyices.py638 return yicespy.yices_bv_type(tp.width)
/dports/math/yices/yices-2.6.2/src/include/
H A Dyices.h347 __YICES_DLLSPEC__ extern type_t yices_bv_type(uint32_t size);
/dports/math/yices/yices-2.6.2/src/api/
H A Dyices_api.c2698 EXPORTED type_t yices_bv_type(uint32_t size) { in yices_bv_type() function