Conversation
Collaborator
Author
|
Added a bug fix in src/model/concrete_values.c
|
ahmed-irfan
approved these changes
Mar 3, 2026
Ovascos
approved these changes
Mar 9, 2026
| ==================================== =========================== | ||
| :c:enum:`YICES_BOOL_CONSTANT` Boolean constant | ||
| :c:enum:`YICES_ARITH_CONSTANT` Arithmetic constant | ||
| :c:enum:`YICES_FF_CONSTANT` Finite-field constant |
| Constructor Term | ||
| ================================ =========================== | ||
| :c:enum:`YICES_ARITH_SUM` Arithmetic sum | ||
| :c:enum:`YICES_FF_SUM` Finite-field sum |
src/include/yices.h
Outdated
| * | ||
| * YICES_BOOL_CONSTANT boolean constant | ||
| * YICES_ARITH_CONSTANT rational constant | ||
| * YICES_FF_CONSTANT finite-field constant |
src/include/yices.h
Outdated
| * | ||
| * YICES_BV_SUM sum of pairs a * t where a is a bitvector constant (and t is a bitvector term) | ||
| * YICES_ARITH_SUM sum of pairs a * t where a is a rational (and t is an arithmetic term) | ||
| * YICES_FF_SUM sum of pairs a * t where a is a finite-field constant (and t is a finite-field term) |
src/terms/term_explorer.c
Outdated
| YICES_SCALAR_CONSTANT, // CONSTANT_TERM | ||
| YICES_ARITH_CONSTANT, // ARITH_CONSTANT | ||
| YICES_ARITH_FF_CONSTANT, // ARITH_FF_CONSTANT | ||
| YICES_FF_CONSTANT, // ARITH_FF_CONSTANT |
src/terms/term_explorer.c
Outdated
| YICES_POWER_PRODUCT, // POWER_PRODUCT | ||
| YICES_ARITH_SUM, // ARITH_POLY | ||
| YICES_ARITH_FF_SUM, // ARITH_FF_POLY | ||
| YICES_FF_SUM, // ARITH_FF_POLY |
daniel-raffler
added a commit
to daniel-raffler/yices2_java_bindings
that referenced
this pull request
Mar 15, 2026
We're not adding the entire ff API, but just the new constructors. This was necessary as the new constructors changed the values of existing constructors Adding the rest of the API will have to be done in a separate commit See SRI-CSL/yices2#605
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR extends the C API with finite-field (ff) term construction/deconstruction/model operations, aligns constructor naming, updates Sphinx docs, and adds API test coverage.
What’s Added
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
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.
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)
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
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.
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
Adjusted to pass both release and debug API test runs.
Validation
make check-api (release): PASS
make YICES_MODE=debug check-api: PASS