Monadic.FOSolver
module FOSolver = Engine.FOSolver
module PFS = Engine.PFS
module Type_env = Engine.Type_env
module Reduction = Engine.Reduction
module Formula = Gillian.Gil_syntax.Formula
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 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_equal :
pc:Pc.t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t ->
bool
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 reduce_expr :
pc:Pc.t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t
val reduce_formula :
pc:Pc.t ->
Gillian.Gil_syntax.Formula.t ->
Gillian.Gil_syntax.Formula.t
val resolve_type :
pc:Pc.t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Type.t option