AbSolute is a constraint solver based on abstract domains. It implements the solving method presented in: "A Constraint Solver Based on Abstract Domains". This is a simplified version that does not enjoy all the features of the real AbSolute which can be found here.
/* simple example with sinus and cosinus */
init{
real x = [-10;10];
real y = [-5;5];
}
constraints{
y < sin(x) + 1;
y > cos(x) - 1;
}
You can see other examples of problems in the problem directory
A simple make will do the job.
For some reason, having both packages libapron and libapron-dev installed will make the building of absolute fail. Therefore, the easiest way to deal with apron is to install it with and only with opam : https://opam.ocaml.org/packages/
./solver.opt problemto display the list of options, type: ./solver.opt -help or ./solver.opt --help
- An ANSI C compiler
- OCaml > 4.01 : http://ocaml.org/
- Apron: http://apron.cri.ensmp.fr/library/
- Zarith : https://forge.ocamlcore.org/projects/zarith
AbSolute is currently still in developpement, and have not been tested. Feel free to contact any member of the developpement team if you want to report a bug or suggest a feature