package touist

  1. Overview
  2. Docs
The solver for the Touist language

Install

Dune Dependency

Authors

Maintainers

Sources

v3.5.0.tar.gz
sha256=859a4428ced26ed38615a606138c02ec63541cd34cf94a37b3e35d5bf46d40c4
md5=c09dd1cda8aff444889d1374636c810b

doc/touist.yices2/Touist_yices2/SmtSolve/index.html

Module Touist_yices2.SmtSolveSource

Requires yices2 Process an evaluated AST in order to solve it with Yices2.

Sourceval ast_to_yices : Touist.Types.AstSet.elt -> 'term * (string, 'term) Hashtbl.t
Sourceval string_of_model : ?value_sep:string -> (string, 'term) Hashtbl.t -> 'model -> string

Turn a model into a string.

Sourceval solve : string -> 'term -> 'model option

solve logic form solves the Yices2 formula form. logic can be "QF_LIA", "QF_LRA"...

Sourceval logic_supported : string -> bool

Tell if this logic string (e.g., QF_LIA) is supported by Yices2.

Sourceval enabled : bool

Is this library enabled? (requires yices2 to be installed)

OCaml

Innovation. Community. Security.