Module Logtk.Int_litSource

Arithmetic Integer Literal

A literal for linear integer arithmetic.

Care has been taken to normalize such literals. Some things are not stable by substitution (e.g. positions in int literals) and therefore there are functions such as apply_subst_no_simp that preserve positions.

Sourcetype term = Term.t

Type Decls

Sourcetype op =
  1. | Equal
  2. | Different
  3. | Less
  4. | Lesseq
Sourcetype 'm divides = {
  1. num : Z.t;
  2. power : int;
  3. monome : 'm;
  4. sign : bool;
}

num^power divides monome or not.

Sourcetype t = private
  1. | Binary of op * Z.t Monome.t * Z.t Monome.t
  2. | Divides of Z.t Monome.t divides
    (*

    Arithmetic literal (on integers)

    *)
Sourcetype lit = t

Basics

Sourceval equal_com : t -> t -> bool
Sourceval compare : t -> t -> int
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval make : op -> Z.t Monome.t -> Z.t Monome.t -> t
Sourceval make_no_simp : op -> Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_eq : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_neq : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_less : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_lesseq : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_divides : ?sign:bool -> Z.t -> power:int -> Z.t Monome.t -> t
Sourceval mk_not_divides : Z.t -> power:int -> Z.t Monome.t -> t
Sourceval negate : t -> t
Sourceval sign : t -> bool
Sourceval polarity : t -> bool

Used for the literal ordering

Sourceval is_pos : t -> bool
Sourceval is_neg : t -> bool
Sourceval is_eq : t -> bool
Sourceval is_neq : t -> bool
Sourceval is_eqn : t -> bool

= or !=

Sourceval is_ineq : t -> bool

< or <=

Sourceval is_less : t -> bool
Sourceval is_lesseq : t -> bool
Sourceval is_divides : t -> bool
Sourceval to_string : t -> string

Operators

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

functor

Sourcetype ('subst, 'a) unif = subst:'subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t
Sourceval generic_unif : ('subst, Z.t Monome.t) unif -> ('subst, t) unif

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

Sourceval apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
Sourceval 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.

Sourceval matching : ?subst:Subst.t -> t Scoped.t -> t Scoped.t -> Subst.t Iter.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.

Sourceval variant : ?subst:Subst.t -> t Scoped.t -> t Scoped.t -> Subst.t Iter.t
Sourceval subsumes : ?subst:Subst.t -> t Scoped.t -> t Scoped.t -> Subst.t Iter.t

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

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

Maximal terms of the literal

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

Conversion into a simple literal

Iterators

Sourcemodule Seq : sig ... end

Focus on a Term

Sourcemodule Focus : sig ... end
Sourcemodule Util : sig ... end