Module LogtkRewriting.FormRW

module FormRW: sig .. end

type t 
type form = LogtkFormula.FO.t 
type rule = LogtkFOTerm.t * form 
rewrite rule, from left to right
val empty : unit -> t
val add : t ->
rule -> t
val add_seq : t ->
rule Sequence.t -> t
val add_list : t ->
rule list -> t
val add_term_rule : t ->
LogtkFOTerm.t * LogtkFOTerm.t -> t
val add_term_rules : t ->
(LogtkFOTerm.t * LogtkFOTerm.t) list -> t
val to_seq : t -> rule Sequence.t
val of_seq : rule Sequence.t -> t
val of_list : rule list -> t
val size : t -> int
val iter : t -> (rule -> unit) -> unit
val rule_to_form : rule -> form
Convert the rule back to a term
val rewrite_collect : t ->
form ->
form * rule list
Compute normal form of the formula, and return it together with the list of rules that were used to rewrite.
val rewrite : t ->
form -> form
see LogtkRewriting.FormRW.rewrite_collect