A Manual (kind of)

Invocation

You can normally just call Princess with a command similar to ./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)

Options

A complete list of the Princess options can be obtained using options -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 SMT-LIB 2 problems from stdin       (default: -)
 [+-]incremental           Incremental SMT-LIB 2 interpreter        (default: -)
                             (+incremental implies -genTotalityAxioms)
 -timeout=val              Set a timeout in milliseconds        (default: infty)
 -timeoutPer=val           Set a timeout per SMT-LIB 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 SMT-LIB 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 quantifier-free 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           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: +)
 [+-]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: shift-and-add axiom
                             native:   built-in 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)

Structure of input files in the native format (.pri)

\sorts {
  /* Declare sorts and algebraic data-types */

  // 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}

Types

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 Boolean-values functions can also be declared in the \predicates section.

mod[lower, upper] Finite intervals of integers, but with operations interpreted with wrap-around semantics.

bv[bits] Unsigned fixed-size bit-vectors. bv[bits] is short-hand notation for mod[0, 2^bits - 1].

signed bv[bits] Signed fixed-size bit-vectors. bv[bits] is short-hand notation for mod[-2^(bits-1), 2^(bits-1) - 1].

ident Types declared in the \sorts section.

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 Boolean-values functions can also be declared in the `\predicates` section.
`mod[lower, upper]`	Finite intervals of integers, but with operations interpreted with wrap-around semantics.
`bv[bits]`	Unsigned fixed-size bit-vectors. `bv[bits]` is short-hand notation for `mod[0, 2^bits - 1]`.
`signed bv[bits]`	Signed fixed-size bit-vectors. `bv[bits]` is short-hand notation for `mod[-2^(bits-1), 2^(bits-1) - 1]`.
`ident`	Types declared in the `\sorts` section.

Built-in Operators

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 data-types 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 SMT-LIB, the bounds are inclusive, and the upper bit comes first.

s ^ n Exponentiation with non-negative integer exponent.

+t
-t Signed integer terms (positive or negative).

~t
-t Bit-wise negation of an unsigned bit-vector, 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) 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 Concatenation of two unsigned bit-vectors, i.e., terms of type bv[n].

s + t
s - t Sum and difference of two terms.

s << t
s >> t Left-shift and right-shift 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 bit-wise and of two unsigned bit-vectors, i.e., two terms of type bv[n].

phi | psi
phi || psi Disjunction of two formulae.
The operator | is overloaded and can also denotes bit-wise or of two unsigned bit-vectors, i.e., two terms of type bv[n].

phi -> psi
psi <- phi Implication between two formulae.

phi <-> psi Equivalence of two formulae.

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 data-types 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 SMT-LIB, the bounds are inclusive, and the upper bit comes first.
`s ^ n`	Exponentiation with non-negative integer exponent.
`+t` `-t`	Signed integer terms (positive or negative).
`~t` `-t`	Bit-wise negation of an unsigned bit-vector, 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) 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`	Concatenation of two unsigned bit-vectors, i.e., terms of type `bv[n]`.
`s + t` `s - t`	Sum and difference of two terms.
`s << t` `s >> t`	Left-shift and right-shift 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. (2x <= t & t <= 2x + 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 bit-wise and of two unsigned bit-vectors, i.e., two terms of type `bv[n]`.
`phi \| psi` `phi \|\| psi`	Disjunction of two formulae. The operator `\|` is overloaded and can also denotes bit-wise or of two unsigned bit-vectors, i.e., two terms of type `bv[n]`.
`phi -> psi` `psi <- phi`	Implication between two formulae.
`phi <-> psi`	Equivalence of two formulae.