./princess <inputfile>
.
The source and binary distributions provide different scripts
for invocation:
princess
: script for running Princess on the
command line (Linux, UNIX, MacOS)
princess.bat
: Windows batch file for running Princess on the
command line
princessGui
: script for starting the graphical Princess
interface (Linux, UNIX, MacOS)
princessGui.bat
: Windows batch file for starting
the graphical Princess interface
princessClient
: script for running Princess on the
command line in client-server mode. This will keep a Princess daemon
running in the background to avoid repeated (slow) start-up of the
Java virtual machine; when no longer used, the daemon will shut itself
down after a few minutes.
werePrincess, werePrincess.bat
: older scripts for
integration in the Wolverine model checker (now mostly defunct)
-h
:
Options: [+-]logo Print logo and elapsed time (default: +) [+-]version Print version and exit (default: -) [+-]quiet Suppress all output to stderr (default: -) [+-]printTree Output the constructed proof tree (default: -) -inputFormat=val Specify format of problem file: (default: auto) auto, pri, smtlib, tptp [+-]stdin Read SMT-LIB 2 problems from stdin (default: -) [+-]incremental Incremental SMT-LIB 2 interpreter (default: -) (+incremental implies -genTotalityAxioms) -printSMT=filename Output the problem in SMT-LIB format (default: "") -printTPTP=filename Output the problem in TPTP format (default: "") -printDOT=filename Output the proof in GraphViz format (default: "") [+-]assert Enable runtime assertions (default: -) -timeout=val Set a timeout in milliseconds (default: infty) -timeoutPer=val Set a timeout per SMT-LIB query (ms) (default: infty) [+-]multiStrategy Use a portfolio of different strategies (default: -) -simplifyConstraints=val How to simplify constraints: none: not at all fair: fair construction of a proof lemmas: proof construction with lemmas (default) [+-]traceConstraintSimplifier Show constraint simplifications (default: -) [+-]mostGeneralConstraint Derive the most general constraint for this problem (quantifier elimination for PA formulae) (default: -) [+-]dnfConstraints Turn ground constraints into DNF (default: +) -clausifier=val Choose the clausifier (none, simple) (default: none) [+-]posUnitResolution Resolution of clauses with literals in (default: +) the antecedent -generateTriggers=val Automatically choose triggers for quant. formulae none: not at all total: for all total functions (default) all: for all functions -functionGC=val Garbage-collect function terms none: not at all total: for all total functions (default) all: for all functions [+-]tightFunctionScopes Keep function application defs. local (default: +) [+-]genTotalityAxioms Generate totality axioms for functions (default: +) [+-]boolFunsAsPreds In smtlib and tptp, encode (default: -) boolean functions as predicates -mulProcedure=val Handling of nonlinear integer formulae bitShift: shift-and-add axiom native: built-in theory solver (default) -constructProofs=val Extract proofs never ifInterpolating: if \interpolant occurs (default) always [+-]simplifyProofs Simplify extracted proofs (default: +) [+-]elimInterpolantQuants Eliminate quantifiers from interpolants (default: +)
\universalConstants { /* Declare universally quantified constants of the problem */ // int x; } \existentialConstants { /* Declare existentially quantified constants of the problem */ // int Y; } \functions { /* Declare constants and functions occurring in the problem * (implicitly universally quantified). * The keyword "\partial" can be used to define functions without totality axiom, * while "\relational" can be used to define "functions" without functionality axiom. */ // int z; // int f(int); // \partial int g(int, int); } \predicates { /* Declare predicates occurring in the problem * (implicitly universally quantified) */ // p(int, int); } \problem { /* Problem to be proven. The implicit quantification is: * \forall; * \exists ; * \forall ; ... */ true } // \interpolant{p1; p2, p3}
The following table describes the operators available for writing
terms and formulae in Princess, within
the \problem
section. The operators are listed in order of
precedence, i.e., the first operator binds strongest, the last
operator least strong.
Operator | Description |
---|---|
(...) |
Parentheses can be used to group terms and formula, and overwrite the natural precedence of operators. |
\if (cond) \then (a) \else (b) |
Conditional terms and formulae. A conditional expression evaluates to a if cond is true , and to b
otherwise.Conditional expressions can be used for both terms and formulae. |
\abs (t) |
Absolute value of a term. |
\max (t1, ..., tn) \min (t1, ..., tn) |
Maximum and minimum value of a set of terms. |
\distinct (t1, ..., tn) |
Terms or formulae are pairwise distinct. |
s ^ n |
Exponentiation with non-negative integer exponent. |
+t -t |
Signed integer terms (positive or negative). |
s * t |
Product of two terms. To stay within Presburger arithmetic (linear integer arithmetic), one of the two terms has to be a literal constant. Multiplication of other expressions is handled via (incomplete) built-in algorithms such as Groebner bases and interval propagation. |
s / t s % t |
Euclidian quotient and remainder of two terms. The operations are within Presburger arithmetic if t
is a literal constant; otherwise, they will be encoded with the help
of multiplication. |
s + t s - t |
Sum and difference of two terms. |
s = t s != t s < t s <= t s > t s >= t |
Binary relations between integer terms. |
!phi |
Negation of a formula. |
\forall int x; phi \exists int x; phi |
Universal and existential quantifiers . Quantifiers over multiple variables can be written as \forall int x, y, z; phi or
\forall (int x; int y) phi .
The available types for quantification are mathematical integers int , natural numbers nat , and
intervals of integers such as int[0, 10], int[-inf, 5], int[0, inf] .Triggers describing strategies to instantiate a quantified formula can be specified using the syntax \forall int x, y; {f(x), g(y)} phi . Also multiple triggers can be given, e.g.,
\forall int x; {f(x)} {g(y)} phi . NB: Quantifiers bind more strongly than most Boolean connectives; for instance, the formula \forall int x; A & B will be parsed as (\forall int x; A) & B . |
\eps int x; phi |
Epsilon terms. An epsilon term evaluates to some value x such that phi is satisfied. For instance,
\eps int x. (2*x <= t & t <= 2*x + 1) encodes the integer division t div 2 , rounding downwards.NB: The meaning of epsilon expressions is undefined if there are no or multiple values of x
satisfying phi . |
\part[n] phi |
Labelling of a formula. Labels are currently only used for interpolation. |
phi & psi |
Conjunction of two formulae. |
phi | psi |
Disjunction of two formulae. |
phi -> psi psi <- phi |
Implication between two formulae. |
phi <-> psi |
Equivalence of two formulae. |