| /dports/math/yices/yices-2.6.2/src/terms/ |
| H A D | rba_buffer_terms.c | 39 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in rba_buffer_add_term()
76 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in rba_buffer_sub_term()
113 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in rba_buffer_mul_term()
151 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in rba_buffer_add_const_times_term()
196 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in rba_buffer_mul_term_power()
|
| H A D | arith_buffer_terms.c | 39 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in arith_buffer_add_term()
76 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in arith_buffer_sub_term()
113 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in arith_buffer_mul_term()
151 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in arith_buffer_add_const_times_term()
196 assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); in arith_buffer_mul_term_power()
|
| H A D | bvarith64_buffer_terms.c | 75 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); in bvarith64_buffer_set_term()
96 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith64_buffer_add_term()
150 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith64_buffer_sub_term()
204 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith64_buffer_mul_term()
254 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith64_buffer_add_const_times_term()
310 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith64_buffer_mul_term_power()
|
| H A D | bit_term_conversion.c | 63 x = node_table_alloc_var(nodes, pos_term(i)); in convert_term_to_bit()
74 x = node_table_alloc_var(nodes, pos_term(i)); in convert_term_to_bit()
79 x = node_table_alloc_var(nodes, pos_term(i)); in convert_term_to_bit()
91 assert((bit_is_pos(x) && map_of_node(nodes, node_of_bit(x)) == pos_term(i)) || in convert_term_to_bit()
|
| H A D | bvarith_buffer_terms.c | 76 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); in bvarith_buffer_set_term()
98 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith_buffer_add_term()
152 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith_buffer_sub_term()
206 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith_buffer_mul_term()
258 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith_buffer_add_const_times_term()
321 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvarith_buffer_mul_term_power()
|
| H A D | terms.c | 2053 return pos_term(i); in constant_term()
2069 return pos_term(i); in new_uninterpreted_term()
2085 return pos_term(i); in new_variable()
2156 return pos_term(i); in ite_term()
2181 return pos_term(i); in app_term()
2209 return pos_term(i); in update_term()
2231 return pos_term(i); in tuple_term()
2256 return pos_term(i); in select_term()
2282 return pos_term(i); in binary_term()
2303 return pos_term(i); in unary_term()
[all …]
|
| H A D | bvlogic_buffers.c | 1862 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); in bvlogic_buffer_set_term()
1910 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && i <= j); in bvlogic_buffer_set_slice_term()
1964 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvlogic_buffer_and_term()
2011 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvlogic_buffer_or_term()
2058 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvlogic_buffer_xor_term()
2108 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && in bvlogic_buffer_comp_term()
2159 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); in bvlogic_buffer_concat_left_term()
2204 assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); in bvlogic_buffer_concat_right_term()
|
| H A D | free_var_collector.c | 300 result = singleton_fvar_set(collect, pos_term(i)); in get_free_vars_of_term()
|
| H A D | full_subst.c | 279 s = full_subst_get_map(subst, pos_term(i)); in fsubst_explore()
284 full_subst_remove_map(subst, pos_term(i)); in fsubst_explore()
|
| H A D | terms.h | 947 static inline term_t pos_term(int32_t i) { in pos_term() function
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | internalization_printer.c | 136 t = pos_term(i); in print_intern_substitution()
164 r = pos_term(i); in print_intern_mapping()
192 t = pos_term(i); in print_intern_substitution2()
|
| H A D | shared_terms.c | 72 root = intern_tbl_get_root(map->intern, pos_term(i)); in sharing_map_process_occurrence()
340 parent = pos_term(r->val); in unique_parent()
|
| H A D | context_printer.c | 215 t = pos_term(i); in pp_intern_substitutions()
|
| H A D | internalization_table.c | 438 i = index_of(intern_tbl_get_root(tbl, pos_term(i)));
|
| H A D | context_simplifier.c | 1552 r = subst_candidate(ctx, pos_term(i)); in visit()
1558 remove_subst_candidate(ctx, pos_term(i)); in visit()
3178 r = intern_tbl_get_root(&ctx->intern, pos_term(idx)); in analyze_dl()
3179 if (r != pos_term(idx)) { in analyze_dl()
|
| /dports/math/yices/yices-2.6.2/src/solvers/bv/ |
| H A D | dimacs_printer.c | 414 t = pos_term(i); in print_dimacs_header()
|
| /dports/math/yices/yices-2.6.2/src/io/ |
| H A D | term_printer.c | 870 name = term_name(tbl, pos_term(i)); in print_term_idx_recur()
1193 name = term_name(tbl, pos_term(i)); in max_term_name_length()
1504 print_padded_string(f, term_name(tbl, pos_term(i)), name_size); in print_term_table()
1654 print_term_name(f, tbl, pos_term(i)); in print_term_idx_desc()
2465 name = term_name(tbl, pos_term(i)); in pp_term_idx_name()
2783 t = pos_term(i); in pp_term_table()
|
| /dports/math/py-or-tools/or-tools-9.2/ortools/constraint_solver/ |
| H A D | expr_array.cc | 2808 IntExpr* pos_term = nullptr; in MakeScalProdEqualityFct() local
2814 pos_term = solver->MakeProd(vars[i], coefs[i]); in MakeScalProdEqualityFct()
2819 return solver->MakeEquality(pos_term, rhs); in MakeScalProdEqualityFct()
2993 IntExpr* const pos_term = solver->MakeSum(pos_terms[0], -rhs); in MakeScalProdLessOrEqualFct() local
2994 return solver->MakeGreaterOrEqual(solver->MakeSum(neg_terms), pos_term); in MakeScalProdLessOrEqualFct()
3003 IntExpr* pos_term = nullptr; in MakeScalProdLessOrEqualFct() local
3009 pos_term = solver->MakeProd(vars[i], coefs[i]); in MakeScalProdLessOrEqualFct()
3014 return solver->MakeLessOrEqual(pos_term, rhs); in MakeScalProdLessOrEqualFct()
|
| /dports/math/yices/yices-2.6.2/src/model/ |
| H A D | model_support.c | 349 result = singleton_support(constructor, pos_term(i)); in get_term_support()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_intern_table.c | 1288 t = pos_term(i); in show_subst()
1318 r = pos_term(i); in show_mapping()
|
| /dports/net/yaz/yaz-5.31.1/client/ |
| H A D | client.c | 3483 Odr_int pos_term = res->positionOfTerm ? *res->positionOfTerm : -1; in process_Z3950_scanResponse() local
3486 printf("%c ", i + 1 == pos_term ? '*' : ' '); in process_Z3950_scanResponse()
|