Hackage :: [Package]

LPPaver: An automated prover targeting problems that involve nonlinear real arithmetic

[ formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers, verification ] [ Propose Tags ] [ Report a vulnerability ]

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

[Skip to Readme]

Modules

[Last Documentation]

  • LPPaver
    • Algorithm
      • LPPaver.Algorithm.DNF
      • LPPaver.Algorithm.Linearisation
      • LPPaver.Algorithm.Type
      • LPPaver.Algorithm.Util
    • Constraint
      • LPPaver.Constraint.Type
      • LPPaver.Constraint.Util

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.0.3.1, 0.0.5.0
Change log ChangeLog.md
Dependencies aern2-mfun (>=0.2.9 && <0.3), aern2-mp (>=0.2.9.1 && <0.3), base (>=4.7 && <5), collect-errors (>=0.1 && <0.2), containers (>=0.6 && <0.7), directory (>=1.3 && <1.4), filepath, LPPaver, mixed-types-num (>=0.5.10 && <0.6), optparse-applicative (>=0.16 && <0.17), parallel (>=3.2 && <3.3), pqueue (>=1.4 && <1.5), PropaFP (>=0.1.1 && <0.2), simplex-method (>=0.1 && <0.2) [details]
License MPL-2.0
Copyright MPL-2.0
Author Junaid Rasheed
Maintainer rasheeja@aston.ac.uk
Category Math, Maths, Mathematics, Formal methods, Theorem Provers, verification
Home page https://github.com/rasheedja/LPPaver#readme
Bug tracker https://github.com/rasheedja/LPPaver/issues
Source repo head: git clone https://github.com/rasheedja/LPPaver
Uploaded by JunaidRasheed at 2023-03-13T19:52:05Z
Distributions
Executables lppaver
Downloads 179 total (3 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2023-03-13 [all 2 reports]

Readme for LPPaver-0.0.5.0

[back to package description]

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:

Formula describing the Place benchmarks

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.