Module `Logtk.Rat_lit`Source

Arithmetic Rational Literal

Atomic formulas for linear rational arithmetic. Similar to Int_lit.

Sourcetype term = Term.t

Type Decls

Sourcetype op =

| Equal
| Less

Sourcetype t = private {

op : op;
left : Q.t Monome.t;
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 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 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, 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

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 ->
  ?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

package logtk

Module Logtk.Rat_litSource

Arithmetic Rational Literal

Type Decls

Basics

Operators

Iterators

Focus on a Term

Module `Logtk.Rat_lit`Source