DolmenIntf (docs.other.smtml.Smtml.Dolmenexpr_to

module ConstMap : Smtml_prelude.Map.S with type key = DExpr.term_cst

type ty = DTy.t

type term = DTerm.t

type interp = DM.Value.t

type model = interp ConstMap.t

type func_decl = DTerm.Const.t

val true_ : term

val false_ : term

val int : int -> term

val real : float -> term

val const : string -> ty -> term

val not_ : term -> term

val and_ : term -> term -> term

val or_ : term -> term -> term

val logand : term list -> term

val logor : term list -> term

val xor : term -> term -> term

val implies : term -> term -> term

val eq : term -> term -> term

val distinct : term list -> term

val ite : term -> term -> term -> term

val forall : term list -> term -> term

val exists : term list -> term -> term

module Types : sig ... end

module Interp : sig ... end

module Int : sig ... end

module Real : sig ... end

module String : sig ... end

module Re : sig ... end

module Bitv : sig ... end

module Float : sig ... end

module Adt : sig ... end

module Func : sig ... end

module Model : sig ... end

module Smtlib : sig ... end