| /dports/math/yices/yices-2.6.2/src/scratch/ |
| H A D | flattening.c | 148 d = or_term_desc(terms, t); in flattener_build_conjuncts()
244 d = or_term_desc(terms, t); in flattener_build_disjuncts()
341 d = or_term_desc(terms, t); in flattener_forall_conjuncts()
451 d = or_term_desc(terms, t); in flattener_forall_disjuncts()
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | common_conjuncts.c | 108 or = or_term_desc(terms, t); in bfs_collect_conjuncts()
166 or = or_term_desc(terms, t); in bfs_collect_disjuncts()
|
| H A D | eq_learner.c | 347 a = eq_abstract_or(learner, or_term_desc(terms, f), polarity); in eq_abstract()
|
| H A D | symmetry_breaking.c | 561 push_children(queue, cache, or_term_desc(terms, r)); in formula_is_range_constraint()
961 x = ctx_subst_or(s, or_term_desc(terms, r)); in ctx_subst()
|
| H A D | conditional_definitions.c | 734 cond_def_explore_or(c, or_term_desc(terms, f), is_pos_term(f)); in cond_def_explore()
|
| H A D | context_simplifier.c | 2051 d = or_term_desc(ctx->terms, r); in flatten_or()
2609 or = or_term_desc(terms, t); in flatten_or_process_queue()
|
| H A D | context.c | 3149 l = map_or_to_literal(ctx, or_term_desc(terms, r)); in internalize_to_literal()
4592 assert_toplevel_or(ctx, or_term_desc(terms, t), tt); in assert_toplevel_formula()
4725 assert_toplevel_or(ctx, or_term_desc(terms, t), tt); in assert_term()
|
| /dports/math/yices/yices-2.6.2/src/exists_forall/ |
| H A D | ef_analyze.c | 252 b = or_term_desc(terms, t); in ef_flatten_distribute()
356 d = or_term_desc(terms, t); in ef_flatten_quantifiers_conjuncts()
548 d = or_term_desc(terms, t); in ef_build_disjuncts()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
| H A D | bv_utils.h | 251 composite_term_t* t_composite = or_term_desc(terms, t); in bv_term_compute_value()
|
| H A D | bv_evaluator.c | 514 composite_term_t* t_comp = or_term_desc(terms, t); in bv_evaluator_run_atom()
|
| H A D | bv_plugin.c | 451 composite_term_t* current_comp = or_term_desc(terms, current); in bv_plugin_get_notified_term_subvariables()
|
| H A D | bdd_computation.c | 1222 assert(children_bdds->size == or_term_desc(terms, t)->arity); in bdds_compute_bdds()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/ |
| H A D | preprocessor.c | 108 return or_term_desc(terms, t); in get_composite()
|
| /dports/math/yices/yices-2.6.2/src/terms/ |
| H A D | terms.h | 1563 static inline composite_term_t *or_term_desc(const term_table_t *table, term_t t) { in or_term_desc() function
|
| H A D | full_subst.c | 1232 s = full_subst_or(subst, or_term_desc(terms, t)); in full_subst_composite()
|
| H A D | term_substitution.c | 1200 result = subst_or(subst, or_term_desc(terms, t)); in subst_composite()
|
| /dports/math/yices/yices-2.6.2/src/model/ |
| H A D | literal_collector.c | 1381 u = lit_collector_visit_or_formula(collect, t, or_term_desc(terms, t)); in lit_collector_visit()
|
| H A D | model_eval.c | 1298 v = eval_or(eval, or_term_desc(terms, t)); in eval_term()
|
| /dports/math/yices/yices-2.6.2/src/io/ |
| H A D | term_printer.c | 2028 d = or_term_desc(tbl, t); in p_score()
|