/dports/math/yices/yices-2.6.2/src/terms/ |
H A D | bvarith64_buffer_terms.c | 116 case BV_ARRAY: in bvarith64_buffer_add_term() 170 case BV_ARRAY: in bvarith64_buffer_sub_term() 224 case BV_ARRAY: in bvarith64_buffer_mul_term() 275 case BV_ARRAY: in bvarith64_buffer_add_const_times_term() 334 case BV_ARRAY: in bvarith64_buffer_mul_term_power()
|
H A D | bvarith_buffer_terms.c | 118 case BV_ARRAY: in bvarith_buffer_add_term() 172 case BV_ARRAY: in bvarith_buffer_sub_term() 226 case BV_ARRAY: in bvarith_buffer_mul_term() 282 case BV_ARRAY: in bvarith_buffer_add_const_times_term() 348 case BV_ARRAY: in bvarith_buffer_mul_term_power()
|
H A D | term_utils.c | 1338 case BV_ARRAY: in upper_bound_unsigned() 1369 case BV_ARRAY: in lower_bound_unsigned() 1399 case BV_ARRAY: in upper_bound_signed() 1431 case BV_ARRAY: in lower_bound_signed() 1465 case BV_ARRAY: in upper_bound_unsigned64() 1493 case BV_ARRAY: in lower_bound_unsigned64() 2180 case BV_ARRAY: in add_bvterm_to_buffer() 2216 case BV_ARRAY: in sub_bvterm_from_buffer() 2328 case BV_ARRAY: in addmul_bvterm64_to_buffer() 2453 case BV_ARRAY: in addmul_bvterm_to_buffer() [all …]
|
H A D | bvlogic_buffers.c | 1876 case BV_ARRAY: in bvlogic_buffer_set_term() 1926 case BV_ARRAY: in bvlogic_buffer_set_slice_term() 1979 case BV_ARRAY: in bvlogic_buffer_and_term() 2026 case BV_ARRAY: in bvlogic_buffer_or_term() 2073 case BV_ARRAY: in bvlogic_buffer_xor_term() 2123 case BV_ARRAY: in bvlogic_buffer_comp_term() 2173 case BV_ARRAY: in bvlogic_buffer_concat_left_term() 2218 case BV_ARRAY: in bvlogic_buffer_concat_right_term()
|
H A D | free_var_collector.c | 334 case BV_ARRAY: in get_free_vars_of_term()
|
H A D | term_explorer.c | 350 case BV_ARRAY: in term_num_children()
|
H A D | terms.h | 287 BV_ARRAY, // array of boolean terms enumerator 1599 assert(term_kind(table, t) == BV_ARRAY); in bvarray_term_desc()
|
H A D | term_manager.c | 683 term_kind(tbl, t1) == BV_ARRAY && term_kind(tbl, t2) == BV_ARRAY) { in mk_bitvector_eq() 1402 if (kind_y == BV_ARRAY) { in mk_bv_ite() 1412 if (kind_y == BV_ARRAY) { in mk_bv_ite() 1417 case BV_ARRAY: in mk_bv_ite() 1422 } else if (kind_y == BV_ARRAY) { in mk_bv_ite() 4318 if (term_kind(tbl, t) == BV_ARRAY) { in pprod_get_bvarray() 5413 case BV_ARRAY: in mk_bitextract()
|
H A D | full_subst.c | 323 case BV_ARRAY: in fsubst_explore() 1259 case BV_ARRAY: in full_subst_composite()
|
H A D | terms.c | 1590 case BV_ARRAY: in delete_term() 1834 case BV_ARRAY: in delete_term_descriptors() 2672 composite_hobj.tag = BV_ARRAY; in bvarray_term() 3575 case BV_ARRAY: in mark_reachable_terms()
|
H A D | term_substitution.c | 1227 case BV_ARRAY: in subst_composite()
|
/dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
H A D | bv_utils.h | 75 case BV_ARRAY: in bv_term_has_children() 109 case BV_ARRAY: in bv_term_kind_get_type() 241 case BV_ARRAY: { in bv_term_compute_value() 353 case BV_ARRAY: in mk_bv_composite() 424 && term_kind(terms, bit_term_arg(terms, result)) == BV_ARRAY) { in bv_bitterm()
|
H A D | bv_bdd_manager.c | 398 case BV_ARRAY: in bv_bdd_manager_ensure_term_data() 411 assert(t_kind == BV_ARRAY || t_i_bitsize == bitsize); in bv_bdd_manager_ensure_term_data() 412 assert(t_kind != BV_ARRAY || t_i_bitsize == 1); in bv_bdd_manager_ensure_term_data() 570 case BV_ARRAY: in bv_bdd_manager_recompute_timestamps() 719 case BV_ARRAY: in bv_bdd_manager_compute_value() 838 case BV_ARRAY: in bv_bdd_manager_compute_bdd()
|
H A D | bv_evaluator.c | 142 assert(term_kind(terms, t) == BV_ARRAY); in bv_evaluator_run_bv_array() 240 case BV_ARRAY: in bv_evaluator_run_composite_term() 318 case BV_ARRAY: in bv_evaluator_run_term() 856 case BV_ARRAY: { in bv_evaluator_not_free_up_to()
|
H A D | bv_plugin.c | 154 ctx->request_term_notification_by_kind(ctx, BV_ARRAY); in bv_plugin_construct() 436 case BV_ARRAY: { in bv_plugin_get_notified_term_subvariables()
|
/dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/ |
H A D | arith_norm.c | 206 assert(term_kind(terms, base) != BV_ARRAY); in analyse_bvarray() 389 case BV_ARRAY: { // Concatenated boolean terms in arith_analyse() 767 case BV_ARRAY: { // Concatenated boolean terms in arith_normalise_upto() 793 assert(term_kind(terms, base) != BV_ARRAY); in arith_normalise_upto() 840 assert(term_kind(terms, base) != BV_ARRAY); in arith_normalise_upto()
|
H A D | eq_ext_con.c | 466 if (term_kind(terms, arg) == BV_ARRAY) { in bit_over_extract() 497 if ((!is_evaluable) && (term_kind(terms, t) == BV_ARRAY)) { in bv_slicing_norm() 785 if (t_kind == BV_ARRAY) { in term_is_ext_con() 922 case BV_ARRAY: { in term_is_ext_con()
|
/dports/math/yices/yices-2.6.2/src/mcsat/utils/ |
H A D | substitution.c | 49 case BV_ARRAY: in mk_composite() 208 case BV_ARRAY: in substitution_run_core()
|
/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | preprocessor.c | 133 case BV_ARRAY: in get_composite() 206 case BV_ARRAY: in mk_composite() 464 case BV_ARRAY: in preprocessor_apply()
|
/dports/math/yices/yices-2.6.2/src/context/ |
H A D | shared_terms.c | 214 case BV_ARRAY: in sharing_map_visit_subterms()
|
H A D | internalization_table.c | 602 case BV_ARRAY:
|
/dports/math/yices/yices-2.6.2/src/model/ |
H A D | model_support.c | 397 case BV_ARRAY: in get_term_support()
|
H A D | literal_collector.c | 1408 case BV_ARRAY: in lit_collector_visit()
|
/dports/math/yices/yices-2.6.2/src/io/ |
H A D | term_printer.c | 981 case BV_ARRAY: in print_term_idx_recur() 1588 case BV_ARRAY: in print_term_table() 1715 case BV_ARRAY: in print_term_idx_desc() 2609 case BV_ARRAY: in pp_term_idx()
|
/dports/math/yices/yices-2.6.2/src/exists_forall/ |
H A D | ef_analyze.c | 736 case BV_ARRAY: in ef_get_vars()
|