Engine.FOSolverval check_satisfiability_with_model :
Gillian.Gil_syntax.Formula.t list ->
Symbolic.Type_env.t ->
Gillian.Symbolic.Subst.t optioncheck_satisfiability_with_model pfs gamma checks whether or not the pure formulae pfs are satisfiable under the typing environment gamma. If this is the case, the function returns the appropriate logical environment.
val check_satisfiability :
?matching:bool ->
?time:string ->
?relevant_info:
(Utils.Containers.SS.t * Utils.Containers.SS.t * Utils.Containers.SS.t) ->
Gillian.Gil_syntax.Formula.t list ->
Symbolic.Type_env.t ->
boolcheck_satisfiability ?matching pfs gamma checks whether or not the pure formulae pfs are satisfiable under the typing environment gamma. The matching flag should not be used by Gillian instantiation developers.
val sat :
matching:bool ->
pfs:Symbolic.Pure_context.t ->
gamma:Symbolic.Type_env.t ->
Gillian.Gil_syntax.Formula.t ->
boolA different API for check_satisfiability better adapted for usage in memory models
val check_entailment :
?matching:bool ->
Utils.Containers.SS.t ->
Symbolic.Pure_context.t ->
Gillian.Gil_syntax.Formula.t list ->
Symbolic.Type_env.t ->
boolcheck_entailment existentials lpfs rpfs gamma checks whether or not the entailment << ∃ existentials. lpfs => rpfs >> holds under the typing environment gamma.
val is_equal :
pfs:Symbolic.Pure_context.t ->
gamma:Symbolic.Type_env.t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t ->
boolis_equal e1 e2 pfs gamma checks whether or not << pfs, gamma |- e1 = e2 >>.
val is_different :
pfs:Symbolic.Pure_context.t ->
gamma:Symbolic.Type_env.t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t ->
boolis_different e1 e2 pfs gamma checks whether or not << pfs, gamma |- e1 <> e2 >>.
val num_is_less_or_equal :
pfs:Symbolic.Pure_context.t ->
gamma:Symbolic.Type_env.t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t ->
boolval resolve_loc_name :
pfs:Symbolic.Pure_context.t ->
gamma:Symbolic.Type_env.t ->
Gillian.Gil_syntax.Expr.t ->
string option