Module Logtk.Rat_litSource

Arithmetic Rational Literal

Atomic formulas for linear rational arithmetic. Similar to Int_lit.

Sourcetype term = Term.t

Type Decls

Sourcetype op =
  1. | Equal
  2. | Less
Sourcetype t = private {
  1. op : op;
  2. left : Q.t Monome.t;
  3. right : Q.t Monome.t;
}

Arithmetic literal (on rationals)

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 -> Q.t Monome.t -> Q.t Monome.t -> t
Sourceval make_no_simp : op -> Q.t Monome.t -> Q.t Monome.t -> t
Sourceval mk_eq : Q.t Monome.t -> Q.t Monome.t -> t
Sourceval mk_less : Q.t Monome.t -> Q.t Monome.t -> t
Sourceval is_eq : t -> bool
Sourceval is_less : t -> bool
Sourceval to_term : t -> term

Back to terms (for negation)

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, Q.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 -> ?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