Module Logtk.Rat_lit

Arithmetic Rational Literal

type term = Term.t

Type Decls

type op =
| Equal
| Less
type t = private {
op : op;
left : Q.t Monome.t;
right : Q.t Monome.t;
}

Arithmetic literal (on rationals)

type lit = t

Basics

val equal_com : t -> t -> bool
val compare : t -> t -> int
include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
val make : op -> Q.t Monome.t -> Q.t Monome.t -> t
val mk_eq : Q.t Monome.t -> Q.t Monome.t -> t
val mk_less : Q.t Monome.t -> Q.t Monome.t -> t
val is_eq : t -> bool
val is_less : t -> bool
val to_term : t -> term

Back to terms (for negation)

val pp : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val to_string : t -> string

Operators

val fold : ('a -> term -> 'a) -> 'a -> t -> 'a
val map : (term -> term) -> t -> t

functor

type ('subst, 'a) unif = subst:'subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Sequence.t
val generic_unif : ('subst, Q.t Monome.t) unif -> ('subst, t) unif

Generic unification/matching/variant, given such an operation on monomes

val apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
val apply_subst_no_simp : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t

Same as apply_subst but takes care B NOT simplifying the literal. In practice, mostly useful for comparison purpose.

val matching : ?⁠subst:Subst.t -> t Scoped.t -> t Scoped.t -> Subst.t Sequence.t

checks whether subst(lit_a) is equal to lit_b. Returns alternative substitutions s such that s(lit_a) = lit_b and s contains subst.

val variant : ?⁠subst:Subst.t -> t Scoped.t -> t Scoped.t -> Subst.t Sequence.t
val unify : ?⁠subst:Unif_subst.t -> t Scoped.t -> t Scoped.t -> Unif_subst.t Sequence.t
val subsumes : ?⁠subst:Subst.t -> t Scoped.t -> t Scoped.t -> Subst.t Sequence.t

Find substitutions such that subst(lit_a) implies lit_b. This is more general than matching.

val are_variant : t -> t -> bool
val is_trivial : t -> bool
val is_absurd : t -> bool
val fold_terms : ?⁠pos:Position.t -> ?⁠vars:bool -> ?⁠ty_args:bool -> which:[< `Max | `All ] -> ord:Ordering.t -> subterms:bool -> t -> (term * Position.t) Sequence.t
val max_terms : ord:Ordering.t -> t -> term list

Maximal terms of the literal

val to_form : t -> Term.t SLiteral.t

Conversion into a simple literal

Iterators

module Seq : sig ... end

Focus on a Term

module Focus : sig ... end