Module Logtk.Literal

Literals

Literals are the representation of atomic formulas in the clausal world of resolution/superposition provers.

A literal is an atomic formula (equality or predicate), paired with a sign that carries negation.

type term = Term.t
type t = private
  1. | True
  2. | False
  3. | Equation of term * term * bool

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 with type t := t
val equal : t -> t -> bool
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 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 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 are_opposite_subst : subst:Subst.t -> t Scoped.t -> t Scoped.t -> bool

Literals are equal according to given substitution for variables, but are of opposite sign

val are_opposite_same_sc : t -> t -> bool

Literals are equal, but are of opposite signs

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 -> ID.Set.t
val root_terms : t -> term list

all the terms immediatly under the lit

val to_ho_term : t -> term

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 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_predicate_lit : 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 max_term_positions : ord:Ordering.t -> t -> int
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_zf : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val to_string : t -> string