Make (gillian.Engine.Normaliser.Make)

Parameters

module SPState : PState.S

Signature

val normalise_assertion : 
  pred_defs:MP.preds_tbl_t ->
  init_data:SPState.init_data ->
  ?pvars:Utils.Containers.SS.t ->
  Gillian.Gil_syntax.Asrt.t ->
  ((SPState.t * Gillian.Symbolic.Subst.t) list, string) Stdlib.result

normalise_assertion ?pred_defs ?gamma ?pvars a normalises the assertion a starting from the typing environment gamma considering the predicate table pred_defs and program variables pvars. It returns the appropriate predicate state and all learned bindings.