
  * Copyright ( c ) 2009 - 2013 , Monoidics ltd . 
  * Copyright ( c ) Facebook , Inc. and its affiliates . 
  * 
  * This source code is licensed under the MIT license found in the 
  * LICENSE file in the root directory of this source tree . 
 
 * Copyright (c) 2009-2013, Monoidics ltd.
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd

(** Implementation of Abstraction Functions *)

(** Abstraction rules discovered *)
type rules

val abstract : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Abstract a proposition. *)

val abstract_spec :
  Procname.t -> Tenv.t -> Prop.normal BiabductionSummary.spec -> BiabductionSummary.NormSpec.t
* Normalizes names and applies simplifications , soem of which require looking at both pre and 
     post .
    post. *)

val abstract_junk : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the
    junk, otherwise raise a Leak exception. *)

val abstract_no_symop : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
* Abstract a proposition but do n't pay a SymOp

val get_current_rules : unit -> rules
(** Get the current rules discoveres *)

val lifted_abstract : Procname.t -> Tenv.t -> Propset.t -> Propset.t
(** Abstract each proposition in [propset] *)

val remove_redundant_array_elements :
  Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Remove redundant elements in an array, and check for junk afterwards *)

val reset_current_rules : unit -> unit
(** Reset the abstraction rules discovered *)

val set_current_rules : rules -> unit
(** Set the current rules discovered *)

* Implementation of Abstraction Functions 
* Abstraction rules discovered 
* Abstract a proposition. 
* Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the
    junk, otherwise raise a Leak exception. 
* Get the current rules discoveres 
* Abstract each proposition in [propset] 
* Remove redundant elements in an array, and check for junk afterwards 
* Reset the abstraction rules discovered 
* Set the current rules discovered 

  * Copyright ( c ) 2009 - 2013 , Monoidics ltd . 
  * Copyright ( c ) Facebook , Inc. and its affiliates . 
  * 
  * This source code is licensed under the MIT license found in the 
  * LICENSE file in the root directory of this source tree . 
 
 * Copyright (c) 2009-2013, Monoidics ltd.
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd


type rules

val abstract : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t

val abstract_spec :
  Procname.t -> Tenv.t -> Prop.normal BiabductionSummary.spec -> BiabductionSummary.NormSpec.t
* Normalizes names and applies simplifications , soem of which require looking at both pre and 
     post .
    post. *)

val abstract_junk : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t

val abstract_no_symop : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
* Abstract a proposition but do n't pay a SymOp

val get_current_rules : unit -> rules

val lifted_abstract : Procname.t -> Tenv.t -> Propset.t -> Propset.t

val remove_redundant_array_elements :
  Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t

val reset_current_rules : unit -> unit

val set_current_rules : rules -> unit
