Module SMTExpr

Datatypes and helper function for the SMT solver interface

Sorts

type sort = Type.t

An SMT sort is of type Type.t

type t = Term.t

An SMT expression is of type Term.t

type var = Var.t

An SMT variable is of type Var.t

type custom_arg =
  1. | ArgString of string
    (*

    String argument

    *)
  2. | ArgExpr of t
    (*

    Expression argument

    *)
  3. | ArgList of custom_arg list

Arguments to a custom command

Pretty-printing and String Conversions

module type Conv = sig ... end