Princess — The Scala Theorem Prover

Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted predicates, written entirely in Scala. Princess can reason about problems in integer arithmetic, augmented with predicates that can be axiomatised arbitrarily. Such problems can contain arbitrary quantifiers to express that some formula is supposed to hold for all or for some integers.

Main features of Princess include:

• Decision + quantifier elimination procedure for Presburger arithmetic.
• Modules for various theories beyond Presburger:
  Equality, uninterpreted functions/predicates (EUF); non-linear integer arithmetic; rationals; bit-vectors; arrays; heap; algebraic data-types (ADTs); strings.
• Proof generation and Craig interpolation for several of the theories:
  Presburger, EUF, non-linear integers, bit-vectors, arrays, heap, ADTs.
• Support for both free variables and triggers and e-matching to handle quantifiers.
   
• Input formats: native language of Princess, SMT-LIB 2, and TPTP (FOF/TFF/CNF, see details).
• Convenient APIs: for use in Scala applications or Java applications.

Princess runs on any platform that provides a Java runtime environment (version 1.5 or higher).

Princess won the TFA division (arithmetic problems) at CASC J6, 2012. In 2013 and 2014, Princess won in the TFI category of CASC, (integer problems), and was runner-up in the overall TFA division. We currently maintain a separate branch for full support of the TPTP format.

Princess is free software. Since version 2021-03-10, Princess is distributed under BSD 3-clause. Previous versions were distributed under LGPL v2.1 or later; under LGPL v3, and even earlier under GPL v3.

Please contact me if you are interested in any projects or thesis work related to Princess.

Examples

Sources

Benchmarks

Documentation and Publications

• A basic manual of Princess. Examples are included in the Princess distributions, and on the examples page.
• Definition of the Princess syntax.
• Princess API.

