Tacking Issue: Proposal: A Standard for the Theory of Finite Fields

[alex-ozdemir]

Discussed in #29

^{Originally posted by alex-ozdemir September 24, 2024}
Hi SMT community,

Thomas Hader and I have been developing SMT solvers that support a theory of finite fields. We've been ensuring compatibility between our solvers by agreeing upon a bespoke SMT-LIB interface for this theory. We think it is time to standardize that interface.

Below, we have attached a PDF with our proposal. We have presented our proposal at the SMT workshop and shared it with the SMT-LIB coordinators. Now, we are seeking broader community feedback.

If this theory interests you, please consider our proposal and let us know what you think. Comments and questions are both welcome. We encourage you to reply with your comments before October 31st.

Cheers,
Alex Ozdemir

Changes since the SMT workshop presentation.

• We have removed the `#f` shorthand notation for literals, because it served the same purpose as the indexed literal notation.

smtlib-ff-proposal.pdf