Snapshots of the Princess Sources

Stable snapshots

• 15/11/2021: The theory of Heap was extended and further improved; this release also has initial support for polymorphic ADTs.
• 10/05/2021: In this release, mainly the new ExtArray solver was improved and optimised; several bugfixes are included as well.
• 10/03/2021: After one year, finally a new stable version. The license of Princess has changed to BSD 3-clause. The formula data-structures (IFormula) have been changed to properly store the sort of quantified variables. There are a number of new theory solvers, development still ongoing: Rationals, which are used to handle SMT-LIB reals; ExtArray, a new solver for extensional arrays; Heap, a solver for the theory of heap we proposed at last year's HCVS and SMT workshops.
• 12/03/2020: Several optimisations in the linear integer solver, and various bugfixes. This source release compiles with Scala 2.11 and 2.12, to use Scala 2.13 you need to download a version from the scala-2.13 branch from above. Our Maven repository contains Scala 2.13 binaries as well. At the moment, however, Scala 2.11 is the fastest!
• 02/10/2019: Various bugfixes; support for uninterpreted sort with possibly finite cardinality; support for the right-shift operator in the bit-vector solver.
• 24/07/2019: More work on the bit-vector solver, in particular better support for extract, concat, and some of the bit-wise operations (thanks to Peter Backeman for most of this effort!)
• 26/10/2018: The biggest change is the addition of a theory of strings, following more or less the proposed SMT-LIB standard for Unicode strings. Princess comes with a very naive (and incomplete) built-in solver for this theory based on ADTs, but can also use OSTRICH as a library. OSTRICH is already included in the version running our web interface. Apart from this, there were various improvements, optimisations, and bug-fixes.
• 25/05/2018: Various further improvements in the bit-vector solver, including support for interpolation. Handling of shifts has been extended, but right-shifts are still not fully supported yet. bvand and bvor work if one of the operands is a concrete number.
• 27/01/2018: More work on the bit-vector solver, which should have become more complete and faster. Shifts and bit-wise operations are still not fully supported.
• 06/12/2017: This release includes the first version of a bit-vector solver, including procedures for bit-vector interpolation and bit-vector quantifier elimination. Bit-vector support is still work in progress, and currently most complete for linear arithmetic formulas; non-linear bit-vector formulas work partly, and bit-wise operations are not implemented yet.
• 17/07/2017: This version includes a larger set of updates. Most importantly, a new type system was added to the front-end layer, which means that types like bool, int[1, 9], int[-inf, 0], nat can now be used in all places where symbols are declared. The module for algebraic datatypes (ADTs) was completed, and now also supports Craig interpolation. Finally, the module for non-linear integer reasoning has been made proof-producing, and therefore also supports Craig interpolation (however, interpolants are not always quantifier-free).
• 26/12/2016: Initial support for algebraic datatypes (ADTs), see examples in testcases/api/ADTTest* and testcases/smtlib/datatype*. Various bugfixes.
• 01/07/2016: Support for pretty-printed proof output using the option +printProof, and initial support for learning lemmas (enabled whenever proofs are generated). Much better processing of SMT-LIB scripts, in particular when using the option +incremental for incremental processing. Various bugfixes.
• 07/12/2015: Various optimisations and bugfixes. The incremental SMT-LIB now also supports tree interpolation, again following the SMTInterpol proposal. The licence of Princess was relaxed, and is now "LGPL v2.1 or later" (before it was "LGPL v3").
• 11/03/2015: This version is a bigger update and contains major changes. The two most important new features are a new theory solver (developed by Peter Backeman) for non-linear integer arithmetic, and a complete rewrite of the incremental SMT-LIB parser that should make Princess significantly faster and more standard-compliant for processing SMT-LIB scripts. The incremental SMT-LIB parser now also supports specification of interpolant sequences in the same format as SMTInterpol (an example is shown by the GUI that can be started with ./princessGui). Many thanks go to Matthias Heizmann for various bug reports over the last months!
• 27/08/2014: A further version with many internal changes, and extensions in the API. The biggest visible changes are the switch from GPL to LGPL, to enable integration of Princess in other (non-GPL) systems, and the addition of a client-server mode. The latter mode avoids frequent restart of the JVM, and the resulting start-up delay. To use the client-server mode, one can simply call the script princessClient instead of princess; the first call will then start a daemon that takes care of all subsequent queries. This mode is currently only tested on Linux, and requires some more work for Macs or Windows.
• 10/02/2014: Mainly internal changes, and new functionality in the API. There is a new standardised interface for specifying new theories (e.g., arrays), which can be implemented either with the help of axioms, or directly in Scala. The interface is not used in all places yet, but will be in the future.
• 06/09/2013: Various optimisations, bugfixes, and improvements in the GUI (that can be started with ./princessGui). Most importantly, the status messages produced by Princess have been revised. Given a problem in the Princess input format, Princess now consistently prints VALID if the problem could be proven logically valid, and INVALID if the problem was found invalid (counter-satisfiable). The GUI now supports adjustment of font size (zooming in/out) via the key combination control + mouse wheel. The Princess input format has been slightly extended, and now uses flags \noMatch and \negMatch that control whether uninterpreted predicates in quantified formulae are matched positively, negatively, or not at all. An example is in testcases/onlyUnitResolution/negMatching.pri.
• 21/04/2013: Mainly internal changes and bugfixes. The biggest change affects compilation: this snapshot can (and has to) be compiled with Scala 2.10. Due to incompatibilities between Scala 2.9 and Scala 2.10, compilation with older versions of Scala is not possible anymore. The ap.SimpleAPI interface has become more mature and offers more functionality. E.g., now there is very rudimentary functionality for adding user-defined theory plugins via the API, as a way to efficiently define new theories (to be extended).
• 02/11/2012: Various changes and optimisations. The SMT-LIB 2 interface is now (at least partly) incremental, so it can process inputs with multiple check-sat commands, and handle push and pop to organisation the assertion stack; the provided answers should mostly follow the SMT-LIB 2 standard. Incremental problems are not yet handled very efficiently though. There is a new option +stdin to read SMT-LIB 2 inputs from stdin, and an option +quiet to reduce prover output to a minimum, namely the actual prover answers.
  There is also a new API class ap.SimpleAPI that simplifies the integration of Princess into Scala applications; an example for the use of this API is given in testcases/api/SimpleAPITest.scala. To use the API you will have to download the source distribution of Princess (not the binary distribution, which was compressed using ProGuard).
