PV4 ⊧ Yicesproduces a satisfiability result for a formula

Application domain/field

• SMT solving
• SMT (Satisfiability Modulo Theories)

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB(version 1.2 and 2.0), or its own specification language. It also has a C API and bindings for Java, Python, Go and OCaml.

Expected output

sat if the problem is satisfiable, unsat if it is not satisfiable or unknown if the solver does not terminate within a fixed number of iterations. If the formula can be satisfied, then you can ask Yices for a satisfying model.

Comments

License: GPLv3