verimag-polyhedra / vpl Goto Github PK

View Code? Open in Web Editor NEW

17.0 5.0 2.0 1.43 MB

Verimag Polyhedra Library

License: GNU Lesser General Public License v3.0

Makefile 0.19% OCaml 78.51% Coq 21.18% Standard ML 0.08% Shell 0.04%

abstract-domain polyhedral-computations polyhedra coq-formalization

vpl's Introduction

VPL (Verified Polyhedra Library)

GENERAL INFORMATIONS

The VPL is an Ocaml library allowing to compute with convex polyhedra. It provides standard operators -- certified in Coq -- to use this library as an abstract domain of polyhedra.

Contributors: Alexis Fouilhé, Alexandre Maréchal, Sylvain Boulmé, Hang Yu, Michaël Périn, David Monniaux. Developed at Verimag and supported by ANR Verasco and ERC Stator.

If you find a bug or have any comment, feel free to contact us at [email protected]

INSTALLATION

From opam

First, add the following repository in your opam system:
```
 opam repo add vpl https://raw.githubusercontent.com/VERIMAG-Polyhedra/opam-vpl/master
```
Then, install the following packages (depending on your needs):
- vpl-core: the ocaml library
```
opam install vpl-core
```
- coq-vpl: the Coq library (only needed to get Coq proofs about VPL operators)
```
opam install coq-vpl
```
- coq-vpltactic: the VplTactic plugin for Coq (also install coq-vpl and vpl-core)
```
opam install coq-vpltactic
```
From sources
1. Dependencies
  
  The VPL requires the following packages:
  - ocaml required version >= 4.08.0
  - zarith available in OPAM tested with version 1.4.1 and 1.9.1
  - dune available in OPAM required version >= 2.1
2. Compiling the VPL
  
  (Optional) To re-extract from the coq files, simply run at the root directory
```
 make coq_extract
```
  To compile the VPL, simply run from the root directory
```
 make vpl
```
  Tests can be run by typing
```
 make check
```
  Finally, to install the library with ocamlfind, type
```
 make install
```
  To uninstall the library from ocamlfind, run
```
 make uninstall
```

Documentation

Documentation can be built from sources with

make doc; make open_doc

It contains the interface of main modules.

Using the VPL

There are several ways to use the library.

From Coq (see opam package coq-vpl)
As a Coq tactic (see VplTactic)
As an OCaml library (see opam package vpl-core)

As an OCaml library, the entry point of the VPL is the module UserInterface, which contains several version of the abstract domain. Polyhedral domains can work over Q or Z, and there are three levels of certification, which gives 6 possible domains. The level of certifications are:

No certification: no certificate is produced. This is implemented in modules UncertifiedZ and UncertifiedQ.
OCaml certification: Each operator of the domain produces a certificate, ie a witness of its computation that can be checked. This is implemented in modules OCamlCertifiedZ and OCamlCertifiedQ.

As an OCaml library (see opam package vpl-core)

Coq certification: In addition to guarantees offered by OCaml certification, certificates are here extracted from Coq proven types. This is implemented in modules CoqCertifiedZ and CoqCertifiedQ.

Documentation

Online: link
From sources: make doc

The html documentation is then generated in the folder _build/_doc/_html/index.html

vpl's People

Contributors

Stargazers

Watchers

Forkers

isbnhao paulraunite

vpl's Issues

HTML page

Make a HTML page with the VPL doc.
Upload it somewhere ?

Opam package

Fix the opam package for opam 2.0.
Fix VPL dependencies.

New operator: projection and inclusion testing

Make a new operator that, given two polyhedra A and B:

Computes the projection A|X on a set of variables X.
Checks if A|X contains B

Handelman Normalization

Try putting normalization on all Handelman's products except the linear part of the polynomial.

Handelman default heuristic

Handelman default heuristic builds all combination up to a certain degree (the degree of the polynomial to linearize). However, it currently seems to compute too many combinations: the degree must be wrong.

Code normalization

Type, module and function names should be normalized.

Check polynomial parser

Maintain PLP regions

IneqSet must maintain an optional partition into regions.
After calling a PLP operator, regions must be stored into the abstract value.

Assume_back: renormalization

When assuming back a constraint which puts the normalization point outside of the result's interior, regions must be renormalized to a new normalization point.
Can it be done by simply replacing the normalization constraint with a new one in each region ?

Join operator: certificate failure - strict inequalities

Certificates may fail when computing the join of two polyhedra with strict inequalities.
Example :
First polyhedron

P1 = -1.v2 + 1.v4 <= 0
1.v2 + 1.v4 <= 5
14.v2 + 5.v4 <= 237/4
-1.v4 <= 0
-293/56.v2 + -5/2.v4 < -461/56

Second polyhedron

P2 = -1.v2 <= -1
-1.v4 <= 2
14.v2 + 5.v4 <= 237/4
1.v4 < 0
-333/56.v2 + 2.v4 < -501/56

Output

14.v2 + 5.v4 <= 237/4: 14.v2 + 5.v4 <= 237/4
-1.v2 + 1.v4 < 0: -1.v2 + 1.v4 <= 0 
1.v2 + 1.v4 < 5: 1.v2 + 1.v4 <= 5
-1.v4 < 2: -1.v4 < 2
-1.v2 < -1: -1.v2 < -1
-2221/56.v2 + 1.v4 < -2305/56: -2221/56.v2 + 1.v4 < -2305/56

Fix trace generation

Trace generation has been adapted for the new trace language. It needs to be checked.

Incremental operators

Make operators incremental: one must be able to add a constraint to the input polyhedron, and reuse the previous result to avoid recomputing everything.

Handelman Plotting

Handelman plotting has a strange shape :

open Vpl;;
open Calculator;;
open Notations;;

Flags.lin := Flags.Handelman;;
Debug.enable();;
Debug.set_colors();;
Debug.print_enable();;

PLPCore.Debug.enable DebugTypes.([Title ; MInput ; MOutput ; Normal ; Sage]);;
let p = parse "x >= 1, y >= -2, x - y >= 0, x + y <= 5, x * x + y * y <= 4";;

Ocaml version?
GLPK? Eigen?
Coq version ?

User interface

Make the user interface simpler and clearer.

General code review

The code should be reviewed to track down sources of inefficiency.
In particular, some lists may be changed into arrays when necessary.

verimag-polyhedra / vpl Goto Github PK

vpl's Introduction

VPL (Verified Polyhedra Library)

GENERAL INFORMATIONS

INSTALLATION

Documentation

Using the VPL

Documentation

vpl's People

Contributors

Stargazers

Watchers

Forkers

vpl's Issues

Recommend Projects

Recommend Topics

Recommend Org