dreal3
dreal3 copied to clipboard
dreal
There is a new version of dReal, available at https://github.com/dreal/dreal4
Starting from a simple case, i.e., ones with constant RHSs.
We've been working on contractors which manipulate overapproximations. In principle they are most needed for proving UNSAT. To get faster SAT answers we should start using underapproximations. Let's tentatively call...
> "Another thing that we need to re-implement in dReal3 is the ordering of ODE pruning operators. For now, it always applies forward ODE pruning first and then backward ODE...
@soonhokong @scungao : Here is a very rough outline of the enhancements I would like for the API. The following is psuedo-code to describe my intent, but there may be...
There can be many use cases for this one. For now, @nnarodytska and I are thinking about using it to enhance theory propagation.
From `void prune(box & b, ...)` to `void prune(box & b, ..., vector & bin)` This extension allows a pruning operator to return a set of boxes. - It can...