Module Rewrite_rule

module Rewrite_rule: sig .. end

Rewrite Rules

val section : Libzipperposition.Util.Section.t

type rule_term

val rhs_term : rule_term -> Libzipperposition.FOTerm.t

val pp_rule_term : rule_term CCFormat.printer

type rule_clause

val rhs_clause : rule_clause -> Literal.t list list

val pp_rule_clause : rule_clause CCFormat.printer

module Set: sig .. end

Set of Rewrite Rules

val normalize_term : Set.t ->
       Libzipperposition.FOTerm.t -> Libzipperposition.FOTerm.t

normalize rules t computes the normal form of t w.r.t the set of rewrite rules

val narrow_term : ?subst:Libzipperposition.Substs.t ->
       Set.t Libzipperposition.Scoped.t ->
       Libzipperposition.FOTerm.t Libzipperposition.Scoped.t ->
       (rule_term * Libzipperposition.Substs.t) Sequence.t

narrow_term rules t finds the set of rules (l --> r) in rules and substitutions sigma such that sigma(l) = sigma(t)

val normalize_clause : Set.t -> Literal.t list -> Literal.t list list option

normalize literals of the clause w.r.t. rules, or return None if no rule applies

val narrow_lit : ?subst:Libzipperposition.Substs.t ->
       Set.t Libzipperposition.Scoped.t ->
       Literal.t Libzipperposition.Scoped.t ->
       (rule_clause * Libzipperposition.Substs.t) Sequence.t

narrow_term rules lit finds the set of rules (l --> clauses) in rules and substitutions sigma such that sigma(l) = sigma(tit)