• 04/06/2012: A number of small improvements and bugfixes. Most importantly, interpolants and counterexamples are now pretty-printed (and can therefore be parsed, even if containing quantifiers), instead of just dumped in the internal format. Also the TPTP parser has been extended substantially, and now partly supports the rational and real datatype.
  Together with this version, we are also releasing a dedicated CASC version prepared for the CASC competition later in June. A pre-compiled binary (with assertions removed) can be downloaded here. The CASC edition is mostly equivalent to the standard Princess release, but also contains a number of modifications: (i) the default input format is chosen to be TPTP; (ii) by default, the prover runs with the option +multiStrategy, with a portfolio of strategies optimised for TPTP problems; (iii) the semantics of uninterpreted sorts is different from the semantics assumed by standard Princess: in the standard version, uninterpreted sorts are always considered to be infinite (since they are internally mapped to the datatype of integers), whereas in the CASC version type guards are generated to correctly model also finite domains; (iv) results are output in the SZS notation.
• 04/05/2012: Various optimisations and bugfixes, but also a number of new features: (i) Princess now contains a first version of a TPTP front-end, supporting the FOF and TFF dialects of TPTP (thanks to Peter Baumgartner for contributing the initial version of the TPTP parser!); (ii) it is possible to use general multiplication in problems (e.g., also multiplication between two variables), which is automatically encoded using an uninterpreted function symbol and axioms; (iii) new datatypes (actually short-hand notations) nat, as well as intervals have been introduced for quantifiers, the syntax is \forall nat x; ..., \forall int[0, 5] x; ..., \forall int[-inf, 5] x; ....
• 03/01/2012: A number of bugfixes, no bigger changes otherwise.
• 12/11/2011: Some small bugfixes and optimisations. Changed the portfolio mode (invoked using the option +multiStrategy).
• 02/10/2011: A number of further optimisations, otherwise the behaviour of Princess should not have changed.
• 10/09/2011: Various optimisations, in particular concerning the treatment of quantifiers and uninterpreted functions. I added an experimental portfolio-mode, in which different prove strategies are applied in parallel to prove a problem; this mode can be enabled using the option +multiStrategy. The SMT-LIB 2 parser now also supports arrays (as in, e.g., the SMT-LIB category AUFLIA).
  
