package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Arithmetic Rational Literal

Atomic formulas for linear rational arithmetic. Similar to Int_lit.

type term = Term.t

Type Decls

type op =
  1. | Equal
  2. | Less
type t = private {
  1. op : op;
  2. left : Q.t Monome.t;
  3. 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 with type t := t
val equal : t -> t -> bool
val hash : t -> int
val make : op -> Q.t Monome.t -> Q.t Monome.t -> t
val make_no_simp : 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_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, 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 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