Module `Logtk.Literal`

Literals

type term = Term.t
type t = private | True | False | Equation of term * 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: 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: weight of the lit (sum of weights of terms)

val ho_weight : t -> int

weight of the lit (sum of weights of terms)

ho weight of the lit (sum of weights of terms, ignoring applied variables and lambda prefixes

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

ho weight of the lit (sum of weights of terms, ignoring applied variables and lambda prefixes

heuristic difficulty to eliminate lit

val depth : t -> int: depth of literal

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

val is_neg : t -> bool: is the literal negative?

val is_eqn : t -> bool: is the literal a proper (in)equation or prop?

val is_prop : t -> bool: is the literal a boolean proposition?

val is_eq : t -> bool: is the literal of the form a = b?

val is_neq : t -> bool: is the literal of the form a != b?

val is_essentially_prop : t -> bool

is the literal of the form a != b?

is the literal non-equational literal of type Prop

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

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

val is_arith_less : t -> bool
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: proposition

val mk_true : term -> t: true proposition

val mk_false : term -> t: false proposition

val mk_tauto : t: tautological literal

val mk_absurd : t: absurd literal, like ~ true

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 no_prop_invariant : t -> bool
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) Iter.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) Iter.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) Iter.t
val unify : ?⁠subst:Unif_subst.t -> t Scoped.t -> t Scoped.t -> (Unif_subst.t * Builtin.Tag.t list) Iter.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 fold : ('a -> term -> 'a) -> 'a -> t -> 'a: basic fold

val for_all : (term -> bool) -> t -> bool: for the term or both terms of the literal

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

val var_occurs : Type.t HVar.t -> t -> bool
val is_ground : t -> bool
val symbols : ?⁠include_types:bool -> 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 is_app_var_eq : t -> bool: if is_absurd lit, return why

val is_type_pred : t -> bool

val is_typex_pred : t -> bool

val is_propositional : t -> bool

val as_inj_def : t -> (ID.t * (Term.var * Term.var) list) option

val is_pure_var : t -> bool

val as_pos_pure_var : t -> (Term.var * Term.var) option

val fold_terms : ?⁠position:Position.t -> ?⁠vars:bool -> ?⁠var_args:bool -> ?⁠fun_bodies:bool -> ?⁠ty_args:bool -> which:[< `Max | `All ] -> ?⁠ord:Ordering.t -> subterms:bool -> t -> term Position.With.t Iter.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) var_args decides whether arguments of applied variables are iterated on too fun_bodies decides whether bodies of lambda-expressions are iterated on too ty_args decides whether type arguments are iterated on too 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

val normalize_eq : t -> t option

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