Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Finite Field support #513

Merged
merged 162 commits into from
Jul 3, 2024
Merged

Finite Field support #513

merged 162 commits into from
Jul 3, 2024

Conversation

Ovascos
Copy link
Contributor

@Ovascos Ovascos commented May 24, 2024

This PR adds the theory of finite field arithmetic (QF_FFA) to Yices. The theory is solved using mcsat, however, many auxiliary parts (SMT-LIB 2 parsing, terms, types, etc.) needed to modified.
Further, it contains some code cleanup in the NRA mcsat plugin.

Thomas Hader added 30 commits November 20, 2023 12:49
Symbols created, eval_ff_* to be done
8c41f5f
Added ff_plugin stub
d8aab36
Registered ff plugin to mcsat
383e87d
Added further type support for FF type
d8eea38
Added printing support for the ff type
b257789
fixed warning
c1cb009
actual missing error strings
aed17f3
Parsing of (as (_ ff3 13) FF0) done
17b8ef6
reformat indentions
aecf376
reformat indentions
3a4932d
Front-end parsing done
283aa8b
mod_rba_buffer_t and TAG_ARITH_FF_BUFFER
2035c47
Code Formatting
a10d403
Finite Field term generation done
7a4ef2d
Fixed print_elem in term_stack2.c
cf60337
Code Formatting
65a9c3a
Removed unnecessary todos
211d1f1
Support arbitrary finite field size
9a03d90
Some optimization for ff eq term generation
36e83f9
Code Formatting and Warning fixes
ba8887f
Added exceptions when ff is solved with non-mcsat context.
ae3399b
fixed model_eval to handle finite field terms (and return unknown).
46d8907
Term manager update (added further ff code to term_manager)
b4387c8
Added FF support to MCSAT preprocessor
085b9be
Added FF support to model printing
816b525
fix
e849bd2
Fixed printing and added value_ff_t.
92f8e37
WIP: ff_plugin_new_term_notify
088783e
Code Formatting fixes
35afa14
extracted lp_data handling from NRA plugin
c93e4bd
@coveralls
Copy link

coveralls commented May 24, 2024 •
edited
Loading

Coverage Status

coverage: 65.927% (+0.2%) from 65.726%
when pulling c7ddc21 on Ovascos:ffsat
into edc0d01 on SRI-CSL:master.

ahmed-irfan
ahmed-irfan reviewed Jun 25, 2024
View reviewed changes
Copy link
Member

@ahmed-irfan ahmed-irfan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review so far...

src/context/shared_terms.c Show resolved Hide resolved
src/frontend/yices/yices_parser.c Show resolved Hide resolved
src/include/yices_types.h Outdated Show resolved Hide resolved
src/mcsat/value.h Show resolved Hide resolved
src/model/model_eval.c Outdated Show resolved Hide resolved
src/solvers/simplex/diophantine_systems.c Show resolved Hide resolved
src/terms/polynomials.h Outdated Show resolved Hide resolved
ahmed-irfan
ahmed-irfan reviewed Jul 1, 2024
View reviewed changes
Copy link
Member

@ahmed-irfan ahmed-irfan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rest of the review.

Can you also add a test case in which the finite field is not a prime number? Yices should report an error, right?

src/frontend/smt2/smt2_lexer.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_feasible_set_db.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_plugin.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_plugin_explain.c Show resolved Hide resolved
src/mcsat/ff/ff_plugin_explain.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_plugin_explain.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_plugin_explain.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_plugin_explain.c Outdated Show resolved Hide resolved
src/mcsat/ff/ff_plugin_explain.c Show resolved Hide resolved
src/mcsat/utils/value_version_set.c Outdated Show resolved Hide resolved
@Ovascos
Copy link
Contributor Author

Ovascos commented Jul 2, 2024 •
edited
Loading

All comments have be taken care of. Also, fixed some todos in the finite field printer.

ahmed-irfan
ahmed-irfan approved these changes Jul 3, 2024
View reviewed changes
Copy link
Member

@ahmed-irfan ahmed-irfan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

Two things to be done in future PRs:

  • Extend Yices API
  • Update Yices documentation

@ahmed-irfan ahmed-irfan merged commit 06903da into SRI-CSL:master Jul 3, 2024
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ahmed-irfan ahmed-irfan ahmed-irfan approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Ovascos @coveralls @ahmed-irfan