mpelleau / absolute Goto Github PK
View Code? Open in Web Editor NEWConstraint solver based on abstract domains
License: GNU Lesser General Public License v3.0
Constraint solver based on abstract domains
License: GNU Lesser General Public License v3.0
AbSolute does not seem to have a test library/framework yet, and I would need one to make simple tests on the octagon abstract domain I'm developing.
Since I won't (shouldn't ? ;-)) be the only one to use it, I prefer to ask what is your preference.
After a quick look on the ones available in OPAM, my preference goes to ppx_inline_test for the following reasons:
What do you think?
Hello,
I cannot install AbSolute via opam. As I can build AbSolute from the sources, I have compared both sources from master branch and the opam package sources :
dune
file in the opam package contains the line(c_names src/ml_float)
instead of
(c_names ml_float)
which leads to a dune error
Pervasives
is still used in the source files which leads to deprecation error.My environment :
Best,
Christophe
Segfault with rational boxes on an octagon problem (octagon.abs
added in pull request #12).
Replicate with:
absolute -domain boxQ problems/octagon.abs
absolute -domain boxQS problems/octagon.abs
Problem: AbSolute is compiled with a Makefile, and script to support compilation with and without the VPL library.
Also if we want to ppx_inline_test
as a test framework (issue #6), the compilation script will get heavier.
Proposed solution: I suggest to use Dune which is a modern OCaml build system. The advantages include:
ppx_inline_test
and Menhir
.(library
((name absolute)
(libraries (vpl (select vpl_domain.ml from
(vpl -> vpl_domain.ok.ml)
(!vpl -> vpl_domain.ko.ml))))))
self explanatory
Travis CI is a tool for continuous integration of projects, which is very useful to know when the project is does not compile anymore (which frequently happens :-)).
I set the .travis.yml
file on my fork, and it works well.
If you are interested, and in order to make it work on this repository, here the steps (it should take 5 minutes):
And it should work.
Hello,
I'm trying this set of constraints :
init{
int x = [-20;20];
int y = [-1;2];
}
constraints{
x - y > 1;
x - y < 0;
}
When solving this (with the command $ ./solver.opt problems/test.txt ),
I get
solving ends
Unique solution - #created nodes: 2
I don't think it should be possible.
I've looked at the other problems and I think that the syntax is correct.
What I've tried :
-using real instead of int : same problem
-using different domains : same problem sometimes. But with y in [0;2] for instance the problem disappear (the solver say that there are no solutions).
-using another precision that the default one (with the option -p). Even with precision 0 or precision 120, I still get one solution
-with not strict inequalities (typing >= and <=) : same problem
I've also tried to locate the said solution. The visualization option does not help.
Thus I've tried to add constraints.
If I add the constraint y>1, no solution. So in the solution, y should be <= 1.
But if I add the constraint y<=1, no solutions either.
Is there a way to print the found solutions (other than the visualization option)?
Maybe I just did something wrong in the syntax or maybe I missed something, but I don't know what.
Step by step does not work when pruning is enabled.
Self explanatory
F.to_rat F.inf
throws a signal FPE (floating point exception).
Can Mpqf represent infinite numbers? Nothing is written in its documentation.
This is problematic in the function var_bounds
if the bounds are not constrained yet.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.