• LPAR'08 paper about the calculus that is used in Princess. Please refer to this paper if you want to cite Princess:

  @InProceedings{princess08,
    author    = {Philipp R{\"u}mmer},
    title     = {A Constraint Sequent Calculus for First-Order Logic with
                 Linear Integer Arithmetic},
    booktitle = {Proceedings, 15th International Conference on Logic
                 for Programming, Artificial Intelligence and
                 Reasoning},
    year      = 2008,
    volume    = {5330},
    pages     = {274-289},
    isbn      = {978-3-540-89438-4},
    series    = {LNCS},
    publisher = {Springer}
  }
  

• A more detailed description of the calculus and Princess is part of my PhD thesis
• IJCAR paper on interpolant generation in Presburger arithmetic
• VERIFY and VMCAI papers on interpolant generation in the presence of uninterpreted predicates, functions, and arrays
• LPAR paper about e-matching and the handling of functions in Princess
• The native input format of Princess much resembles the format that is used by the KeY tool. You can have a look at the example files that are included in the distributions below.

Installation of the binary distribution

We provide a binary distribution of the latest version of Princess. This distribution contains all required libraries, i.e., the Scala API and the Cup parser generator library; it is only necessary to have a Java runtime environment (version 1.5 or newer) installed.

To install, just download the archive and unpack it in some directory of your choice. The Princess gui can then be invoked using the script princessGui, the command line tool using the script princess. In addition, the script princessClient can be used to run Princess in client-server mode (more details).

Using Princess as a Scala Library

If you want to use the Princess API, it is easiest to start from the class ap.SimpleAPI, and use the functions in ap.parser.IExpression to construct formulae. A number of examples are included in both the source and binary distributions, in directory testcases/api.

Stable versions of Princess can be obtained from Maven Central, it is enough to add the following line to your build.sbt script:

libraryDependencies += "io.github.uuverifiers" %% "princess" % "2024-01-12"

For use in Scala3, the line has to be modified to:

libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2024-01-12").cross(CrossVersion.for3Use2_13)

We also maintain a local Maven repository with stable and unstable Princess versions, with URL https://eldarica.org/maven/ and organisation id uuverifiers. If you build your software using sbt, you can simply add the following two lines in the build.sbt script to automatically download Princess during compilation:

resolvers += "uuverifiers" at "https://eldarica.org/maven/"

libraryDependencies += "uuverifiers" %% "princess" % "2024-01-12"

You can download a complete hello-world project here. The example can be compiled using sbt. If you have sbt installed, just calling sbt run in directory hw should take care of downloading Princess, and all other dependencies, compilation, and running the example.

Other examples:

• Sudoku
• String constraints, solved using the OSTRICH library

Using Princess as a Java Library

The class ap.JavaWrapper can be used for processing input in textual form, for instance stored as string or a file, with exactly the same functionality as on the command line:

[...]

final ArrayList<String> options = new ArrayList<> ();

options.add("-inputFormat=pri");   // Input in the Princess format
options.add("+quiet");             // No warnings or debugging output

final String input1 =
  "\\functions { int x, y, z; } \\problem { x > y & y > z -> x > z }";

System.out.println(JavaWrapper.readFromString(input1, options));

[...]

> mvn package
> mvn exec:java -Dexec.mainClass=SimpleSolving

To generate formulas programmatically within a Java application, we recommend that you have a look at the JavaSMT wrapper, which provides uniform access to Princess and many other SMT solvers. When building Java programs using Maven, it is enough to put the following lines in your pom.xml to have all required libraries downloaded automatically:

<project ...>
  ...

  <dependencies>
    <dependency>
      <groupId>org.sosy-lab</groupId>
      <artifactId>java-smt</artifactId>
      <version>4.1.0</version>
    </dependency>
    <dependency>
      <groupId>io.github.uuverifiers</groupId>
      <artifactId>princess_2.13</artifactId>
      <version>2023-06-19</version>
    </dependency>
  </dependencies>
</project>

You can again download a complete hello-world project, again including a Maven build file pre-configured to use Princess together with JavaSMT. If you have Maven installed on your machine, you can compile and run the example by invoking

> mvn package
> mvn exec:java -Dexec.mainClass=Riddle

Other Java examples:

• Interpolation example

Installation of the binary CASC/TPTP distribution

We currently maintain a separate branch for full support of the TPTP format. You can download a binary of the latest version, or the sources. This version differs from normal Princess mainly in the following points:

• the default input format is chosen to be TPTP;
• by default, the prover runs with the option +multiStrategy, with a portfolio of strategies optimised for TPTP problems;
• results are output in the SZS notation;
• to generate and output proofs, the option +printProof can be added.

The Royal Family

• ePrincess, a variant of Princess that uses Bounded Rigid E-Unification for closing branches.
• iPrincess (now defunct), which added support for Craig interpolation to Princess. This functionality is now integrated in the main Princess branch.

Compilation and Installation from Sources using sbt

1. Unpack one of the snapshots (preferably the newest one) and change to the princess-* directory
2. Call sbt run in order to compile Princess and run it
3. Call sbt assembly to create a standalone jar file that you can run with java -jar target/scala-2.XX/Princess-assembly-XX.jar.

After sbt assembly, you can also use the provided scripts princess, princessGui, princessClient to invoke Princess through the jar file.

Compilation and Installation from Sources using make

The compilation is so far only tested on Linux systems. For the installation, using the make tool, you need:

• A compiler for Scala version 2.11 or newer
• A Java SDK version 1.5 or newer
• The Cup parser generator for Java (get the file java-cup-11a.jar)
• If you want to compile the parser yourself (binaries are included in the Princess snapshots below), you also need the BNF converter and JLex.

The actual installation consists of the following steps:

1. Unpack one of the snapshots (preferably the newest one) and change to the princess-* directory
2. Create a directory extlibs and copy the file java-cup-11a.jar into it
3. In case you want to compile the parser yourself (not necessary), run make parser-jar
4. Run make to compile Princess.

If everything went ok, it is possible to run Princess with the command ./princess <inputfile>
A list of the Princess options can be printed using ./princess -h

Applications

• JavaSMT, a unifying Java interface for SMT solvers
• Seneschal, a ranking function generator for bitvector relations
• Eldarica, a predicate abstraction-based model checker
• Joogie, Gravy, and Bixie, tools for detecting inconsistent and infeasible code in Java applications
• JayHorn, a Java model checker
• Picasso, a static analyzer for depth-bounded systems

Funding

• The Microsoft Research PhD Grant "First-Order Satisfiability Modulo Theories" (2013-2016)
• The Swedish Research Council grant 2014-5484 "Satisfiability Modulo Theories and Quantifiers" (2015-2018)