Add a logico-numerical abstract domain
caballa opened this issue · 3 comments
caballa commented
From @caballa on October 15, 2016 23:32
One simple option is to integrate BDDApron but it is implemented in OCaml so it will add more dependencies to Crab and it would still require changes for supporting Crab domains.
Instead, I prefer to re-implement BDDApron by combining the ADD library (MTBDD) provided by CUDD with the existing Crab domains.
Copied from original issue: caballa/crab#6
caballa commented
We have implemented a reduced product of a numerical domain with a simple flat 3-valued boolean domain (see beb705f). This is less precise that the above described MTBDD-based domain but it is very cheap.
caballa commented
The boxes domain can also reason about Booleans.
caballa commented
We also have boxes so I close for now this issue.