search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
360 stars 45 forks source link

Finite Field support #513

Closed Ovascos closed 6 days ago

Ovascos commented 1 month ago

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.

coveralls commented 1 month ago

Coverage Status

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

Ovascos commented 1 week ago

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