Home
last modified time | relevance | path

Searched refs:UNUSED_TERM (Results 1 – 12 of 12) sorted by relevance

/dports/math/yices/yices-2.6.2/src/model/
H A Dterm_to_val.c139 case UNUSED_TERM: in term_to_val()
H A Dliteral_collector.c1480 case UNUSED_TERM: in lit_collector_visit()
/dports/math/yices/yices-2.6.2/src/context/
H A Dshared_terms.c250 case UNUSED_TERM: in sharing_map_visit_subterms()
H A Dcontext_simplifier.c1625 case UNUSED_TERM: in visit()
2179 case UNUSED_TERM: in flatten_assertion()
H A Dsymmetry_breaking.c1229 case UNUSED_TERM: in collect_constants()
/dports/math/yices/yices-2.6.2/src/mcsat/uf/
H A Duf_plugin.c652 …term_kind_t app_kind = UNUSED_TERM, prev_app_kind = UNUSED_TERM; // Kind of the current and previo… in uf_plugin_build_model()
/dports/math/yices/yices-2.6.2/src/io/
H A Dterm_printer.c1042 case UNUSED_TERM: in print_term_idx_recur()
1192 if (tbl->kind[i] != UNUSED_TERM) { in max_term_name_length()
1501 if (tbl->kind[i] != UNUSED_TERM) { in print_term_table()
1646 case UNUSED_TERM: in print_term_idx_desc()
2641 case UNUSED_TERM: in pp_term_idx()
2782 if (kind != UNUSED_TERM && kind != RESERVED_TERM) { in pp_term_table()
/dports/math/yices/yices-2.6.2/src/terms/
H A Dterm_explorer.c302 case UNUSED_TERM: // should not happen in term_num_children()
H A Dterms.h241 UNUSED_TERM, // deleted term enumerator
1141 return valid_term_idx(table, i) && table->kind[i] != UNUSED_TERM; in live_term_idx()
H A Dterms.c1701 case UNUSED_TERM: in delete_term()
1715 table->kind[i] = UNUSED_TERM; in delete_term()
1800 case UNUSED_TERM: in delete_term_descriptors()
3534 case UNUSED_TERM: in mark_reachable_terms()
3714 if (! term_idx_is_marked(table, i) && table->kind[i] != UNUSED_TERM) { in term_table_gc()
H A Dfull_subst.c359 case UNUSED_TERM: in fsubst_explore()
1374 case UNUSED_TERM: in full_subst()
/dports/math/yices/yices-2.6.2/src/frontend/smt2/
H A Dsmt2_commands.c2674 case UNUSED_TERM: in needs_egraph()