Home
last modified time | relevance | path

Searched refs:composite_term_desc (Results 1 – 21 of 21) sorted by relevance

/dports/math/yices/yices-2.6.2/src/mcsat/bool/
H A Dcnf.c116 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 Delim_subst.c306 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 Dterms.h1384 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 Dterm_explorer.c498 c = composite_term_desc(table, t); in get_term_children()
H A Dterm_utils.c4151 eq = composite_term_desc(tbl, t); in is_term_eq_const()
/dports/math/yices/yices-2.6.2/src/mcsat/bv/
H A Dbv_bdd_manager.c391 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 Dbv_evaluator.c146 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 Dbv_plugin.c413 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 Dbv_utils.h242 composite_term_t* t_composite = composite_term_desc(terms, t); in bv_term_compute_value()
H A Dbdd_computation.c1234 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 Dcontext_printer.c48 eq = composite_term_desc(terms, e); in print_subst_eq()
H A Dsymmetry_breaking.c1289 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 Dcontext_simplifier.c1332 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 Dsubstitution.c221 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 Deq_ext_con.c927 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 Darith.c1185 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 Darith_norm.c676 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 Duf_plugin.c673 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 Def_analyze.c748 ef_analyze_composite(ef, composite_term_desc(terms, t)); in ef_get_vars()
/dports/math/yices/yices-2.6.2/src/mcsat/
H A Dsolver.c344 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 Dsmt2_commands.c2727 result = composite_needs_egraph(seen, composite_term_desc(terms, t)); in needs_egraph()