Module Monadic.FOSolver

module FOSolver = Engine.FOSolver
module PFS = Engine.PFS
module Type_env = Engine.Type_env
module Reduction = Engine.Reduction
module Typing = Engine.Typing
val build_full_pfs : Pc.t -> Gillian.Symbolic.Pure_context.t

FIXME: optimization?

val build_full_gamma : Pc.t -> Gillian.Symbolic.Type_env.t
val sat : pc:Pc.t -> Formula.t -> bool
val check_entailment : pc:Pc.t -> Formula.t -> bool
val of_comp_fun : (pfs:Gillian.Symbolic.Pure_context.t -> gamma:Gillian.Symbolic.Type_env.t -> 'a -> 'b -> 'c) -> pc:Pc.t -> 'a -> 'b -> 'c
val is_different : pc:Pc.t -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> bool
val num_is_less_or_equal : pc:Pc.t -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> bool
val resolve_loc_name : pc:Pc.t -> Gillian.Gil_syntax.Expr.t -> string option
val resolve_type : pc:Pc.t -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Type.t option