| /dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/ |
| H A D | arith_intervals.c | 57 init_bvconstant(&a_base); in bvconst_le_base()
58 init_bvconstant(&b_base); in bvconst_le_base()
163 init_bvconstant(&output->lo); in interval_construct()
164 init_bvconstant(&output->hi); in interval_construct()
165 init_bvconstant(&output->length); in interval_construct()
338 init_bvconstant(&aux); in interval_uptrim()
453 init_bvconstant(&aux); in interval_downtrim()
466 init_bvconstant(&lo_light); in interval_downtrim()
467 init_bvconstant(&hi_light); in interval_downtrim()
|
| H A D | arith_utils.c | 61 init_bvconstant(&zero); in arith_zero()
153 init_bvconstant(&half); in arith_add_half()
236 init_bvconstant(&coeff); in arith_eq0()
391 init_bvconstant(&newcoeff); in arith_sum_norm()
|
| H A D | arith.c | 363 init_bvconstant(cc); in bv_arith_init_side()
446 init_bvconstant(&lo); in bv_arith_unit_le()
447 init_bvconstant(&hi); in bv_arith_unit_le()
837 init_bvconstant(&saved_hi_copy); in cover()
877 init_bvconstant(&lo); in cover()
878 init_bvconstant(&hi); in cover()
879 init_bvconstant(&smaller_values); in cover()
908 init_bvconstant(&lo_proj); in cover()
909 init_bvconstant(&hi_proj); in cover()
|
| H A D | arith_norm.c | 367 init_bvconstant(&coeff[i]); in arith_analyse()
742 init_bvconstant(&coeff[i]); in arith_normalise_upto()
|
| H A D | full_bv_sat.c | 280 init_bvconstant(&slice_value); in bb_sat_solver_solve_and_get_core()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
| H A D | bv_evaluator.c | 109 init_bvconstant(value); in bv_evaluator_get_term_cache()
123 init_bvconstant(value_copy); in bv_evaluator_set_term_cache()
155 init_bvconstant(out_value); in bv_evaluator_run_bv_array()
212 init_bvconstant(out_value); in bv_evaluator_run_composite_term()
294 init_bvconstant(out_value); in bv_evaluator_run_term()
306 init_bvconstant(out_value); in bv_evaluator_run_term()
313 init_bvconstant(out_value); in bv_evaluator_run_term()
337 init_bvconstant(out_value); in bv_evaluator_run_term()
349 init_bvconstant(out_value); in bv_evaluator_run_term()
391 init_bvconstant(out_value); in bv_evaluator_run_term()
[all …]
|
| H A D | bv_plugin.c | 700 init_bvconstant(&x_bv_value); in bv_plugin_process_unit_constraint()
|
| H A D | bv_bdd_manager.c | 68 init_bvconstant(&term_info->value); in term_info_construct()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/ |
| H A D | value.c | 52 init_bvconstant(&value->bv_value); in mcsat_value_construct_bv_value()
74 init_bvconstant(&value->bv_value); in mcsat_value_construct_copy()
89 init_bvconstant(&t_bvconst); in mcsat_value_construct_from_constant_term()
100 init_bvconstant(&t_bvconst); in mcsat_value_construct_from_constant_term()
|
| /dports/math/yices/yices-2.6.2/src/terms/ |
| H A D | bvarith_buffer_terms.c | 268 init_bvconstant(&c); in bvarith_buffer_add_const_times_term()
287 init_bvconstant(&c); in bvarith_buffer_add_const_times_term()
332 init_bvconstant(&c); in bvarith_buffer_mul_term_power()
|
| H A D | bvfactor_buffers.c | 40 init_bvconstant(&b->constant); in init_bvfactor_buffer()
43 init_bvconstant(&b->aux); in init_bvfactor_buffer()
|
| H A D | bv_constants.h | 111 extern void init_bvconstant(bvconstant_t *b);
|
| H A D | bv_constants.c | 213 void init_bvconstant(bvconstant_t *b) { in init_bvconstant() function
|
| H A D | term_manager.c | 66 init_bvconstant(&manager->bv0); in init_term_manager()
67 init_bvconstant(&manager->bv1); in init_term_manager()
68 init_bvconstant(&manager->bv2); in init_term_manager()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_bv_intervals.c | 444 init_bvconstant(&buffer); in check_sum_unsigned()
479 init_bvconstant(&buffer); in check_sum_signed()
520 init_bvconstant(&buffer); in check_diff_unsigned()
554 init_bvconstant(&buffer); in check_diff_signed()
592 init_bvconstant(&buffer); in check_addmul_unsigned()
626 init_bvconstant(&buffer); in check_addmul_signed()
|
| H A D | test_bvbounds.c | 62 init_bvconstant(&aux); in test_bounds()
|
| /dports/math/yices/yices-2.6.2/src/model/ |
| H A D | fresh_value_maker.c | 300 init_bvconstant(&maker->aux); in init_fresh_val_maker()
|
| H A D | concrete_values.c | 596 init_bvconstant(&table->buffer); in init_value_table()
|
| /dports/math/yices/yices-2.6.2/src/solvers/bv/ |
| H A D | bvexp_table.c | 48 init_bvconstant(&table->bvconst); in init_bvexp_table()
|
| H A D | new_bvsolver.c | 6978 init_bvconstant(&solver->aux1); in init_bv_solver()
6979 init_bvconstant(&solver->aux2); in init_bv_solver()
6980 init_bvconstant(&solver->aux3); in init_bv_solver()
|
| H A D | bvsolver.c | 7178 init_bvconstant(&solver->aux1); in init_bv_solver()
7179 init_bvconstant(&solver->aux2); in init_bv_solver()
7180 init_bvconstant(&solver->aux3); in init_bv_solver()
|
| H A D | bvpoly_dag.c | 255 init_bvconstant(&dag->aux); in init_bvc_dag()
|
| /dports/math/yices/yices-2.6.2/src/parser_utils/ |
| H A D | term_stack2.c | 198 init_bvconstant(&stack->bvconst_buffer); in alloc_tstack()
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | context.c | 5543 init_bvconstant(&ctx->bv_buffer); in init_context()
|
| /dports/math/yices/yices-2.6.2/src/solvers/egraph/ |
| H A D | egraph.c | 943 init_bvconstant(&mdl->bv_buffer); in init_egraph_model()
|