PV2 ⊧ CoqQFBVproduces a satisfiability formula for a query

SMT solver for QF_BV (quantifier-free bit-vector) logic.

Application domain/field

• SMT solving
• Quantifier-Free Bit-Vector (QF_BV) logic

Type of tool

SMT solver for QF_BV logic

Expected input

SMT QF_BV query

Format:

SMT-LIB v2

Expected output

Boolean formula such that the query is satisfiable if and only if the Boolean formula is satisfiable. Output is generated in the DIMACS format.

Internals

This is a certified SMT solver for quantifier-free bit-vector (QF_BV) formulas. It has been specified and verified in the proof assistant Coq. It takes a QF_BV query in SMT-LIB format. This is converted into a formal QF_BV expression. Then a CNF formula is constructed. Then it uses Kissat to solve the CNF formula. If the result is unsat with a certificate, then the certificate is verified with GRAT. If the results is sat with assignments, then this is translated back to SMT assignments and the tool will verify whether these assignments satisfy the QF_BV expression.