/dports/math/yices/yices-2.6.2/src/model/ |
H A D | presburger.c | 740 poly_buffer_add_poly(buffer, poly_term_desc(terms, t1)); in presburger_add_arith_bineq() 754 poly_buffer_sub_poly(buffer, poly_term_desc(terms, t2)); in presburger_add_arith_bineq() 789 poly_buffer_add_poly(buffer, poly_term_desc(terms, u)); in presburger_add_arith_divides() 850 presburger_add_poly_eq_zero(pres, poly_term_desc(terms, t)); in presburger_add_constraint() 870 presburger_add_poly_geq_zero(pres, poly_term_desc(terms, t)); in presburger_add_constraint() 877 presburger_add_poly_lt_zero(pres, poly_term_desc(terms, t)); in presburger_add_constraint()
|
H A D | arith_projection.c | 1133 aproj_buffer_add_poly(buffer, &proj->vtbl, poly_term_desc(terms, t1)); in aproj_add_arith_bineq() 1147 aproj_buffer_sub_poly(buffer, &proj->vtbl, poly_term_desc(terms, t2)); in aproj_add_arith_bineq() 1207 aproj_add_poly_eq_zero(proj, poly_term_desc(terms, t)); in aproj_add_constraint() 1227 aproj_add_poly_geq_zero(proj, poly_term_desc(terms, t)); in aproj_add_constraint() 1234 aproj_add_poly_lt_zero(proj, poly_term_desc(terms, t)); in aproj_add_constraint()
|
H A D | projection.c | 358 proj_add_poly_vars(proj, poly_term_desc(terms, t)); in proj_add_arith_term()
|
H A D | literal_collector.c | 1469 u = lit_collector_visit_poly(collect, t, poly_term_desc(terms, t)); in lit_collector_visit()
|
H A D | model_eval.c | 1391 v = eval_arith_poly(eval, poly_term_desc(terms, t)); in eval_term()
|
/dports/math/yices/yices-2.6.2/src/terms/ |
H A D | term_explorer.c | 375 result = poly_term_desc(table, t)->nterms; in term_num_children() 537 p = poly_term_desc(table, t); in sum_term_component()
|
H A D | term_utils.c | 825 return non_integer_polynomial(tbl, poly_term_desc(tbl, t)); in arith_term_is_not_integer() 912 return disequal_polynomials(poly_term_desc(tbl, x), poly_term_desc(tbl, y)); in disequal_arith_terms() 916 return polynomial_is_const_plus_var(poly_term_desc(tbl, x), y); in disequal_arith_terms() 920 return polynomial_is_const_plus_var(poly_term_desc(tbl, y), x); in disequal_arith_terms() 1196 return polynomial_is_nonneg(poly_term_desc(tbl, t)); in arith_term_is_nonneg() 1232 return polynomial_is_nonpos(poly_term_desc(tbl, t)); in arith_term_is_nonpos() 1264 return polynomial_is_neg(poly_term_desc(tbl, t)); in arith_term_is_negative() 1288 return polynomial_is_nonzero(poly_term_desc(tbl, t)); in arith_term_is_nonzero() 3831 arith_cnstr_set_poly(cnstr, poly_term_desc(tbl, t)); in store_arith_eq() 3845 arith_cnstr_set_poly(cnstr, poly_term_desc(tbl, t)); in store_arith_geq() [all …]
|
H A D | elim_subst.c | 165 return elim_subst_try_arith_elim(subst, poly_term_desc(subst->terms, t), check_cycles); in elim_subst_try_arith_eq0()
|
H A D | term_manager.c | 1748 p = poly_term_desc(tbl, t); // then part in mk_integer_polynomial_ite() 1749 q = poly_term_desc(tbl, e); // else part in mk_integer_polynomial_ite() 1838 p = poly_term_desc(tbl, t); in try_offset_ite() 1850 p = poly_term_desc(tbl, e); in try_offset_ite() 2841 p_poly = poly_term_desc(terms, p); in mk_arith_root_atom_aux()
|
H A D | terms.h | 1408 static inline polynomial_t *poly_term_desc(const term_table_t *table, term_t t) { in poly_term_desc() function
|
H A D | full_subst.c | 1320 s = full_subst_poly(subst, poly_term_desc(terms, t)); in full_subst_composite()
|
H A D | term_substitution.c | 1288 result = subst_poly(subst, poly_term_desc(terms, t)); in subst_composite()
|
/dports/math/yices/yices-2.6.2/src/mcsat/nra/ |
H A D | nra_plugin_internal.c | 85 polynomial_t* polynomial = poly_term_desc(terms, t); in nra_plugin_get_term_variables()
|
H A D | libpoly_utils.c | 166 result = lp_polynomial_from_polynomial(nra, poly_term_desc(terms, t), c); in lp_polynomial_from_term()
|
/dports/math/yices/yices-2.6.2/src/context/ |
H A D | context.c | 2130 l = map_poly_ge_to_literal(ctx, poly_term_desc(terms, t)); in map_arith_geq_to_literal() 2288 l = map_poly_eq_to_literal(ctx, poly_term_desc(terms, t)); in map_arith_eq_to_literal() 2680 x = map_poly_to_arith(ctx, poly_term_desc(terms, r)); in internalize_to_eterm() 2854 x = map_poly_to_arith(ctx, poly_term_desc(terms, r)); in internalize_to_arith() 4005 p = poly_term_desc(terms, t); in assert_toplevel_arith_eq() 4014 assert_toplevel_poly_eq(ctx, poly_term_desc(terms, t), tt); in assert_toplevel_arith_eq() 4070 assert_toplevel_poly_geq(ctx, poly_term_desc(terms, t), tt); in assert_toplevel_arith_geq()
|
H A D | symmetry_breaking.c | 1307 push_poly_vars(queue, cache, poly_term_desc(terms, r)); in collect_constants()
|
H A D | context_simplifier.c | 2983 return dl_convert_poly(ctx, triple, poly_term_desc(terms, t)); in dl_convert_term()
|
/dports/math/yices/yices-2.6.2/src/exists_forall/ |
H A D | ef_analyze.c | 768 ef_analyze_poly(ef, poly_term_desc(terms, t)); in ef_get_vars()
|
/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | preprocessor.c | 816 polynomial_t* p = poly_term_desc(terms, current); in preprocessor_apply()
|
/dports/math/yices/yices-2.6.2/src/frontend/smt2/ |
H A D | smt2_commands.c | 2748 result = poly_needs_egraph(seen, poly_term_desc(terms, t)); in needs_egraph()
|