• 15/07/2011: Improved the SMT-LIB 2 parser, which now also supports operations like ite, div, mod, etc. Functions and predicates with boolean arguments should also work. Correspondingly, there have been extensions in the .pri-parser, which now accepts conditional terms and formulae using the syntax \if (cond) \then (t1) \else (t2) (similar as in KeY). More generally, the .pri-format now also provides epsilon terms of the form  (\eps int x; phi(x)); such a term evaluates to an integer value x satisfying the predicate phi(x).
  Princess can and is now compiled using Scala 2.9. Unfortunately, the new Scala version seems to lead to a performance degradation of about 15-20%, I'm not quite sure yet what the reason is.
  
• 27/05/2011: Some bugfixes and a number of optimisations, in particular in the code handling functions and quantifiers. Princess now also has a basic built-in SMT-LIB 2 parser, primarily targetting the logics QF_LIA and AUFLIA. The parser does not yet support all features of the SMT-LIB language, in particular it is not supported to have formulae/Boolean expressions as arguments of functions or predicates, and the handling of user-specified triggers is a bit shaky. Also, the command script interface is not really interactive or incremental at the moment.
  
• 02/05/2011: Various improvements, optimisations, and bug-fixes, in particular concerning the generation of interpolants. Proofs are now simplified before interpolants are extracted, which can lead to significantly smaller interpolants and better performance. I also decided to switch off assertions by default, since benchmarking Princess with assertions switched on can lead to very misleading results. If Princess seems to do strange things, it can be a good idea to enable assertions using the commandline switch +assert.
• 10/11/2010: Fixed issues with Scala 2.8.1, which introduced a few API changed that prevented compilation of Princess (vice versa, this means that this snapshot of Princess probably cannot be compiled with Scala 2.8.0). The proof and interpolation packages have seen various changes since the last snapshot, but most of the modifications should not be visible for the user. One exception: Princess can now generate Graphviz diagrams to visualise proofs; this is enabled using the option -printDOT=<filename>.
• 31/08/2010: Princess can (and has to) be compiled with Scala 2.8 now. We backported the Craig interpolation functionality of iPrincess into Princess. The Swing GUI has been reworked and offers an MDI interface, as well as load and save functions. Of course, various bugfixes.
• 13/01/2010: Fixed a couple of bugs and added some optimisations
• 01/12/2009b: Eliminated some non-determinism that made the behaviour of Princess unpredictable (in a few cases)
  
• 01/12/2009: Bugfixes and internal changes, most of which are not really visible when using Princess (for the time being)
  
• 27/09/2009: Fixed a bug in the previous snapshot
• 23/09/2009: It is now possible to declare \universalConstants and \existentialConstants, which can both occur in constraints (the universal constants are implicitly quantified on the outermost level, the existential constants on the inner level). Such constraints behave a bit like unifiers in first-order theorem provers and can be used to formulate more flexible queries than before. I will add an example what this is good to this page in the near future. Besides, there are various internal changes that are mostly not (yet) visible when using Princess.
• 12/07/2009: Some small optimisations. Princess is now distributed under GPL v3.
  
• 10/06/2009: Optimised various things and changed some internals. Most of the changes are not visible when using Princess, but were necessary for Seneschal. Deciding formulae in Presburger arithmetic (i.e., formulae without uninterpreted predicates) has become a lot faster in some cases.
  
• 17/05/2009: The first new version of Princess in a while (the first post-PhD version so to speak). Most importantly, the code for instantiating quantified formulae using unit resolution has been rewritten, so that instantiation should be both more efficient and more fair. Several bugs have been fixed, and some rules have been optimised (in particular the Omega rule for splitting inequalities).
  Princess also got a couple of new options:
• It is now possible to derive the most general constraint for a given problem (using +mostGeneralConstraint). This implements quantifier elimination for Presburger formulae, but can also meaningful for other formulae if the termination of constructing the proof tree is ensured.
• Using -dnfConstraints, the conversion of constraints to DNF during proof construction is less aggressive, which can be more efficient in some cases.
• With -printSMT=<filename>, Princess can be told to save a de-sugared version of the input problem in the SMT-Lib format.
  
• 02/12/2008: Fixed a severe bug in the function encoder.
  After learning about a more efficient approach to quantifier elimination at LPAR, I implemented a similar procedure in Princess that can now be switched on with the option -simplifyConstraints=lemmas. I'm still experimenting with different ways to integrate the ideas from the paper, but already now the procedure gives better performance and yields smaller constraints for some examples.
  The option +posUnitResolution is now the default, because when using functions it is usually the preferable setting.
  
