Princess 2024-01-12

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.

Princess 2023-06-19

Mainly bugfixes, and some extensions and improvements in the string solver.

Princess 2023-04-07

Many internal modifications, and a few changes that are externally visible. The string solver was extended a lot, and will be extended even more in the near future. First steps were done to add a sequence solver, and support for lambda-expressions for defining arrays was added. The notation (_ is ctor) for ADTs is now supported.

Princess 2022-11-03

This version adds options -logging for outputting more debugging information; option +equivInlining for simplifying equivalence expressions (on by default); option -timeoutSec for specifying timeouts in seconds; and option -threads for specifying use of multiple cores, in combination of the option -portfolio. The version will also use SZS notation for printing the status of TPTP problems.

Princess 2022-07-01

The first proper release after a long time, and the first release on github. Changes since the last release include mainly bugfixes, and some additional API functions.