Stack refers to push/pop (of constraints). Kodkod already has incremental adding of constraints; this is what #7 is about.
This task is about incremental removal of constraints. Z3 has this functionality, and through experiments, it seems to be much faster.
So we should either get Z3 to work with Kodkod or mimic its functionality with the other SAT solvers.
Note that Z3 has some unstable Java bindings. Also, Z3 requires a license for commercial use, so this might be an issue if people want to use Moolloy for other purposes.
Stack refers to push/pop (of constraints). Kodkod already has incremental adding of constraints; this is what #7 is about.
This task is about incremental removal of constraints. Z3 has this functionality, and through experiments, it seems to be much faster.
So we should either get Z3 to work with Kodkod or mimic its functionality with the other SAT solvers.
Note that Z3 has some unstable Java bindings. Also, Z3 requires a license for commercial use, so this might be an issue if people want to use Moolloy for other purposes.
Dependencies: #23