4 ms·
I've only seriously examined the source of Z3, but encoding an SMT problem to multiple SAT instances remains a feature there - just convert any qf_bv problem in
by ZephyrP 9y ago
I've only seriously examined the source of Z3, but encoding an SMT problem to multiple SAT instances remains a feature there - just convert any qf_bv problem into bit width * SAT instances / 2!
I recall that many popular simplifications required a problem to be expressible as CNF.
(I also seem to recall there is some strategy to simplify logics over Reals/Ints into BV without encoding logical "bignum circuitry" as well?)
- wsxcde 9y ago> but encoding an SMT problem to multiple SAT instances remains a feature there Sure. I'm not arguing that bitblasting should never be done, it's probably still the best way of solving bitvector problems. My point is that the pedagogical objective of an toy SMT solver is lost if doesn't teach DPLL(T) and only focuses on bitblasting.