LogicPreprocessing (gillian.Engine.LogicPreprocessing)

module L = Logging

val unfolded_preds : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t

val auto_unfold : 
  ?unfold_rec_predicates:bool ->
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  Gillian.Gil_syntax.Asrt.t ->
  Gillian.Gil_syntax.Asrt.t list

val find_recursive_preds : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t

val simplify_and_prune : Gillian.Gil_syntax.Pred.t -> Gillian.Gil_syntax.Pred.t

val find_pure_preds : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t

val unfold_preds : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t
  * (string, bool) Utils.Prelude.Hashtbl.t

val unfold_spec : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  Gillian.Gil_syntax.Spec.t ->
  Gillian.Gil_syntax.Spec.t

val unfold_lemma : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  Gillian.Gil_syntax.Lemma.t ->
  Gillian.Gil_syntax.Lemma.t

val unfold_bispec : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  Gillian.Gil_syntax.BiSpec.t ->
  Gillian.Gil_syntax.BiSpec.t

val remove_equalities_between_binders_and_lvars : 
  Stdlib.String.t list ->
  Gillian.Gil_syntax.Asrt.t ->
  Gillian.Gil_syntax.Asrt.t

val unfold_cmd : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  int Gillian.Gil_syntax.Cmd.t ->
  int Gillian.Gil_syntax.Cmd.t

val unfold_proc : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  ('a, int) Gillian.Gil_syntax.Proc.t ->
  ('a, int) Gillian.Gil_syntax.Proc.t

val explicit_param_types : 
  (string, ('a, int) Gillian.Gil_syntax.Proc.t) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Lemma.t) Utils.Prelude.Hashtbl.t ->
  (string, ('a, int) Gillian.Gil_syntax.Proc.t) Utils.Prelude.Hashtbl.t
  * (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t
  * (string, Gillian.Gil_syntax.Lemma.t) Utils.Prelude.Hashtbl.t

val unfold_procs : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  (string, ('a, int) Gillian.Gil_syntax.Proc.t) Utils.Prelude.Hashtbl.t ->
  (string, ('a, int) Gillian.Gil_syntax.Proc.t) Utils.Prelude.Hashtbl.t

val unfold_specs : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Spec.t) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Spec.t) Utils.Prelude.Hashtbl.t

val unfold_lemmas : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Lemma.t) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.Lemma.t) Utils.Prelude.Hashtbl.t

val unfold_bispecs : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  (string, bool) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.BiSpec.t) Utils.Prelude.Hashtbl.t ->
  (string, Gillian.Gil_syntax.BiSpec.t) Utils.Prelude.Hashtbl.t

val add_closing_tokens : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  unit

val preprocess : 
  ('a, int) Gillian.Gil_syntax.Prog.t ->
  bool ->
  ('a, int) Gillian.Gil_syntax.Prog.t