Module ArithLit.Focus

module Focus: sig .. end

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`

focus on a term in one of the two monomes

val mk_left : ArithLit.op -> Z.t Monome.Focus.t -> Z.t Monome.t -> t

val mk_right : ArithLit.op -> Z.t Monome.t -> Z.t Monome.Focus.t -> t

val mk_div : ?sign:bool -> Z.t -> power:int -> Z.t Monome.Focus.t -> t

val get : ArithLit.lit -> Libzipperposition.Position.t -> t option

val get_exn : ArithLit.lit -> Libzipperposition.Position.t -> t

Raises Invalid_argument if the position doesn't fit

val focus_term : ArithLit.lit -> ArithLit.term -> t option

Attempt to focus on the given atomic term, if it occurs directly under the arith literal

val focus_term_exn : ArithLit.lit -> ArithLit.term -> t

val replace : t -> Z.t Monome.t -> ArithLit.lit

replace a m replaces mf.coeff × mf.term with m where mf is the focused monome in a, and return the resulting literal

val term : t -> ArithLit.term

Focused term

val focused_monome : t -> Z.t Monome.Focus.t

The focused monome

val opposite_monome : t -> Z.t Monome.t option

The opposite monome (in Left and Right), if any.

val opposite_monome_exn : t -> Z.t Monome.t

Unsafe version of ArithLit.Focus.opposite_monome.
Raises Invalid_argument if the literal is a Div

val is_max : ord:Libzipperposition.Ordering.t -> t -> bool

Is the focused term maximal in the literal?

val is_strictly_max : ord:Libzipperposition.Ordering.t -> t -> bool

Is the focused term maximal in the literal, ie is it greater than all the othe terms?

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) ->
       t -> t

Apply a function to the monomes and focused monomes

val product : t -> Z.t -> t

Product by a constant

val scale : t -> t -> t * t

Multiply the two literals by some constant so that their focused literals have the same coefficient

val scale_power : t -> int -> t

For a "divides" literal, bring it to the given power.
Raises Invalid_argument if the current power is strictly greater than the argument (cannot scale down), or if the literal is not a Div

val apply_subst : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t

Apply a substitution

val apply_subst_no_renaming : Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t

Apply a substitution with renaming (careful with collisions!)

val unify : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t ->
       (t * t * Libzipperposition.Substs.t) Sequence.t

Unify the two focused terms, and possibly other terms of their respective focused monomes; yield the new literals accounting for the unification along with the unifier

val fold_terms : ?pos:Libzipperposition.Position.t ->
       ArithLit.lit -> (t * Libzipperposition.Position.t) Sequence.t

Fold on focused terms in the literal, one by one, with the position of the focused term

val op : t -> [ `Binary of ArithLit.op | `Divides ]

val unfocus : t -> ArithLit.lit

Conversion back to a literal

val pp : t CCFormat.printer

val to_string : t -> string