Simon Cruanes cbc9c5ac6f refactor(smt): preprocessing is now using a queue of delayed actions ... - preprocessing doesn't simplify anymore, it assumes terms are already simplified. It only adds clauses/adds literals, it does not return new terms. - adding clauses/literals to SAT is done as delayed actions, to avoid issues of reentrancy. These actions are performed after preprocessing, in a loop that has access to the SAT solver.		2022-02-04 16:08:01 -05:00
..
dune	wip: feat(LIA): LIA solver, will rely on LRA solver	2022-01-11 14:00:04 -05:00
sidekick_base_solver.ml	refactor(smt): preprocessing is now using a queue of delayed actions	2022-02-04 16:08:01 -05:00