73 void init_term_subst(term_subst_t *subst, term_manager_t *mngr, uint32_t n, const term_t *v, const …  in init_term_subst()
100 void reset_term_subst(term_subst_t *subst) {  in reset_term_subst()
119 void extend_term_subst(term_subst_t *subst, uint32_t n, const term_t *v, const term_t *t, bool rese…  in extend_term_subst()
145 bool term_subst_var_in_domain(term_subst_t *subst, term_t v) {  in term_subst_var_in_domain()
155 term_t term_subst_var_mapping(term_subst_t *subst, term_t v) {  in term_subst_var_mapping()
185 void term_subst_domain(term_subst_t *subst, ivector_t *d) {  in term_subst_domain()
194 void delete_term_subst(term_subst_t *subst) {  in delete_term_subst()
214 static renaming_ctx_t *term_subst_get_rctx(term_subst_t *subst) {  in term_subst_get_rctx()
234 static term_t get_subst_of_var(term_subst_t *subst, term_t x) {  in get_subst_of_var()
261 static term_t get_subst_of_unint(term_subst_t *subst, term_t x) {  in get_subst_of_unint()
283 static term_t get_cached_subst(term_subst_t *subst, term_t t) {  in get_cached_subst()
305 static void cache_subst_result(term_subst_t *subst, term_t t, term_t u) {  in cache_subst_result()
327 static void subst_push_renaming(term_subst_t *subst, uint32_t n, term_t *v) {  in subst_push_renaming()
339 static void subst_pop_renaming(term_subst_t *subst, uint32_t n) {  in subst_pop_renaming()
438   term_subst_t subst;  in apply_beta_rule()  local
510 static term_t subst_forall(term_subst_t *subst, composite_term_t *d) {  in subst_forall()
545 static term_t subst_lambda(term_subst_t *subst, composite_term_t *d) {  in subst_lambda()
580 static term_t *subst_children(term_subst_t *subst, composite_term_t *d) {  in subst_children()
599 static term_t subst_arith_eq(term_subst_t *subst, term_t t) {  in subst_arith_eq()
607 static term_t subst_arith_ge(term_subst_t *subst, term_t t) {  in subst_arith_ge()
615 static term_t subst_arith_is_int(term_subst_t *subst, term_t t) {  in subst_arith_is_int()
623 static term_t subst_arith_floor(term_subst_t *subst, term_t t) {  in subst_arith_floor()
631 static term_t subst_arith_ceil(term_subst_t *subst, term_t t) {  in subst_arith_ceil()
639 static term_t subst_arith_abs(term_subst_t *subst, term_t t) {  in subst_arith_abs()
647 static term_t subst_ite(term_subst_t *subst, composite_term_t *d) {  in subst_ite()
675 static term_t subst_app(term_subst_t *subst, composite_term_t *d) {  in subst_app()
691 static term_t subst_update(term_subst_t *subst, composite_term_t *d) {  in subst_update()
708 static term_t subst_tuple(term_subst_t *subst, composite_term_t *d) {  in subst_tuple()
720 static term_t subst_eq(term_subst_t *subst, composite_term_t *d) {  in subst_eq()
730 static term_t subst_distinct(term_subst_t *subst, composite_term_t *d) {  in subst_distinct()
742 static term_t subst_or(term_subst_t *subst, composite_term_t *d) {  in subst_or()
767 static term_t subst_xor(term_subst_t *subst, composite_term_t *d) {  in subst_xor()
780 static term_t subst_arith_bineq(term_subst_t *subst, composite_term_t *d) {  in subst_arith_bineq()
790 static term_t subst_arith_rdiv(term_subst_t *subst, composite_term_t *d) {  in subst_arith_rdiv()
800 static term_t subst_arith_idiv(term_subst_t *subst, composite_term_t *d) {  in subst_arith_idiv()
810 static term_t subst_arith_mod(term_subst_t *subst, composite_term_t *d) {  in subst_arith_mod()
820 static term_t subst_arith_divides(term_subst_t *subst, composite_term_t *d) {  in subst_arith_divides()
830 static term_t subst_bvarray(term_subst_t *subst, composite_term_t *d) {  in subst_bvarray()
843 static term_t subst_bvdiv(term_subst_t *subst, composite_term_t *d) {  in subst_bvdiv()
852 static term_t subst_bvrem(term_subst_t *subst, composite_term_t *d) {  in subst_bvrem()
861 static term_t subst_bvsdiv(term_subst_t *subst, composite_term_t *d) {  in subst_bvsdiv()
870 static term_t subst_bvsrem(term_subst_t *subst, composite_term_t *d) {  in subst_bvsrem()
879 static term_t subst_bvsmod(term_subst_t *subst, composite_term_t *d) {  in subst_bvsmod()
888 static term_t subst_bvshl(term_subst_t *subst, composite_term_t *d) {  in subst_bvshl()
897 static term_t subst_bvlshr(term_subst_t *subst, composite_term_t *d) {  in subst_bvlshr()
906 static term_t subst_bvashr(term_subst_t *subst, composite_term_t *d) {  in subst_bvashr()
916 static term_t subst_bveq(term_subst_t *subst, composite_term_t *d) {  in subst_bveq()
925 static term_t subst_bvge(term_subst_t *subst, composite_term_t *d) {  in subst_bvge()
934 static term_t subst_bvsge(term_subst_t *subst, composite_term_t *d) {  in subst_bvsge()
951 static term_t subst_select(term_subst_t *subst, select_term_t *d) {  in subst_select()
960 static term_t subst_bit_select(term_subst_t *subst, select_term_t *d) {  in subst_bit_select()
973 static term_t subst_pprod(term_subst_t *subst, pprod_t *p, type_t tau) {  in subst_pprod()
1025 static term_t subst_poly(term_subst_t *subst, polynomial_t *p) {  in subst_poly()
1058 static term_t subst_bvpoly64(term_subst_t *subst, bvpoly64_t *p) {  in subst_bvpoly64()
1091 static term_t subst_bvpoly(term_subst_t *subst, bvpoly_t *p) {  in subst_bvpoly()
1128 static term_t subst_composite(term_subst_t *subst, term_t t) {  in subst_composite()
1318 static term_t get_subst(term_subst_t *subst, term_t t) {  in get_subst()
1375 term_t apply_term_subst(term_subst_t *subst, term_t t) {  in apply_term_subst()