Module SMTExpr

module SMTExpr: sig .. end
Datatypes and helper function for the SMT solver interface
Author(s): 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