Module Logtk.Int_lit

Arithmetic Integer Literal

type term = Term.t

Type Decls

type op =
| Equal
| Different
| Less
| Lesseq
type 'm divides = {
num : Z.t;
power : int;
monome : 'm;
sign : bool;
}

num^power divides monome or not.

type t = private
| Binary of op * Z.t Monome.t * Z.t Monome.t
| Divides of Z.t Monome.t divides

Arithmetic literal (on integers)

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 -> Z.t Monome.t -> Z.t Monome.t -> t
val make_no_simp : op -> Z.t Monome.t -> Z.t Monome.t -> t
val mk_eq : Z.t Monome.t -> Z.t Monome.t -> t
val mk_neq : Z.t Monome.t -> Z.t Monome.t -> t
val mk_less : Z.t Monome.t -> Z.t Monome.t -> t
val mk_lesseq : Z.t Monome.t -> Z.t Monome.t -> t
val mk_divides : ?⁠sign:bool -> Z.t -> power:int -> Z.t Monome.t -> t
val mk_not_divides : Z.t -> power:int -> Z.t Monome.t -> t
val negate : t -> t
val sign : t -> bool
val polarity : t -> bool

Used for the literal ordering

val is_pos : t -> bool

Used for the literal ordering

val is_neg : t -> bool
val is_eq : t -> bool
val is_neq : t -> bool
val is_eqn : t -> bool
val is_ineq : t -> bool

< or <=

val is_less : t -> bool

< or <=

val is_lesseq : t -> bool
val is_divides : t -> bool
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, Z.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
module Util : sig ... end