A Manual of Princess (to be extended)

Invocation

You can normally just call Princess with a command similar to ./princess <inputfile>. The source and binary distributions provide different scripts for invocation:

Options

A complete list of the Princess options can be obtained using option -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: +)

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

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

Logical 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.
\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.