./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 clientserver mode. This will keep a Princess daemon
running in the background to avoid repeated (slow) startup 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
and +fullHelp
:
Standard options: [+]logo Print logo and elapsed time (default: +) [+]fullHelp Print detailed help and exit (default: ) [+]version Print version and exit (default: ) [+]quiet Suppress all output to stderr (default: ) [+]assert Enable runtime assertions (default: ) inputFormat=val Specify format of problem file: (default: auto) auto, pri, smtlib, tptp [+]stdin Read SMTLIB 2 problems from stdin (default: ) [+]incremental Incremental SMTLIB 2 interpreter (default: ) (+incremental implies genTotalityAxioms) timeout=val Set a timeout in milliseconds (default: infty) timeoutPer=val Set a timeout per SMTLIB query (ms) (default: infty) [+]model Compute models or countermodels (default: ) [+]unsatCore Compute unsatisfiable cores (default: ) [+]printProof Output the constructed proof (default: ) [+]mostGeneralConstraint Derive the most general constraint for this problem (quantifier elimination for PA formulae) (default: ) clausifier=val Choose the clausifier (none, simple) (default: none) [+]genTotalityAxioms Generate totality axioms for functions (default: +) Further general options  [+]printTree Output the internal constraint tree (default: ) printSMT=filename Output the problem in SMTLIB format (default: "") printTPTP=filename Output the problem in TPTP format (default: "") printDOT=filename Output the proof in GraphViz format (default: "") portfolio=val Use a strategy portfolio (default: none) none: off casc: Optimised for CASC/TPTP qf_lia: Optimised for quantifierfree LIA bv: Optimised for quantified BV formulaSign=val Optionally negate input formula (default: auto) positive: do not negate negative: negate auto: choose automatically randomSeed=val Seed for randomisation <seed>: numeric seed (default: 1234567) off: disable randomisation Proof/interpolation options  constructProofs=val Extract proofs never ifInterpolating: if \interpolant occurs (default) always [+]elimInterpolantQuants Eliminate quantifiers from interpolants (default: +) Quantifier/constraint options  [+]posUnitResolution Resolution of clauses with literals in (default: +) the antecedent [+]useStrengthenTree For quantified formulae with inequality (default: ) side conditions, use the StrengthenTree constraint tree constructor 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: ) [+]dnfConstraints Turn ground constraints into DNF (default: +) Function options  generateTriggers=val Automatically choose triggers for quant. formulae none: not at all total: for all total functions (default) all: for all functions complete, completeFrugal: in combination with genTotalityAxioms, in such a way that completeness is not affected triggerStrategy=val How to choose triggers for quantified formulae allMinimal allMinimalAndEmpty allMaximal maximal (default) maximalOutermost functionGC=val Garbagecollect function terms none: not at all total: for all total functions (default) all: for all functions [+]tightFunctionScopes Keep function application defs. local (default: +) [+]boolFunsAsPreds In smtlib and tptp, encode (default: ) Boolean functions as predicates [+]reverseFunctionalityPropagation Infer distinctness of (default: ) arguments from distinctness of results [+]useFunctionalConsistencyTheory Use dummy theory to represent (default: ) functional consistency axioms Theory options  mulProcedure=val Handling of nonlinear integer formulae bitShift: shiftandadd axiom native: builtin theory solver (default) adtMeasure=val Measure to ensure acyclicity of ADTs relDepth: relative depth of terms size: size of terms (default) stringSolver=val Specify the used string solver (default: ap.theories.strings.SeqStringTheory)
\sorts { /* Declare sorts and algebraic datatypes */ // Sort; // Colour { red; green; blue; }; // BoolList { nil; cons(bool head, BoolList tail); }; } \universalConstants { /* Declare universally quantified constants of the problem */ // int x; } \existentialConstants { // Synonyms: \variables, \metaVariables /* 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; p4}
The following table describes the types that can be used when declaring constraints, predicates, functions, or in quantifiers.
Operator  Description 

int 
Mathematical integers. 
nat 
Natural numbers. 
int[lower, upper] 
Intervals of integers,
such as int[0, 10], int[inf, 5], int[0, inf] . 
bool 
Booleans. NB: Boolean variables and Booleanvalues functions can also be declared in the \predicates section. 
mod[lower, upper] 
Finite intervals of integers, but with operations interpreted with wraparound semantics. 
bv[bits] 
Unsigned fixedsize bitvectors. bv[bits]
is shorthand notation for mod[0, 2^bits  1] .

signed bv[bits] 
Signed fixedsize bitvectors. bv[bits]
is shorthand notation for
mod[2^(bits1), 2^(bits1)  1] .

ident 
Types declared in the \sorts section. 
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. 
f(t1, ..., tn) t.f 
Function application. The syntax
t.f is only available for unary functions. 
\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) t.\abs 
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. 
\size(t) t.\size 
Term size in algebraic datatypes
declared in the \sorts section. 
t[bit] 
Extraction of an individual bit from
a term of type bv[n] or signed bv[n] . 
t[from:to] 
Extraction of an interval
[from, to] of bits from
a term of type bv[n] or signed bv[n] .
Like in SMTLIB, the bounds are inclusive, and the upper
bit comes first. 
s ^ n 
Exponentiation with nonnegative integer exponent. 
+t t 
Signed integer terms (positive or negative). 
~t t 
Bitwise negation of an unsigned bitvector,
a term of type bv[n] . 
\as[type](t) t.\as[type] 
Cast of a term to a given type. 
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) builtin 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 
Concatenation of two unsigned bitvectors, i.e.,
terms of type bv[n] . 
s + t s  t 
Sum and difference of two terms. 
s << t s >> t 
Leftshift and rightshift 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 type x; phi \exists type 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 . 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 type 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 used for interpolation (with \interpolant ),
and when computing unsatisfiable cores
(option +unsatCore ). 
phi & psi phi && psi 
Conjunction of two formulae. The operator & is overloaded and can also denotes
bitwise and of two unsigned bitvectors, i.e.,
two terms of type bv[n] .

phi  psi phi  psi 
Disjunction of two formulae. The operator  is overloaded and can also denotes
bitwise or of two unsigned bitvectors, i.e.,
two terms of type bv[n] .

phi > psi psi < phi 
Implication between two formulae. 
phi <> psi 
Equivalence of two formulae. 