Module SMTExpr

Datatypes and helper function for the SMT solver interface

Alain Mebsout, Christoph Sticksel


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