Some support for exploring a solution space.
Eliminate work Q, recurse directly.
Fix a bug in model creation.
When considering a collection of (say) lower bound, we'd add 1 for
each bound! What we want to do is pick the largest lower bound,
and just add 1 once at the end.
Derive Read instances.
Functions to get back a user name, if possible.
Generate positive names
Change the representation of names to avoid +ve -ve hack
A function to get the possible values for an expression
Compute intervals based on a model
Don't normalize Choice---leads to leaks
Remove other modules from cabal file, and update description
Remove old implementation.
We may want to resurrect this later, as it supports arbitrary nesting
A stand-alone file with the entire solver.
Replace with a .pdf version of the paper.
Make a proper interface
Put things together.
Compute a model for an inert set.
Update bounds DB, when inserting a new constraint.
Clean-up manipulation of lower and upper bounds
Keep upper and lower bounds together.
This should make it easier to extract models
Checkpoint: has syntax errors, fix soon!
Remove DarkGray entries in workQ, split the world instead.
Refactor to eliminate duplication
Add a case to handle adding 0
Fix handling of dark and gray shadows
Comments about computing shadows
Algorithm implemented, compiles but not tested. XXX: add API that pli…
Checkpoint: need to update to deal with lists in the upper and lower …
Finish up equalities.
Checkpoint: start on implementing CVC4's online algorithm.