Module Logtk.LiteralSource

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.

We also have special arithmetic literals that have the intuitive meaning, see Int_lit and Rat_lit for more details.

Sourcetype term = Term.t
Sourcetype t = private
  1. | True
  2. | False
  3. | Equation of term * term * bool
  4. | Int of Int_lit.t
  5. | Rat of Rat_lit.t

a literal, that is, a signed atomic formula

Sourceval equal_com : t -> t -> bool

commutative equality of lits

Sourceval compare : t -> t -> int

lexicographic comparison of literals

include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int

hashing of literal

Sourceval weight : t -> int

weight of the lit (sum of weights of terms)

Sourceval 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

Sourceval 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

Sourceval depth : t -> int

depth of literal

Sourceval is_pos : t -> bool

is the literal positive?

Sourceval is_neg : t -> bool

is the literal negative?

Sourceval is_eqn : t -> bool

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

Sourceval is_prop : t -> bool

is the literal a boolean proposition?

Sourceval is_eq : t -> bool

is the literal of the form a = b?

Sourceval is_neq : t -> bool

is the literal of the form a != b?

Sourceval is_essentially_prop : t -> bool

is the literal of the form a != b?

is the literal non-equational literal of type Prop

Sourceval is_arith : t -> bool
Sourceval is_arith_eqn : t -> bool

= or !=

Sourceval is_arith_eq : t -> bool
Sourceval is_arith_neq : t -> bool
Sourceval is_arith_ineq : t -> bool

< or <=

Sourceval is_arith_less : t -> bool
Sourceval is_arith_lesseq : t -> bool
Sourceval is_arith_divides : t -> bool
Sourceval is_rat : t -> bool
Sourceval is_rat_eq : t -> bool
Sourceval is_rat_less : t -> bool
Sourceval 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

Sourceval mk_neq : term -> term -> t
Sourceval mk_lit : term -> term -> bool -> t
Sourceval mk_prop : term -> bool -> t

proposition

Sourceval mk_true : term -> t

true proposition

Sourceval mk_false : term -> t

false proposition

Sourceval mk_tauto : t

tautological literal

Sourceval mk_absurd : t

absurd literal, like ~ true

Sourceval mk_arith : Int_lit.t -> t
Sourceval mk_arith_op : Int_lit.op -> Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_arith_eq : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_arith_neq : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_arith_less : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_arith_lesseq : Z.t Monome.t -> Z.t Monome.t -> t
Sourceval mk_divides : ?sign:bool -> Z.t -> power:int -> Z.t Monome.t -> t
Sourceval mk_not_divides : Z.t -> power:int -> Z.t Monome.t -> t
Sourceval mk_rat : Rat_lit.t -> t
Sourceval mk_rat_op : Rat_lit.op -> Q.t Monome.t -> Q.t Monome.t -> t
Sourceval mk_rat_eq : Q.t Monome.t -> Q.t Monome.t -> t
Sourceval mk_rat_less : Q.t Monome.t -> Q.t Monome.t -> t
Sourceval no_prop_invariant : t -> bool
Sourceval mk_constraint : term -> term -> t

mk_constraint t u makes a disequation or a HO constraint depending on how t and u look.

Sourceval 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.

Sourceval 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.

Sourceval variant : ?subst:Subst.t -> t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t
Sourceval are_variant : t -> t -> bool
Sourceval apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
Sourceval apply_subst_no_simp : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
Sourceval apply_subst_list : Subst.Renaming.t -> Subst.t -> t list Scoped.t -> t list
Sourceexception Lit_is_constraint
Sourceval negate : t -> t

negate literal

Sourceval is_constraint : t -> bool

Is the literal a constraint?

Sourceval is_ho_constraint : t -> bool
Sourceval 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.

Sourceval map : (term -> term) -> t -> t

functor

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

basic fold

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

for the term or both terms of the literal

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

gather variables

Sourceval var_occurs : Type.t HVar.t -> t -> bool
Sourceval is_ground : t -> bool
Sourceval symbols : ?include_types:bool -> t -> ID.Set.t
Sourceval root_terms : t -> term list

all the terms immediatly under the lit

Sourceval to_ho_term : t -> term option

Conversion to higher-order term using Term.Form

Sourceval as_ho_predicate : t -> (Term.var * term * term list * bool) option

View on literals F t1…tn and ¬ (F t1…tn)

Sourceval is_ho_predicate : t -> bool

Does as_ho_predicate return Some?

Sourcemodule Set : CCSet.S with type elt = t

Basic semantic checks

Sourceval is_trivial : t -> bool
Sourceval is_absurd : t -> bool
Sourceval is_absurd_tags : t -> Proof.tag list

if is_absurd lit, return why

Sourceval is_app_var_eq : t -> bool

if is_absurd lit, return why

Sourceval is_type_pred : t -> bool
Sourceval is_typex_pred : t -> bool
Sourceval is_propositional : t -> bool
Sourceval as_inj_def : t -> (ID.t * (Term.var * Term.var) list) option
Sourceval is_pure_var : t -> bool
Sourceval as_pos_pure_var : t -> (Term.var * Term.var) option
Sourceval 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
Sourceval normalize_eq : t -> t option
Sourcemodule Comp : sig ... end
Sourcemodule Seq : sig ... end
Sourcemodule Pos : sig ... end
Sourceval replace : t -> old:term -> by:term -> t

replace lit ~old ~by syntactically replaces all occurrences of old in lit by the term by.

Sourcemodule View : sig ... end
Sourcemodule Conv : sig ... end

IO

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

might print the literal on the given buffer.

  • returns

    true if it printed, false otherwise

Sourceval add_default_hook : print_hook -> unit
Sourceval pp_debug : ?hooks:print_hook list -> t CCFormat.printer
Sourceval to_string : t -> string