Previous  Up  Next

Module ArithLit

module ArithLit: sig .. end

Arithmetic Literal


type term = Libzipperposition.FOTerm.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 : t -> t -> bool
val equal_com : t -> t -> bool
val compare : t -> t -> int
include Interfaces.HASH
val make : 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
val is_ineq : t -> bool
< or <=
val is_less : t -> bool
val is_lesseq : t -> bool
val is_divides : t -> bool
val pp : t CCFormat.printer
val pp_tstp : 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 'a unif = subst:Libzipperposition.Substs.t ->
       'a Libzipperposition.Scoped.t ->
       'a Libzipperposition.Scoped.t -> Libzipperposition.Substs.t Sequence.t 
val generic_unif : Z.t Monome.t unif -> t unif
Generic unification/matching/variant, given such an operation on monomes
val apply_subst : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t
val apply_subst_no_renaming : Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t
val apply_subst_no_simp : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t
Same as ArithLit.apply_subst but takes care simplifying the literal. In practice, mostly useful for comparison purpose.
val matching : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t ->
       Libzipperposition.Substs.t Sequence.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:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t ->
       Libzipperposition.Substs.t Sequence.t
val unify : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t ->
       Libzipperposition.Substs.t Sequence.t
val subsumes : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t ->
       Libzipperposition.Substs.t Sequence.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:Libzipperposition.Position.t ->
       ?vars:bool ->
       ?ty_args:bool ->
       which:[< `All | `Max ] ->
       ord:Libzipperposition.Ordering.t ->
       subterms:bool ->
       t -> (term * Libzipperposition.Position.t) Sequence.t
val max_terms : ord:Libzipperposition.Ordering.t -> t -> term list
Maximal terms of the literal
val to_form : t -> Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t
Conversion into a simple literal

Iterators


module Seq: sig .. end

Focus on a Term


module Focus: sig .. end
module Util: sig .. end
Some Utils for arith