sig
type term = Libzipperposition.FOTerm.t
type t = Literal.t array
val equal_com : Literals.t -> Literals.t -> bool
val compare : Literals.t -> Literals.t -> int
val equal : Literals.t -> Literals.t -> bool
val hash_fun : t -> CCHash.state -> CCHash.state
val hash : t -> int
val variant :
?subst:Libzipperposition.Substs.t ->
Literals.t Libzipperposition.Scoped.t ->
Literals.t Libzipperposition.Scoped.t ->
Libzipperposition.Substs.t Sequence.t
val are_variant : Literals.t -> Literals.t -> bool
val weight : Literals.t -> int
val depth : Literals.t -> int
val vars :
Literals.t -> Libzipperposition.Type.t Libzipperposition.HVar.t list
val is_ground : Literals.t -> bool
val to_form : Literals.t -> Literals.term Libzipperposition.SLiteral.t list
val apply_subst :
renaming:Libzipperposition.Substs.Renaming.t ->
Libzipperposition.Substs.t ->
Literals.t Libzipperposition.Scoped.t -> Literals.t
val map : (Literals.term -> Literals.term) -> Literals.t -> Literals.t
val pos : Literals.t -> CCBV.t
val neg : Literals.t -> CCBV.t
val maxlits : ord:Libzipperposition.Ordering.t -> Literals.t -> CCBV.t
val maxlits_l :
ord:Libzipperposition.Ordering.t -> Literals.t -> (Literal.t * int) list
val is_max : ord:Libzipperposition.Ordering.t -> Literals.t -> int -> bool
val is_trivial : Literals.t -> bool
val is_absurd : Literals.t -> bool
module Seq :
sig
val vars :
Literals.t ->
Libzipperposition.Type.t Libzipperposition.HVar.t Sequence.t
val terms : Literals.t -> Literals.term Sequence.t
val to_form :
Literals.t -> Literals.term Libzipperposition.SLiteral.t Sequence.t
end
module Pos :
sig
val at : Literals.t -> Libzipperposition.Position.t -> Literals.term
val lit_at :
Literals.t ->
Libzipperposition.Position.t ->
Literal.t * Libzipperposition.Position.t
val replace :
Literals.t ->
at:Libzipperposition.Position.t -> by:Literals.term -> unit
val idx : Libzipperposition.Position.t -> int
val tail : Libzipperposition.Position.t -> Libzipperposition.Position.t
val cut :
Libzipperposition.Position.t -> int * Libzipperposition.Position.t
end
module Conv :
sig
val of_forms :
?hooks:Literal.Conv.hook_from list ->
Literals.term Libzipperposition.SLiteral.t list -> Literals.t
val to_forms :
?hooks:Literal.Conv.hook_to list ->
Literals.t -> Literals.term Libzipperposition.SLiteral.t list
end
module View :
sig
val get_eqn :
Literals.t ->
Libzipperposition.Position.t ->
(Literals.term * Literals.term * bool) option
val get_arith :
Literals.t -> Libzipperposition.Position.t -> ArithLit.Focus.t option
val get_eqn_exn :
Literals.t ->
Libzipperposition.Position.t -> Literals.term * Literals.term * bool
val get_arith_exn :
Literals.t -> Libzipperposition.Position.t -> ArithLit.Focus.t
end
val fold_lits :
eligible:(int -> Literal.t -> bool) ->
Literals.t -> (Literal.t * int) Sequence.t
val fold_eqn :
?both:bool ->
?sign:bool ->
ord:Libzipperposition.Ordering.t ->
eligible:(int -> Literal.t -> bool) ->
Literals.t ->
(Literals.term * Literals.term * bool * Libzipperposition.Position.t)
Sequence.t
val fold_arith :
eligible:(int -> Literal.t -> bool) ->
Literals.t -> (ArithLit.t * Libzipperposition.Position.t) Sequence.t
val fold_arith_terms :
eligible:(int -> Literal.t -> bool) ->
which:[< `All | `Max ] ->
ord:Libzipperposition.Ordering.t ->
Literals.t ->
(Literals.term * ArithLit.Focus.t * Libzipperposition.Position.t)
Sequence.t
val fold_terms :
?vars:bool ->
?ty_args:bool ->
which:[< `All | `Max ] ->
ord:Libzipperposition.Ordering.t ->
subterms:bool ->
eligible:(int -> Literal.t -> bool) ->
Literals.t -> (Literals.term * Libzipperposition.Position.t) Sequence.t
val symbols :
?init:Libzipperposition.ID.Set.t ->
Literals.t -> Libzipperposition.ID.Set.t
val pp : Literals.t CCFormat.printer
val pp_tstp : Literals.t CCFormat.printer
val to_string : Literals.t -> string
val is_RR_horn_clause : Literals.t -> bool
val is_horn : Literals.t -> bool
val is_pos_eq : Literals.t -> (Literals.term * Literals.term) option
end