/dports/math/yices/yices-2.6.2/src/mcsat/bool/ |
H A D | cnf.c | 116 or_composite = composite_term_desc(cnf->ctx->terms, or); in cnf_convert_or() 158 xor_composite = composite_term_desc(cnf->ctx->terms, xor); in cnf_convert_xor() 220 eq_composite = composite_term_desc(cnf->ctx->terms, eq); in cnf_convert_eq() 269 ite_composite = composite_term_desc(cnf->ctx->terms, ite); in cnf_convert_ite()
|
/dports/math/yices/yices-2.6.2/src/terms/ |
H A D | elim_subst.c | 306 eq = composite_term_desc(terms, f); in elim_subst_try_map() 352 eq = composite_term_desc(terms, f); in elim_subst_try_cheap_map()
|
H A D | terms.h | 1384 static inline composite_term_t *composite_term_desc(const term_table_t *table, term_t t) { in composite_term_desc() function 1439 return composite_term_desc(table, t)->arity; in composite_term_arity() 1445 return composite_term_desc(table, t)->arg[i]; in composite_term_arg()
|
H A D | term_explorer.c | 498 c = composite_term_desc(table, t); in get_term_children()
|
H A D | term_utils.c | 4151 eq = composite_term_desc(tbl, t); in is_term_eq_const()
|
/dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
H A D | bv_bdd_manager.c | 391 composite_term_t* atom_comp = composite_term_desc(terms, t); in bv_bdd_manager_ensure_term_data() 408 composite_term_t* t_comp = composite_term_desc(terms, t); in bv_bdd_manager_ensure_term_data() 580 composite_term_t* t_comp = composite_term_desc(terms, t); in bv_bdd_manager_recompute_timestamps() 729 composite_term_t* t_comp = composite_term_desc(terms, t); in bv_bdd_manager_compute_value() 848 composite_term_t* t_comp = composite_term_desc(terms, t); in bv_bdd_manager_compute_bdd()
|
H A D | bv_evaluator.c | 146 composite_term_t* t_composite = composite_term_desc(eval->ctx->terms, t); in bv_evaluator_run_bv_array() 187 composite_term_t* t_composite = composite_term_desc(eval->ctx->terms, t); in bv_evaluator_run_composite_term() 546 composite_term_t* atom_desc = composite_term_desc(terms, t); in bv_evaluator_run_atom() 793 composite_term_t* composite_desc = composite_term_desc(terms, t); in bv_evaluator_not_free_up_to()
|
H A D | bv_plugin.c | 413 composite_term_t* atom_comp = composite_term_desc(terms, current); in bv_plugin_get_notified_term_subvariables() 430 composite_term_t* atom_comp = composite_term_desc(terms, current); in bv_plugin_get_notified_term_subvariables() 481 composite_term_t* current_comp = composite_term_desc(terms, current); in bv_plugin_get_notified_term_subvariables() 492 composite_term_t* current_comp = composite_term_desc(terms, current); in bv_plugin_get_notified_term_subvariables()
|
H A D | bv_utils.h | 242 composite_term_t* t_composite = composite_term_desc(terms, t); in bv_term_compute_value()
|
H A D | bdd_computation.c | 1234 composite_term_t* comp = composite_term_desc(terms, t); in bdds_compute_bdds() 1244 composite_term_t* comp = composite_term_desc(terms, t); in bdds_compute_bdds() 1254 composite_term_t* comp = composite_term_desc(terms, t); in bdds_compute_bdds()
|
/dports/math/yices/yices-2.6.2/src/context/ |
H A D | context_printer.c | 48 eq = composite_term_desc(terms, e); in print_subst_eq()
|
H A D | symmetry_breaking.c | 1289 push_children(queue, cache, composite_term_desc(terms, r)); in collect_constants() 1294 push_last_child(queue, cache, composite_term_desc(terms, r)); in collect_constants()
|
H A D | context_simplifier.c | 1332 eq = composite_term_desc(terms, e); in process_subst_eqs() 2396 d = composite_term_desc(ctx->terms, eq); in process_aux_eq()
|
/dports/math/yices/yices-2.6.2/src/mcsat/utils/ |
H A D | substitution.c | 221 composite_term_t* desc = composite_term_desc(terms, current); in substitution_run_core()
|
/dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/ |
H A D | eq_ext_con.c | 927 composite_term_t* composite_desc = composite_term_desc(terms, t); in term_is_ext_con() 1021 composite_term_t* atom_i_comp = composite_term_desc(terms, atom_i_term); in bv_slicing_construct() 1386 composite_term_t* eq = composite_term_desc(terms, atom_term); in can_explain_conflict()
|
H A D | arith.c | 1185 composite_term_t* atom_i_comp = composite_term_desc(terms, atom_i_term); in bvarith_explain() 1386 composite_term_t* atom_comp = composite_term_desc(terms, atom_term); in can_explain_conflict()
|
H A D | arith_norm.c | 676 composite_term_t* composite_desc = composite_term_desc(terms, t); in arith_normalise_upto()
|
/dports/math/yices/yices-2.6.2/src/mcsat/uf/ |
H A D | uf_plugin.c | 673 composite_term_t* app_comp = composite_term_desc(terms, app_term); in uf_plugin_build_model()
|
/dports/math/yices/yices-2.6.2/src/exists_forall/ |
H A D | ef_analyze.c | 748 ef_analyze_composite(ef, composite_term_desc(terms, t)); in ef_get_vars()
|
/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | solver.c | 344 composite_term_t* eq_desc = composite_term_desc(mcsat->terms, t); in mcsat_evaluates()
|
/dports/math/yices/yices-2.6.2/src/frontend/smt2/ |
H A D | smt2_commands.c | 2727 result = composite_needs_egraph(seen, composite_term_desc(terms, t)); in needs_egraph()
|