sig
type t =
Left of ArithLit.op * Z.t Monome.Focus.t * Z.t Monome.t
| Right of ArithLit.op * Z.t Monome.t * Z.t Monome.Focus.t
| Div of Z.t Monome.Focus.t ArithLit.divides
val mk_left :
ArithLit.op -> Z.t Monome.Focus.t -> Z.t Monome.t -> ArithLit.Focus.t
val mk_right :
ArithLit.op -> Z.t Monome.t -> Z.t Monome.Focus.t -> ArithLit.Focus.t
val mk_div :
?sign:bool -> Z.t -> power:int -> Z.t Monome.Focus.t -> ArithLit.Focus.t
val get :
ArithLit.lit -> Libzipperposition.Position.t -> ArithLit.Focus.t option
val get_exn :
ArithLit.lit -> Libzipperposition.Position.t -> ArithLit.Focus.t
val focus_term : ArithLit.lit -> ArithLit.term -> ArithLit.Focus.t option
val focus_term_exn : ArithLit.lit -> ArithLit.term -> ArithLit.Focus.t
val replace : ArithLit.Focus.t -> Z.t Monome.t -> ArithLit.lit
val term : ArithLit.Focus.t -> ArithLit.term
val focused_monome : ArithLit.Focus.t -> Z.t Monome.Focus.t
val opposite_monome : ArithLit.Focus.t -> Z.t Monome.t option
val opposite_monome_exn : ArithLit.Focus.t -> Z.t Monome.t
val is_max : ord:Libzipperposition.Ordering.t -> ArithLit.Focus.t -> bool
val is_strictly_max :
ord:Libzipperposition.Ordering.t -> ArithLit.Focus.t -> bool
val map_lit :
f_m:(Z.t Monome.t -> Z.t Monome.t) ->
f_mf:(Z.t Monome.Focus.t -> Z.t Monome.Focus.t) ->
ArithLit.Focus.t -> ArithLit.Focus.t
val product : ArithLit.Focus.t -> Z.t -> ArithLit.Focus.t
val scale :
ArithLit.Focus.t ->
ArithLit.Focus.t -> ArithLit.Focus.t * ArithLit.Focus.t
val scale_power : ArithLit.Focus.t -> int -> ArithLit.Focus.t
val apply_subst :
renaming:Libzipperposition.Substs.Renaming.t ->
Libzipperposition.Substs.t ->
ArithLit.Focus.t Libzipperposition.Scoped.t -> ArithLit.Focus.t
val apply_subst_no_renaming :
Libzipperposition.Substs.t ->
ArithLit.Focus.t Libzipperposition.Scoped.t -> ArithLit.Focus.t
val unify :
?subst:Libzipperposition.Substs.t ->
ArithLit.Focus.t Libzipperposition.Scoped.t ->
ArithLit.Focus.t Libzipperposition.Scoped.t ->
(ArithLit.Focus.t * ArithLit.Focus.t * Libzipperposition.Substs.t)
Sequence.t
val fold_terms :
?pos:Libzipperposition.Position.t ->
ArithLit.lit ->
(ArithLit.Focus.t * Libzipperposition.Position.t) Sequence.t
val op : ArithLit.Focus.t -> [ `Binary of ArithLit.op | `Divides ]
val unfocus : ArithLit.Focus.t -> ArithLit.lit
val pp : ArithLit.Focus.t CCFormat.printer
val to_string : ArithLit.Focus.t -> string
end