Module `SMTExpr`

Datatypes and helper function for the SMT solver interface

author: Alain Mebsout, Christoph Sticksel

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 = | ArgString of string String argument | ArgExpr of t Expression argument: Arguments to a custom command

Pretty-printing and String Conversions

module type Conv = sig ... end

module Converter : functor (D : SolverDriver.S) -> Conv