Home
last modified time | relevance | path

Searched refs:poly_term_desc (Results 1 – 20 of 20) sorted by relevance

/dports/math/yices/yices-2.6.2/src/model/
H A Dpresburger.c740 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 Darith_projection.c1133 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 Dprojection.c358 proj_add_poly_vars(proj, poly_term_desc(terms, t)); in proj_add_arith_term()
H A Dliteral_collector.c1469 u = lit_collector_visit_poly(collect, t, poly_term_desc(terms, t)); in lit_collector_visit()
H A Dmodel_eval.c1391 v = eval_arith_poly(eval, poly_term_desc(terms, t)); in eval_term()
/dports/math/yices/yices-2.6.2/src/terms/
H A Dterm_explorer.c375 result = poly_term_desc(table, t)->nterms; in term_num_children()
537 p = poly_term_desc(table, t); in sum_term_component()
H A Dterm_utils.c825 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 Delim_subst.c165 return elim_subst_try_arith_elim(subst, poly_term_desc(subst->terms, t), check_cycles); in elim_subst_try_arith_eq0()
H A Dterm_manager.c1748 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 Dterms.h1408 static inline polynomial_t *poly_term_desc(const term_table_t *table, term_t t) { in poly_term_desc() function
H A Dfull_subst.c1320 s = full_subst_poly(subst, poly_term_desc(terms, t)); in full_subst_composite()
H A Dterm_substitution.c1288 result = subst_poly(subst, poly_term_desc(terms, t)); in subst_composite()
/dports/math/yices/yices-2.6.2/src/mcsat/nra/
H A Dnra_plugin_internal.c85 polynomial_t* polynomial = poly_term_desc(terms, t); in nra_plugin_get_term_variables()
H A Dlibpoly_utils.c166 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 Dcontext.c2130 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 Dsymmetry_breaking.c1307 push_poly_vars(queue, cache, poly_term_desc(terms, r)); in collect_constants()
H A Dcontext_simplifier.c2983 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 Def_analyze.c768 ef_analyze_poly(ef, poly_term_desc(terms, t)); in ef_get_vars()
/dports/math/yices/yices-2.6.2/src/mcsat/
H A Dpreprocessor.c816 polynomial_t* p = poly_term_desc(terms, current); in preprocessor_apply()
/dports/math/yices/yices-2.6.2/src/frontend/smt2/
H A Dsmt2_commands.c2748 result = poly_needs_egraph(seen, poly_term_desc(terms, t)); in needs_egraph()