Module `Logtk.Int_lit`Source

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 =

| Equal
| Different
| Less
| Lesseq

Sourcetype 'm divides = {

num : Z.t;
power : int;
monome : 'm;
sign : bool;

}

num^power divides monome or not.

Sourcetype t = private

| Binary of op * Z.t Monome.t * Z.t Monome.t
| 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 pp : t CCFormat.printer

Sourceval pp_tstp : t CCFormat.printer

Sourceval pp_zf : t CCFormat.printer

Sourceval to_string : t -> string

Operators

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

Sourceval map : (term -> term) -> t -> t

functor

Source

type ('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

Source

val unify : 
  ?subst:Unif_subst.t ->
  t Scoped.t ->
  t Scoped.t ->
  Unif_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

Source

val fold_terms : 
  ?pos:Position.t ->
  ?vars:bool ->
  ?var_args:bool ->
  ?fun_bodies: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

package logtk

Module Logtk.Int_litSource

Arithmetic Integer Literal

Type Decls

Basics

Operators

Iterators

Focus on a Term

Module `Logtk.Int_lit`Source