Searched refs:top_interns (Results 1 – 7 of 7) sorted by relevance
155 ctx->top_formulas.size == 0 && ctx->top_interns.size == 0; in context_is_empty()
244 ctx->top_formulas.size == 0 && ctx->top_interns.size == 0; in context_is_empty()
398 ctx->top_formulas.size == 0 && ctx->top_interns.size == 0; in context_is_empty()
136 print_term_vector(f, ctx->terms, "intern", &ctx->top_interns); in print_context_top_interns()
674 ivector_t top_interns; member
5502 init_ivector(&ctx->top_interns, CTX_DEFAULT_VECTOR_SIZE); in init_context()5607 delete_ivector(&ctx->top_interns); in delete_context()5658 ivector_reset(&ctx->top_interns); in reset_context()5799 ivector_reset(&ctx->top_interns); in _o_context_process_assertions()5926 v = &ctx->top_interns; in _o_context_process_assertions()6089 ivector_reset(&ctx->top_interns); in context_internalize()6165 ivector_reset(&ctx->top_interns); in context_process_formulas()6447 ivector_reset(&ctx->top_interns); in context_gc_mark()
2171 ivector_push(&ctx->top_interns, signed_term(r, tt)); in flatten_assertion()2385 ivector_push(&ctx->top_interns, eq); in process_aux_eq()