Reduction (gillian.Engine.Reduction)

exception ReductionException of Gillian.Gil_syntax.Expr.t * string

ReductionException (e, msg) denotes an exception raised due to an expression e being malformed with explanation msg

val resolve_expr_to_location : 
  Symbolic.Pure_context.t ->
  Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t ->
  string option

resolve_to_location pfs e attempts to resolve the expression denoted by e to a location given the pure formulae pfs. If successful, it returns that location, together with any bindings learned during the resolution.

val get_equal_expressions : 
  Symbolic.Pure_context.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t list

get_equal_expressions pfs e returns a list of expressions that equal e under the pure formulae pfs.

val understand_lstcat : 
  Symbolic.Pure_context.t ->
  Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t list ->
  Gillian.Gil_syntax.Expr.t list ->
  (Gillian.Gil_syntax.Formula.t * Utils.Containers.SS.t) option

val reduce_lexpr : 
  ?matching:bool ->
  ?reduce_lvars:bool ->
  ?pfs:Symbolic.Pure_context.t ->
  ?gamma:Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t

reduce_lexpr ?matching ?reduce_lvars ?pfs ?gamma e reduces the expression e given (optional) pure formulae pfs and typing environment gamma. The reduce_lvars and matching flags should not be used by Gillian instantiation developers.

val reduce_formula : 
  ?matching:bool ->
  ?rpfs:bool ->
  ?time:string ->
  ?pfs:Symbolic.Pure_context.t ->
  ?gamma:Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Formula.t ->
  Gillian.Gil_syntax.Formula.t

reduce_formula ?matching ?pfs ?gamma pf reduces the formula pf given (optional) pure formulae pfs and typing environment gamma. The matching flag should not be used by Gillian instantiation developers.

val reduce_assertion : 
  ?matching:bool ->
  ?pfs:Symbolic.Pure_context.t ->
  ?gamma:Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Asrt.t ->
  Gillian.Gil_syntax.Asrt.t

reduce_assertion ?matching ?pfs ?gamma a reduces the assertion a given (optional) pure formulae pfs and typing environment gamma. The matching flag should not be used by Gillian instantiation developers.

val is_tautology : 
  ?pfs:Symbolic.Pure_context.t ->
  ?gamma:Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Formula.t ->
  bool