PV4 ⊧ Yicesproduces a satisfiability result for a formula
- SMT solving
- SMT (Satisfiability Modulo Theories)
Type of toolSMT solver
Expected inputSMT 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.
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.