• 24/11/2008: The frontend of Princess has been rewritten, which allows for a somewhat nicer syntax (it is no longer necessary to write p() for nullary predicates p, the parentheses can be left out). There is now also a clausifier that can be switched on using a commandline option and that can improve the performance of unit-resolution considerably. Finally and most importantly, the frontend also supports function symbols (both partial and total) that are encoded as relations: phi[f(x)] is turned into \forall int y; f(x,y) -> phi[y] or \exists int y; f(x,y) & phi[y]. The choice which translation is used can be influenced by addings (SMT-like) triggers to quantified formulae, which works quite well together with unit-resolution.
• 18/9/2008: The first version of Princess that implements the free-constant optimisation (Sect. 8 in the techreport), which primarily speeds up reasoning about ground problems and about problems that contain many existential quantifiers in positive positions. The optimisation is also an important step to make the unit-resolution mode (+posUnitResolution) and encodings of functions as predicates practical. Of course, the new Princess version also contains many bugfixes.
• 25/7/2008: Further bugfixes and optimisations, no bigger changes.
• 19/7/2008: A number of bugfixes and optimisations. Most importantly, Princess now selects propositional variables/predicates to split over based on the frequency of occurrence.
• 15/7/2008: The version for July, again with a large number of small bugfixes and some new features. The splitting behaviour of Princess has been refined to avoid splitting Presburger formulae if possible, which means that existential quantifiers (in positive positions) can be handled more efficiently. I also added a commandline switch to turn unit resolution on and off.
• 8/6/2008: June version with many bugfixes and a few new features. The fact/unit propagation into formulas has become more general, clauses are handled more efficiently by unit resolution with positive ground literals (pretty experimental and to be improved). There is now also a simple GUI and Webstart so that Princess can be tested without installing it.
• 6/5/2008: After a long while finally a new version with lots of new features: Princess now supports both inequalities and uninterpreted predicates and thus the whole logic as it is described in the technical report above. There are still many things left to optimise, in particular the predicate handling is currently done in the most naive way possible.
• 27/3/2008: Many bugfixes and improvements everywhere ... there are now some command line parameters (get a list with princess -h), a first version of fact propagation into formulas has been added, constraint propagation/simplification along proof trees has been optimised. One of the next steps will be to add inequalities.
• 17/3/2008: Fixed a bug in the Makefile, added C-style comments to the parser.
• 15/3/2008: Princess now has a parser, and some examples are included. Inequalities and uninterpreted predicates are still not implemented, but stay tuned.
• 5/3/2008: Not really usable for anything yet, apart from running the unit tests

Stable snapshots of the CASC/TPTP version

• 17/07/2017: The version for CASC-26 in 2017, Gothenburg, Sweden. The main change compared to 2016 is proof production for problems involving non-linear integer arithmetic (by introducing appropriate theory lemmas in the proof).
• 06/06/2016: The version for CASC-J8 in 2016, Coimbra, Portugal. Princess is now able to produce proofs/solutions, although not for all problems (some modules are not yet proof-producing). Proof output can be enabled with the option +printProof. Princess has also become a bit more clever with learning lemmas.
• 06/07/2015: The version for CASC-25 in 2015, Berlin; compared to the version for 2014, mainly bugfixes were done.
• 04/07/2014: The version for CASC-J7 in 2014, Vienna. This version has seen various changes and bugfixes. For users, one important new feature is a daemon mode, which can be used to avoid delays due to the JVM start-up time. For the daemon mode it is enough to run the script princess-casc-client, which should behave just like the normal start script princess-casc. Also a new binary is available.
• 14/06/2013: update to get the TPTP version in sync with the main branch. Also a new binary is provided.
• 04/06/2012 prepared for the CASC competition in June 2012. A pre-compiled binary (with assertions removed) can be downloaded here. The CASC edition is mostly equivalent to the standard Princess release, but also contains a number of modifications: (i) the default input format is chosen to be TPTP; (ii) by default, the prover runs with the option +multiStrategy, with a portfolio of strategies optimised for TPTP problems; (iii) the semantics of uninterpreted sorts is different from the semantics assumed by standard Princess: in the standard version, uninterpreted sorts are always considered to be infinite (since they are internally mapped to the datatype of integers), whereas in the CASC version type guards are generated to correctly model also finite domains; (iv) results are output in the SZS notation.