PV4 ⊧ Barcelogicproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB format

Expected output

If satisfiable, then a model (in SMT-LIB format) which describes the truth value for each Boolean variable, a concrete integer or real for each numeric variable and a partial mapping for each uninterpreted function symbol in the formula Else, unsatisfiable