Snapshots of the Princess Sources
- 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