OCaml logo

logtk

Core types and algorithms for logic
Overview Documentation
IN THIS PACKAGE
Module Logtk . Int_lit

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.

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 with type t := 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
val is_neg : t -> bool
val is_eq : t -> bool
val is_neq : t -> bool
val is_eqn : t -> bool

= or !=

val is_ineq : t -> bool

< or <=

val is_less : t -> bool
val is_lesseq : t -> bool
val is_divides : t -> bool
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 Iter.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 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.

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

val are_variant : t -> t -> bool
val is_trivial : t -> bool
val is_absurd : t -> bool
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
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