Previous  Up  Next

Module Literal

module Literal: sig .. end

Equational literals


type term = Libzipperposition.FOTerm.t 
type t = private
| True
| False
| Equation of term * term * bool
| Prop of term * bool
| Arith of ArithLit.t
a literal, that is, a signed atomic formula
val equal : t -> t -> bool
equality of literals
val equal_com : t -> t -> bool
commutative equality of lits
val compare : t -> t -> int
lexicographic comparison of literals
include Interfaces.HASH
val hash : t -> int
hashing of literal
val weight : t -> int
weight of the lit (sum of weights of terms)
val heuristic_weight : (term -> int) -> t -> int
heuristic difficulty to eliminate lit
val depth : t -> int
depth of literal
val sign : t -> bool
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_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 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 : ArithLit.t -> t
val mk_arith_op : ArithLit.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 matching : ?subst:Libzipperposition.Substs.t ->
       pattern:t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t -> Libzipperposition.Substs.t 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:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t -> Libzipperposition.Substs.t Sequence.t
More general version of Literal.matching, yields subst such that subst(lit_a) => lit_b.
val variant : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t -> Libzipperposition.Substs.t Sequence.t
val unify : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t -> Libzipperposition.Substs.t Sequence.t
val are_variant : t -> t -> bool
val apply_subst : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t
val apply_subst_no_renaming : Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t
val apply_subst_no_simp : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t
val apply_subst_list : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t list Libzipperposition.Scoped.t -> t list
val negate : t -> t
negate literal
val map : (term -> term) -> t -> t
functor
val fold : ('a -> term -> 'a) -> 'a -> t -> 'a
basic fold
val vars : t -> Libzipperposition.Type.t Libzipperposition.HVar.t list
gather variables
val var_occurs : Libzipperposition.Type.t Libzipperposition.HVar.t -> t -> bool
val is_ground : t -> bool
val symbols : t -> Libzipperposition.ID.Set.t
val root_terms : t -> term list
all the terms immediatly under the lit

Basic semantic checks


val is_trivial : t -> bool
val is_absurd : t -> bool
val fold_terms : ?position:Libzipperposition.Position.t ->
       ?vars:bool ->
       ?ty_args:bool ->
       which:[< `All | `Max ] ->
       ord:Libzipperposition.Ordering.t ->
       subterms:bool ->
       t -> (term * Libzipperposition.Position.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:


module Comp: sig .. end
Comparisons 
module Seq: sig .. end
module Pos: sig .. end
Positions 
module View: sig .. end
Specific views 
module Conv: sig .. end
Conversions

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_tstp : t CCFormat.printer
val to_string : t -> string