An automated prover targeting problems that involve nonlinear real arithmetic.

Please see the README on GitHub at https://github.com/rasheedja/LPPaver#readme

LPPaver

LPPaver is an automated prover which targets problems involving nonlinear real arithmetic. A paper describing LPPaver in detail is coming soon.

Documentation

Haddock documentation for LPPaver can be found at Hackage.

Reference

LPPaver understands input that is similar to SMT2. LPPaver is designed to work with SMT2 asserts. If an assert contains anything that LPPaver does not understand, the assertion is (currently) silently dropped. The full list of accepted inputs can be found in REFERENCE.md

Building

LPPaver can be built with either Stack or Cabal, though officially we only support Stack.

Stack

stack build

Cabal

cabal build

Examples

Examples can be found in directory test/testFiles. The Place directory contains examples that describe the problem of placing circles of a fixed size into a square of a fixed size in such a way that all of the circles are within the square none of the circles are touching each-other or the edges of the square. The problem has also been generalised to higher dimensions. A formula describing the problem is shown below:

The PropaFP directory contains examples that came from PropaFP. These examples are described in detail in a preprint of a paper describing PropaFP.

In both directories, the sat subdirectory holds files which should be satisfiable, the unsat subdirectory holds files which should be unsatisfiable, and the cannotDecide subdirectory holds files which LPPaver could not decide with default parameters.