batsat
batsat copied to clipboard
c-cube
A (parametrized) Rust SAT solver originally based on MiniSat
This allows theories to produce different explanations in `analyze`, and `analyze_final`. For example, if a theory knows `(a && b) => c` and `c => d` and is asked to...
Previously `batsat` panicked when `Theory::raise_conflict` was called with an empty clause, but I think it would make sense for the solver to just immediately return `unsat`
This makes literal picking somewhat more predictable and robust to the order explanations are given by theories (see https://github.com/dewert99/bat_egg_smt/pull/14). Unfortunately it seems this also makes maintaining the order heap more...
Gives raw access to `solver.v.assumptions` and allows where variables are available for decisions to be changed after they are created, as an alternative to #17? Doing this allows the rest...
As I thinking about `batsat`s non-chronological backtracking with theory propagation I started wondering what requirements the theory propagation had, eg. "a theories explanation of a propagated literal must contain a...