summaryrefslogtreecommitdiff
path: root/abstract/formula.ml
Commit message (Expand)AuthorAgeFilesLines
* Clean up & comment a bit.Alex Auvolat2014-07-151-62/+103
* Acceptable heuristic.Alex Auvolat2014-07-111-2/+15
* DP locations defined by abstract values and not by formula.Alex Auvolat2014-07-101-20/+0
* Fix a few things, this doesn't work well.Alex Auvolat2014-07-101-0/+2
* Now it's starting to work...Alex Auvolat2014-07-091-0/+18
* Add simplification pass && better heuristic for BDDs based on ternaries.Alex Auvolat2014-07-091-9/+42
* Correct some bugs on clocks.Alex Auvolat2014-07-081-2/+4
* Add ternaries, simplifications. BIG BUG FOUND (init/reset translation)Alex Auvolat2014-07-081-0/+68
* First implementation of resetting transitions.Alex Auvolat2014-07-041-11/+17
* Use LAST instead of NEXT (only EDD implementation works at the moment)Alex Auvolat2014-07-041-1/+2
* Adapt for real type with Apron ; not very efficient ATM.Alex Auvolat2014-07-011-9/+11
* Not much. Still does not work very well.Alex Auvolat2014-06-201-5/+5
* Everything proved !!Alex Auvolat2014-06-191-0/+2
* Did most of the boring stuff. Now, work on the abstract domain.Alex Auvolat2014-06-191-24/+40
* Isolate numerical part of domain. Next: isolate numerical part of equations.Alex Auvolat2014-06-191-7/+13
* Nice view of guarantees ; add half test, proved.Alex Auvolat2014-06-181-9/+12
* Add gilbreath suite ; booleans are not represented in a good way.Alex Auvolat2014-06-181-0/+20
* Pretty printing.Alex Auvolat2014-06-181-7/+11
* Write transformation of program into logical formula.Alex Auvolat2014-06-171-0/+78
* Add AST for logical formula.Alex Auvolat2014-06-171-0/+24
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 16:59:10 +0000