Module Monadic.Pc

module Pure_context = Engine.PFS
module Type_env = Engine.Type_env
module FOSolver = Engine.FOSolver
type t = {
  1. pfs : Gillian.Symbolic.Pure_context.t;
  2. gamma : Gillian.Symbolic.Type_env.t;
  3. learned : Gil_syntax.Formula.Set.t;
  4. learned_types : (string * Gillian.Gil_syntax.Type.t) list;
  5. matching : bool;
}
val copy : t -> t
val make : pfs:Gillian.Symbolic.Pure_context.t -> gamma:Gillian.Symbolic.Type_env.t -> matching:bool -> ?learned:Gillian.Gil_syntax.Formula.t list -> ?learned_types:(string * Gillian.Gil_syntax.Type.t) list -> unit -> t
val init : ?matching:bool -> unit -> t
val empty : t
val pfs_to_pfs_and_gamma : Gillian.Gil_syntax.Formula.t list -> Gillian.Gil_syntax.Formula.t list * (string * Gillian.Gil_syntax.Type.t) list
val extend : t -> Gillian.Gil_syntax.Formula.t list -> t
val extend_types : t -> (string * Gillian.Gil_syntax.Type.t) list -> t
val equal : t -> t -> bool
val pp : t Fmt.t
val diff : t -> t -> Gil_syntax.Formula.Set.t * Gil_syntax.Formula.Set.t
val of_gpc : Engine.Gpc.t -> t
val to_gpc : t -> Engine.Gpc.t