module Pure: sig .. end
Operations on pure formulae
type
The type of non-disjunctive pure formulae
val compare : t -> t -> int
Constructors
val ptrue : t
val pfalse : t
val one : Exp.exp -> t
val conj_one : Exp.exp -> t -> t
val conj : t -> t -> t
Tests
val is_true : t -> bool
val is_sat : t -> bool
val is_false : t -> bool
val has_unsat_eq : t -> bool
val has_neql : t -> bool
val identical_eq : t -> t -> bool
If this returns true then pure1.eq == pure2.eq.
Destructors
val to_exp : t -> Exp.exp
val to_sub : t -> Exp.subst
val only_inst_eqs : t -> t
val remove_eqs : t -> t
Free variables / substitutions
val no_s : string -> t -> bool
val fv : t -> Exp.IdSet.t -> Exp.IdSet.t
val exfv : t -> Exp.IdSet.t -> Exp.IdSet.t
val fhd : t -> Exp.IdSet.t -> Exp.IdSet.t
val map : (Exp.exp -> Exp.exp) -> t -> t
val kill_vars : Exp.IdSet.t -> t -> t
Return a weaker assertion that does not mention the killed variables.
val kill_can_return : t -> t
Return a weaker assertion that does not have any can_returns.
Pure prover
val normalize : t -> t list
val normalize_aggr : t -> t list
val entails_exp_aggr : t -> Exp.exp -> bool
entails_exp_aggr pl e returns true if pl |- e.
val entails_exp : t -> Exp.exp -> bool
entails_exp pl e returns true if pl |- e.
val simplify : t -> t -> t
Find a simpler pl3 such that pl1 |- pl3 iff pl1 |- pl2.
val entails : t -> t -> bool
entails pl pl' returns true if pl |- EX exfv(pl'). pl'.
Other operations
val eq_length : t -> int
val fold : (Exp.exp -> 'a -> 'a) -> t -> 'a -> 'a
val filter : (Exp.exp -> bool) -> t -> t
val has_can_return : t -> bool
val common : t -> t -> t
common p1 p2 = p such that p1 => p and p2 => p.
val common3 : t -> t -> t * t * t
val get_set_eqs : t -> (Exp.exp list * Exp.exp list) list
Return the list of equalities between set expressions
in the pure formula.
val get_uneql : Exp.exp -> t -> Exp.Dset.t
Returns the set of expresssions that are not equal to e in pl
val pp : Format.formatter -> t -> unit
Pretty-print a pure assertion
Disjunctive pure assertions
val list_conj : t list -> t list -> t list
val lifted_list_conj : t list -> (unit -> t list) -> t list