Module `Logtk.Literal`

Literals

type term = Term.t
type t = private | True | False | Equation of term * term * bool | Prop of term * bool | Int of Int_lit.t | Rat of Rat_lit.t: a literal, that is, a signed atomic formula

val equal_com : t -> t -> bool: commutative equality of lits

val compare : t -> t -> int

commutative equality of lits

lexicographic comparison of literals

include Interfaces.HASH with type t := t

include Interfaces.EQ

type t

val equal : t -> t -> bool

val hash : t -> int

val hash : t -> int: hashing of literal

val weight : t -> int

hashing of literal

weight of the lit (sum of weights of terms)

val heuristic_weight : (term -> int) -> t -> int

weight of the lit (sum of weights of terms)

heuristic difficulty to eliminate lit

val depth : t -> int

heuristic difficulty to eliminate lit

depth of literal

val sign : t -> bool: depth of literal

val is_pos : t -> bool: is the literal positive?

val is_neg : t -> bool

is the literal positive?

is the literal negative?

val is_eqn : t -> bool

is the literal negative?

is the literal a proper (in)equation or prop?

val is_prop : t -> bool

is the literal a proper (in)equation or prop?

is the literal a boolean proposition?

val is_eq : t -> bool

is the literal a boolean proposition?

is the literal of the form a = b?

val is_neq : t -> bool

is the literal of the form a = b?

is the literal of the form a != b?

val is_arith : t -> bool
val is_arith_eqn : t -> bool: = or !=

val is_arith_eq : t -> bool: = or !=

val is_arith_neq : t -> bool
val is_arith_ineq : t -> bool: < or <=

val is_arith_less : t -> bool: < or <=

val is_arith_lesseq : t -> bool
val is_arith_divides : t -> bool
val is_rat : t -> bool
val is_rat_eq : t -> bool
val is_rat_less : t -> bool
val mk_eq : term -> term -> t: build literals. If sides so not have the same sort, a SortError will be raised. An ordering must be provided

val mk_neq : term -> term -> t
val mk_lit : term -> term -> bool -> t
val mk_prop : term -> bool -> t
val mk_true : term -> t
val mk_false : term -> t
val mk_tauto : t
val mk_absurd : t
val mk_arith : Int_lit.t -> t
val mk_arith_op : Int_lit.op -> Z.t Monome.t -> Z.t Monome.t -> t
val mk_arith_eq : Z.t Monome.t -> Z.t Monome.t -> t
val mk_arith_neq : Z.t Monome.t -> Z.t Monome.t -> t
val mk_arith_less : Z.t Monome.t -> Z.t Monome.t -> t
val mk_arith_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 mk_rat : Rat_lit.t -> t
val mk_rat_op : Rat_lit.op -> Q.t Monome.t -> Q.t Monome.t -> t
val mk_rat_eq : Q.t Monome.t -> Q.t Monome.t -> t
val mk_rat_less : Q.t Monome.t -> Q.t Monome.t -> t
val mk_constraint : term -> term -> t: mk_constraint t u makes a disequation or a HO constraint depending on how t and u look.

val matching : ?⁠subst:Subst.t -> pattern:t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Sequence.t: checks whether subst(lit_a) matches lit_b. Returns alternative substitutions s such that s(lit_a) = lit_b and s contains subst.

val subsumes : ?⁠subst:Subst.t -> t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Sequence.t: More general version of matching, yields subst such that subst(lit_a) => lit_b.

val variant : ?⁠subst:Subst.t -> t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Sequence.t
val unify : ?⁠subst:Unif_subst.t -> t Scoped.t -> t Scoped.t -> (Unif_subst.t * Builtin.Tag.t list) Sequence.t
val are_variant : t -> t -> bool
val apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
val apply_subst_no_simp : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
val apply_subst_list : Subst.Renaming.t -> Subst.t -> t list Scoped.t -> t list

exception Lit_is_constraint

val negate : t -> t: negate literal

val is_constraint : t -> bool: Is the literal a constraint?

val is_ho_constraint : t -> bool
val of_unif_subst : Subst.Renaming.t -> Unif_subst.t -> t list: Make a list of (negative) literals out of the unification constraints contained in this substitution.

val map : (term -> term) -> t -> t: functor

val map_no_simp : (term -> term) -> t -> t

functor

val fold : ('a -> term -> 'a) -> 'a -> t -> 'a

functor

basic fold

val for_all : (term -> bool) -> t -> bool

basic fold

for the term or both terms of the literal

val vars : t -> Type.t HVar.t list

for the term or both terms of the literal

gather variables

val var_occurs : Type.t HVar.t -> t -> bool: gather variables

val is_ground : t -> bool
val symbols : t -> Logtk.ID.Set.t
val root_terms : t -> term list: all the terms immediatly under the lit

val to_ho_term : t -> term option: Conversion to higher-order term using Term.Form

val as_ho_predicate : t -> (Term.var * term * term list * bool) option: View on literals F t1…tn and ¬ (F t1…tn)

val is_ho_predicate : t -> bool: Does as_ho_predicate return Some?

module Set : CCSet.S with type Set.elt = t

Basic semantic checks

val is_trivial : t -> bool
val is_absurd : t -> bool
val is_absurd_tags : t -> Proof.tag list: if is_absurd lit, return why

val fold_terms : ?⁠position:Position.t -> ?⁠vars:bool -> ?⁠ty_args:bool -> which:[< `Max | `All ] -> ?⁠ord:Ordering.t -> subterms:bool -> t -> term Position.With.t Sequence.t

Iterate on terms, maybe subterms, of the literal. Variables are ignored if vars is false.

vars decides whether variables are iterated on too (default false) subterms decides whether strict subterms, not only terms that occur directly under the literal, are explored.

which is used to decide which terms to visit:

if which is `Max, only the maximal terms are explored
if which is `All, all root terms are explored

module Comp : sig ... end

module Seq : sig ... end

module Pos : sig ... end

val replace : t -> old:term -> by:term -> t: replace lit ~old ~by syntactically replaces all occurrences of old in lit by the term by.

module View : sig ... end

module Conv : sig ... end

IO

type print_hook = CCFormat.t -> t -> bool

might print the literal on the given buffer.

returns: true if it printed, false otherwise

val add_default_hook : print_hook -> unit
val pp_debug : ?⁠hooks:print_hook list -> t CCFormat.printer
val pp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val to_string : t -> string