Smt (gillian.Smt)

exception SMT_unknown

val exec_sat : 
  Gil_syntax.Formula.Set.t ->
  (string, Gillian.Gil_syntax.Type.t) Utils.Prelude.Hashtbl.t ->
  Sexplib.Sexp.t option

val is_sat : 
  Gil_syntax.Formula.Set.t ->
  (string, Gillian.Gil_syntax.Type.t) Utils.Prelude.Hashtbl.t ->
  bool

val check_sat : 
  Gil_syntax.Formula.Set.t ->
  (string, Gillian.Gil_syntax.Type.t) Utils.Prelude.Hashtbl.t ->
  Sexplib.Sexp.t option

val lift_model : 
  Sexplib.Sexp.t ->
  (string, Gillian.Gil_syntax.Type.t) Utils.Prelude.Hashtbl.t ->
  (string -> Gillian.Gil_syntax.Expr.t -> unit) ->
  Gil_syntax.Expr.Set.t ->
  unit

val pp_sexp : Sexplib.Sexp.t Fmt.t