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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct