Module type Can.T
module type T = sig end
A
canonizable and ground confluent theory
th is specified
by means of a
- replacement
map f a for replacing uninterpreted
subterms of a with f a and canonizing the result,
- a theory-specific canonizer;
- chainings functions
of_var_equal, of_var_diseq, of_var_diseq
for keeping equality sets ground confluent by triggering inference rules
on pure equalities, variable equalities, and variable disequalities, respectively; and
- a branching function
disjunction.
val th : Th.t
val map : (Term.t -> Term.t) -> Term.t -> Term.t
val sigma : Sym.t -> Term.t list -> Term.t
val of_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
val of_var_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
val of_var_diseq : Fact.Diseq.t -> Can.config -> Fact.Equal.t list
val disjunction : Can.config -> Clause.t