| /dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/ |
| H A D | arith_utils.c | 25 bvconst64_term_t* desc = bvconst64_term_desc(terms,t); in arith_is_zero()
37 bvconst64_term_t* desc = bvconst64_term_desc(terms,t); in arith_is_one()
49 bvconst64_term_t* desc = bvconst64_term_desc(terms,t); in arith_is_minus_one()
|
| /dports/math/yices/yices-2.6.2/src/terms/ |
| H A D | term_manager.c | 601 bvconst64_term_t *c; in term_is_bveq1()
1206 …erm_t mk_bvconst64_ite(term_manager_t *manager, term_t c, bvconst64_term_t *u, bvconst64_term_t *v… in mk_bvconst64_ite()
4799 bvconst64_term_t *u; in term_is_bvzero()
4931 bvconst64_term_t *u; in term_is_bvashr_invariant()
5006 static int32_t bvconst64_term_is_power_of_two(bvconst64_term_t *b) { in bvconst64_term_is_power_of_two()
5030 static term_t bvdiv_const64(term_manager_t *manager, bvconst64_term_t *a, bvconst64_term_t *b) { in bvdiv_const64()
5115 static term_t bvrem_const64(term_manager_t *manager, bvconst64_term_t *a, bvconst64_term_t *b) { in bvrem_const64()
5200 static term_t bvsdiv_const64(term_manager_t *manager, bvconst64_term_t *a, bvconst64_term_t *b) { in bvsdiv_const64()
5260 static term_t bvsrem_const64(term_manager_t *manager, bvconst64_term_t *a, bvconst64_term_t *b) { in bvsrem_const64()
5320 static term_t bvsmod_const64(term_manager_t *manager, bvconst64_term_t *a, bvconst64_term_t *b) { in bvsmod_const64()
[all …]
|
| H A D | bvlogic_buffers.c | 1856 bvconst64_term_t *c64; in bvlogic_buffer_set_term()
1905 bvconst64_term_t *c64; in bvlogic_buffer_set_slice_term()
1958 bvconst64_term_t *c64; in bvlogic_buffer_and_term()
2005 bvconst64_term_t *c64; in bvlogic_buffer_or_term()
2052 bvconst64_term_t *c64; in bvlogic_buffer_xor_term()
2102 bvconst64_term_t *c64; in bvlogic_buffer_comp_term()
2153 bvconst64_term_t *c64; in bvlogic_buffer_concat_left_term()
2198 bvconst64_term_t *c64; in bvlogic_buffer_concat_right_term()
|
| H A D | terms.h | 410 } bvconst64_term_t; typedef
1194 static inline bvconst64_term_t *bvconst64_for_idx(const term_table_t *table, int32_t i) { in bvconst64_for_idx()
1196 return (bvconst64_term_t *) table->desc[i].ptr; in bvconst64_for_idx()
1413 static inline bvconst64_term_t *bvconst64_term_desc(const term_table_t *table, term_t t) { in bvconst64_term_desc()
|
| H A D | terms.c | 448 static bvconst64_term_t *new_bvconst64_term(uint32_t bitsize, uint64_t v) { in new_bvconst64_term()
449 bvconst64_term_t *d; in new_bvconst64_term()
453 d = (bvconst64_term_t *) safe_malloc(sizeof(bvconst64_term_t)); in new_bvconst64_term()
1152 bvconst64_term_t *d; in eq_bvconst64_hobj()
1278 bvconst64_term_t *c; in build_bvconst64_hobj()
1535 bvconst64_term_t *c64; in delete_term()
|
| H A D | term_explorer.c | 638 bvconst64_term_t *bv64; in bv_const_value()
|
| H A D | term_utils.c | 739 static bool disequal_bitarray_bvconst64(composite_term_t *a, bvconst64_term_t *c) { in disequal_bitarray_bvconst64()
1310 static void copy_bvconst64_term(bvconst64_term_t *a, bvconstant_t *c) { in copy_bvconst64_term()
2650 static void bvfactor_const64(bvfactor_buffer_t *b, bvconst64_term_t *c, uint32_t d) { in bvfactor_const64()
3180 static term_t check_eq_bvconst64(bvconst64_term_t *u, composite_term_t *v) { in check_eq_bvconst64()
3302 static void flatten_eq_bvconst64(bvconst64_term_t *u, composite_term_t *v, ivector_t *a) { in flatten_eq_bvconst64()
|
| /dports/math/yices/yices-2.6.2/src/model/ |
| H A D | term_to_val.c | 94 static value_t term_to_bv64_constant(term_converter_t *convert, bvconst64_term_t *d) { in term_to_bv64_constant()
|
| H A D | model_eval.c | 168 static value_t eval_bv64_constant(evaluator_t *eval, bvconst64_term_t *c) { in eval_bv64_constant()
|
| /dports/math/yices/yices-2.6.2/src/solvers/bv/ |
| H A D | new_bvsolver.h | 80 extern thvar_t bv_solver_create_const64(bv_solver_t *solver, bvconst64_term_t *c);
|
| H A D | bvsolver.h | 96 extern thvar_t bv_solver_create_const64(bv_solver_t *solver, bvconst64_term_t *c);
|
| H A D | new_bvsolver.c | 5108 thvar_t bv_solver_create_const64(bv_solver_t *solver, bvconst64_term_t *c) { in bv_solver_create_const64()
|
| H A D | bvsolver.c | 5277 thvar_t bv_solver_create_const64(bv_solver_t *solver, bvconst64_term_t *c) { in bv_solver_create_const64()
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | context_types.h | 551 typedef thvar_t (*create_bv64_const_fun_t)(void *solver, bvconst64_term_t *c);
|
| H A D | context.c | 628 static occ_t map_bvconst64_to_eterm(context_t *ctx, bvconst64_term_t *c) { in map_bvconst64_to_eterm()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/ |
| H A D | value.c | 98 bvconst64_term_t* t_desc = bvconst64_term_desc(terms, t); in mcsat_value_construct_from_constant_term()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_api1.c | 753 bvconst64_term_t *c; in check_bv64_constant()
|
| H A D | test_terms.c | 1844 bvconst64_term_t *d; in check_bvconst64()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
| H A D | bv_evaluator.c | 312 bvconst64_term_t* t_desc = bvconst64_term_desc(terms, t); in bv_evaluator_run_term()
|
| H A D | bv_bdd_manager.c | 474 bvconst64_term_t* t_desc = bvconst64_term_desc(terms, t); in bv_bdd_manager_ensure_term_data()
|
| /dports/math/yices/yices-2.6.2/src/io/ |
| H A D | term_printer.c | 863 static void print_bvconst64_term(FILE *f, bvconst64_term_t *d) { in print_bvconst64_term()
2331 static void pp_bvconst64_term(yices_pp_t *printer, bvconst64_term_t *d) { in pp_bvconst64_term()
|
| /dports/math/yices/yices-2.6.2/src/parser_utils/ |
| H A D | term_stack2.c | 2555 bvconst64_term_t *d64; in bvconstant_copy_term()
|