If
you
are
adventurous,
you
can
download
the
latest Princess sources
right from the SVN
repository:svn co svn://hal4.it.uu.se/princess/interpolation/trunk
Username and password are both anonymous .
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.
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).
testcases/api/ADTTest*
and
testcases/smtlib/datatype*
. Various bugfixes.
+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.
./princessGui
).
Many thanks go to Matthias Heizmann for various
bug reports over the last months!
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.
./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
.
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).
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.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). +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. 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; ...
. +multiStrategy
). +multiStrategy
.
The
SMT-LIB
2 parser now also supports arrays (as in, e.g., the SMT-LIB
category AUFLIA).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)
.+assert
. -printDOT=<filename>
.
\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. +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.-dnfConstraints
, the conversion of
constraints to DNF
during proof construction is less aggressive, which can be more
efficient in some cases.-printSMT=<filename>
, Princess can be
told to save a
de-sugared version of the input problem in the SMT-Lib format.-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. +posUnitResolution
is now the default, because
when using functions it is usually the preferable setting.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. +posUnitResolution
) and encodings of
functions as predicates practical. Of course, the new Princess version
also contains many bugfixes. 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. +printProof
. Princess has also become
a bit more clever with learning lemmas.
princess-casc-client
, which should behave
just like the normal start script princess-casc
.
Also a new binary is available.
+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.