Snapshots of the Princess Sources
The latest releases are available on the Github page.
Nightly builds are available from our
Maven repository.
In addition to the normal version of Princess, we
also maintain a branch specific for solving
TPTP problems.
Older 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 3clause. The formula datastructures (
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 SMTLIB 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 scala2.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 rightshift operator in the bitvector solver.
 24/07/2019:
More work on the bitvector solver, in particular better support
for extract, concat, and some of the bitwise 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
SMTLIB standard for Unicode strings. Princess comes with a very naive
(and incomplete) builtin 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 bugfixes.
 25/05/2018:
Various further improvements in the bitvector solver, including
support for interpolation. Handling of shifts has been extended, but
rightshifts 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 bitvector solver, which should have become
more complete and faster. Shifts and bitwise operations are still
not fully supported.
 06/12/2017:
This release includes the first version of a bitvector solver,
including procedures for bitvector interpolation and bitvector
quantifier elimination. Bitvector support is still work in progress,
and currently most complete for linear arithmetic formulas; nonlinear
bitvector formulas work partly, and bitwise 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 frontend 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 nonlinear integer reasoning has been made proofproducing,
and therefore also supports Craig interpolation (however, interpolants
are not always quantifierfree).
 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 prettyprinted proof output using the option
+printProof
, and initial support for learning lemmas
(enabled whenever proofs are generated). Much better processing
of SMTLIB scripts, in particular when using the option
+incremental
for incremental processing. Various bugfixes.
 07/12/2015:
Various optimisations and bugfixes. The incremental SMTLIB 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 nonlinear integer arithmetic, and a complete
rewrite of the incremental SMTLIB parser that should make
Princess significantly faster and more standardcompliant for processing
SMTLIB scripts. The incremental SMTLIB 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 (nonGPL) systems, and the
addition of a clientserver mode. The latter mode avoids frequent
restart of the JVM, and the resulting startup delay. To use the clientserver
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 (countersatisfiable).
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 userdefined theory plugins via the API, as a way to
efficiently define new theories (to be extended).
 02/11/2012:
Various
changes
and
optimisations.
The
SMTLIB
2
interface
is
now
(at
least
partly)
incremental, so it can
process inputs with multiple
checksat
commands, and
handle push
and pop
to organisation the assertion stack; the provided answers should mostly
follow the SMTLIB 2 standard. Incremental problems are not yet handled
very efficiently though. There is a new option +stdin
to
read SMTLIB 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
prettyprinted
(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 precompiled 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
frontend, 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 shorthand 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
portfoliomode,
in
which
different
prove
strategies
are
applied
in
parallel
to
prove
a
problem; this mode can be enabled using the option
+multiStrategy
.
The
SMTLIB
2 parser now also supports arrays (as in, e.g., the SMTLIB
category AUFLIA).
 15/07/2011:
Improved
the
SMTLIB
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
.priparser, which now accepts conditional terms and formulae using the
syntax \if (cond) \then (t1) \else (t2)
(similar as in
KeY). More generally, the .priformat 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
1520%, 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
builtin
SMTLIB
2 parser, primarily targetting the logics QF_LIA and AUFLIA. The
parser does not yet support all features of the SMTLIB language, in
particular it is not supported to have formulae/Boolean expressions as
arguments of functions or predicates, and the handling of
userspecified 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
bugfixes,
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
nondeterminism
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
firstorder
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
postPhD
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
desugared version of the input problem in the SMTLib 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
unitresolution 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 (SMTlike) triggers to quantified formulae, which works
quite well together with unitresolution.
 18/9/2008:
The
first
version
of
Princess
that
implements
the
freeconstant
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
unitresolution 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
Cstyle
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 CASC26 in 2017, Gothenburg, Sweden.
The main change compared to 2016 is proof production for problems involving
nonlinear integer arithmetic (by introducing appropriate theory lemmas in
the proof).

06/06/2016: The version for CASCJ8 in 2016, Coimbra, Portugal.
Princess is now able to produce proofs/solutions, although not for all
problems (some modules are not yet proofproducing). 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 CASC25 in 2015, Berlin; compared
to the version for 2014, mainly bugfixes were done.

04/07/2014: The version for CASCJ7 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 startup time. For the daemon mode it is enough to run
the script
princesscascclient
, which should behave
just like the normal start script princesscasc
.
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 precompiled 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.