Module Logtk.RewriteSource

Rewriting on Terms and Literals

Rewriting is a (relatively) efficient way of computing on terms and literals using rules that come from the input. Each rule is a pair lhs, rhs (left-hand side, right-hand side) that means that objects matching lhs should be rewritten into rhs.

For term rules, lhs and rhs are both terms (with vars rhs ⊆ vars lhs).

For literal rules, lhs is an atomic literal, and rhs is a list of clauses.

This is used for Deduction Modulo in the prover.

Sourcetype term = Term.t
Sourcetype defined_cst

Payload of a defined function symbol or type

Sourcetype proof = Proof.step
Sourceval section : Util.Section.t
Sourcemodule Term : sig ... end

Rewriting on Literals and Clauses

Sourcemodule Lit : sig ... end

Rules in General

Sourcetype rule =
  1. | T_rule of Term.rule
  2. | L_rule of Lit.rule
Sourcemodule Rule : sig ... end
Sourcemodule Rule_set : CCSet.S with type elt = rule
Sourcetype rule_set = Rule_set.t

Defined Constant

A constant that is defined by at least one rewrite rule

Sourcemodule Defined_cst : sig ... end
Sourceval as_defined_cst : ID.t -> defined_cst option
Sourceval is_defined_cst : ID.t -> bool
Sourceval all_rules : Rule.t Iter.t