Princess is a theorem prover for Presburger arithmetic with
uninterpreted predicates. This means that Princess can reason about
problems in integer arithmetic without multiplication (only
multiplication with integer literals is allowed), augmented with
predicates that can be axiomatised arbitrarily. Such problems can
contain arbitrary quantifiers to express that some formula is supposed
to hold for all or for some integers. Features of Princess
include:

- Decision + quantifier elimination procedure for Presburger arithmetic
- Support for uninterpreted predicates and partial or total functions
- Theory modules for non-linear integer arithmetic (diophantine) and the theory of arrays
- Support for Craig interpolation
- Free variable calculus, to handle quantifiers and extract solutions of formulae
- Triggers and e-matching for user-guided handling of quantified formulae, similar as in SMT solvers
- Problem input in the native language of Princess, in the SMT-LIB 2 format, and in the FOF/TFF/CNF dialects of TPTP (see details).
- Written in Scala, and runs on any platform that provides a Java runtime environment (version 1.5 or higher)
- Convenient API for programmatic use from Scala applications. This API can only be used to integrate Princess in Java applications, although this is somewhat less convenient (for instance see the wrapper used in Bixie)

Princess won the TFA division (arithmetic problems) at CASC J6, 2012. In 2013 and 2014, Princess won in the TFI category of CASC, (integer problems), and was runner-up in the overall TFA division.

Princess is free software. Since version 2015-12-07, Princess is distributed under LGPL v2.1 or later; older versions were licenced under LGPL v3, and even earlier under GPL v3. The latest release is 2015-12-07.

Please contact me if you are interested in any projects or thesis work related to Princess.

- Manual of Princess, although rather incomplete at the moment. Examples are included in the Princess distributions, and on the examples page.
- Definition of the Princess syntax.
- Princess API. If you want to use
the Princess API, it is
easiest to start from the class
ap.SimpleAPI,
and
use
the
functions
in
ap.parser.IExpression
to construct formulae. A number of examples are included in both the
source and binary distributions, in directory
`testcases/api`

.

- LPAR paper about the calculus that is used in Princess
- A more detailed description of the calculus and Princess is part of my PhD thesis
- IJCAR paper on interpolant generation in Presburger arithmetic
- VERIFY and VMCAI papers on interpolant generation in the presence of uninterpreted predicates, functions, and arrays
- LPAR paper about e-matching and the handling of functions in Princess
- The native input format of Princess much resembles the format that is used by the KeY tool. You can have a look at the example files that are included in the distributions below.

- Seneschal, a ranking function generator for bitvector relations
- Eldarica, a predicate abstraction-based model checker
- Joogie, Gravy, and Bixie, tools for detecting inconsistent and infeasible code in Java applications
- Picasso, a static analyzer for depth-bounded systems

We provide a binary distribution of the latest version of Princess. This distribution contains all required libraries, i.e., the Scala API and the Cup parser generator library; it is only necessary to have a Java runtime environment (version 1.5 or newer) installed.

To install, just
download the archive and unpack it in some directory of your choice.
The Princess gui can then be invoked using the script `princessGui`

,
the
command
line
tool
using
the
script
`princess`

. In addition, the script `princessClient`

can be used to run Princess in client-server mode
(more details).

We currently maintain a separate branch for full support of the TPTP format. You can download a binary of the latest version, or the sources. This version differs from normal Princess mainly in the following points:

- the default input format is chosen to be TPTP;
- by default, the prover runs with the option
`+multiStrategy`

, with a portfolio of strategies optimised for TPTP problems; - 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;
- results are output in the SZS notation.

- ePrincess,
a variant of Princess that uses Bounded Rigid
*E*-Unification for closing branches. - iPrincess (now defunct), which added support for Craig interpolation to Princess. This functionality is now integrated in the main Princess branch.

The compilation is so far only tested on Linux systems. For the installation, you need:

- A compiler for Scala version 2.10 (at the moment, Scala 2.11 is not supported yet)
- A Java SDK version 1.5 or newer
- The Cup parser
generator for Java (get the file
`java-cup-11a.jar`

) - If you want to compile the parser yourself (binaries are included in the Princess snapshots below), you also need the BNF converter and JLex.

The actual installation consists of the following steps:

- Unpack one of the snapshots
(preferably the newest one) and
change to the
`princess-*`

directory - Create a directory
`extlibs`

and copy the file`java-cup-11a.jar`

into it - In case you want to compile the parser yourself (not necessary),
run
`make parser-jar`

- Run
`make`

to compile Princess.

If everything went ok, it is possible to run Princess with the
command `./princess <inputfile>`

A list of the Princess options can be printed using `./princess -h`