sig
val section : Libzipperposition.Util.Section.t
type rule_term
val rhs_term : Rewrite_rule.rule_term -> Libzipperposition.FOTerm.t
val pp_rule_term : Rewrite_rule.rule_term CCFormat.printer
type rule_clause
val rhs_clause : Rewrite_rule.rule_clause -> Literal.t list list
val pp_rule_clause : Rewrite_rule.rule_clause CCFormat.printer
module Set :
sig
type t
val empty : Rewrite_rule.Set.t
val is_empty : Rewrite_rule.Set.t -> bool
val add_stmt :
Libzipperposition.Statement.clause_t ->
Rewrite_rule.Set.t -> Rewrite_rule.Set.t
val pp : Rewrite_rule.Set.t CCFormat.printer
end
val normalize_term :
Rewrite_rule.Set.t ->
Libzipperposition.FOTerm.t -> Libzipperposition.FOTerm.t
val narrow_term :
?subst:Libzipperposition.Substs.t ->
Rewrite_rule.Set.t Libzipperposition.Scoped.t ->
Libzipperposition.FOTerm.t Libzipperposition.Scoped.t ->
(Rewrite_rule.rule_term * Libzipperposition.Substs.t) Sequence.t
val normalize_clause :
Rewrite_rule.Set.t -> Literal.t list -> Literal.t list list option
val narrow_lit :
?subst:Libzipperposition.Substs.t ->
Rewrite_rule.Set.t Libzipperposition.Scoped.t ->
Literal.t Libzipperposition.Scoped.t ->
(Rewrite_rule.rule_clause * Libzipperposition.Substs.t) Sequence.t
end