This PR adds initial support to Boolector for the Kissat SAT Solver.
Importantly: Kissat does not yet support incremental solving, which therefore limits its usability inside of Boolector (maybe only QF_BV can be solved?).
Given the lack of incremental solving, I would expect some tests that fail. ctest reports the following:
73% tests passed, 251 tests failed out of 943
when compiled with --only-kissat.
There's one place (in btormbt.c) where I have not added BTOR_USE_KISSAT because of this lack of incremental support as well. This is intentional rather than "missing a spot".
aytey
commented
4 years ago
This PR adds initial support to Boolector for the Kissat SAT Solver.
Importantly: Kissat does not yet support incremental solving, which therefore limits its usability inside of Boolector (maybe only QF_BV can be solved?).
Given the lack of incremental solving, I would expect some tests that fail.
ctestreports the following:when compiled with
--only-kissat.There's one place (in
btormbt.c) where I have not addedBTOR_USE_KISSATbecause of this lack of incremental support as well. This is intentional rather than "missing a spot".Signed-off-by: Andrew V. Jones andrew.jones@vector.com