Skip to content

Princess 2024-01-12

Latest
Compare
Choose a tag to compare
@pruemmer pruemmer released this 12 Jan 07:23
· 28 commits to master since this release

New release for the new year. There are various changes this time, including:

  • Support for the theory of finite fields. Currently restricted to fields with prime cardinality.

  • An option -mgcFormat to output most-general constraints in CNF or DNF.

  • A decision procedure for combinatorial array logic. Currently the procedure can only be used through the API.

  • An option -counterTimeout for setting hardware-independent timeouts, so that timeouts will occur in a fully deterministic and reproducable way. This is currently still experimental, the intention is that the timeouts will (on any machine) be roughly proportional to the actual runtime, but this is not always the case yet.