SRI-CSL / yices2 / 22886107522

71%

push

github

Finite Field API extension (#605)

* FF type + term constructors
    Added yices_ff_type(mpz_t order) with prime-order validation (INVALID_FFSIZE on non-prime).
    Added FF term constructors:
    yices_ff_const
    yices_ff_add, yices_ff_sub, yices_ff_neg
    yices_ff_mul, yices_ff_square, yices_ff_power
    yices_ff_sum, yices_ff_product
    Added FF atoms:
    yices_ff_eq_atom, yices_ff_neq_atom
    yices_ff_eq0_atom, yices_ff_neq0_atom
* FF deconstruction APIs
    Added yices_ff_const_value(term_t t, mpz_t z).
    Split sum deconstruction by theory:
    yices_sum_component(..., mpq_t coeff, ...) is now arithmetic-only.
    Added yices_ffsum_component(..., mpz_t coeff, ...) for FF sums.
* Model extension + value extraction
    Added model assignment API:
    yices_model_set_ff_mpz(model_t *model, term_t var, mpz_t val)
    Added model value extraction APIs:
    yices_get_ff_value(model_t *mdl, term_t t, mpz_t val, mpz_t mod)
    yices_val_get_ff(model_t *mdl, const yval_t *v, mpz_t val, mpz_t mod)
* Constructor naming cleanup
    Simplified public term-constructor names:
    YICES_FF_CONSTANT (canonical)
    YICES_FF_SUM (canonical)
    Kept compatibility aliases in yices_types.h:
    YICES_ARITH_FF_CONSTANT = YICES_FF_CONSTANT
    YICES_ARITH_FF_SUM = YICES_FF_SUM
* Internal/public declarations and docs
    Added matching lock-free o declarations for all new APIs.
    Updated API docs/comments in headers and Sphinx:
    new FF functions
    constructor/tag docs for YICES_FF_CONSTANT, YICES_FF_SUM
    model DAG docs include YVAL_FINITEFIELD
    Removed stale TODO note for YVAL_FINITEFIELD.
* Tests
    Added API test: tests/api/test_ff_api.c
    Covers all newly added FF API entry points, including:
    constructors/atoms
    FF const/sum deconstruction
    model assignment and value extraction

191 of 236 new or added lines in 2 files covered. (80.93%)

83195 of 125032 relevant lines covered (66.54%)

1703879.96 hits per line