package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

Signature

module Env = Env
module C : sig ... end
module PS : sig ... end
module Stm : Libzipperposition.Stream.S with module C = Env.C
Term Indices
val idx_sup_into : unit -> PS.TermIndex.t

index for superposition into the set

val idx_sup_from : unit -> PS.TermIndex.t

index for superposition from the set

val idx_fv : unit -> PS.SubsumptionIndex.t

index for subsumption

Inference Rules
val infer_active : Env.binary_inf_rule

superposition where given clause is active

val infer_passive : Env.binary_inf_rule

superposition where given clause is passive

val infer_equality_resolution : Env.unary_inf_rule
val infer_equality_factoring : Env.unary_inf_rule
Extraction of clauses from the queue (HO feature)
val extract_from_stream_queue : Env.generate_rule

Extracts at most as many clauses from the stream queue as there are streams in the queue. If called with ~full=true extracts only one clause but may loop forever.

val extract_from_stream_queue_fix_stm : Env.generate_rule

Same as extract_from_stream_queue with a different extraction heuristic If possible, all clauses are taken from the first stream

Simplifications rules
val is_tautology : C.t -> bool

Check whether the clause is a (syntactic) tautology, ie whether it contains true or "A" and "not A"

val is_semantic_tautology : C.t -> bool

semantic tautology deletion, using a congruence closure algorithm to see if negative literals imply some positive Literal.t

val handle_distinct_constants : Env.lit_rewrite_rule

Decide on "quoted" "symbols" (which are all distinct)

val basic_simplify : Env.simplify_rule

basic simplifications (remove duplicate literals, trivial literals, destructive equality resolution...)

val subsumes : Logtk.Literal.t array -> Logtk.Literal.t array -> bool

subsumes c1 c2 iff c1 subsumes c2

returns subsuming subst if the first clause subsumes the second one

val eq_subsumes : Logtk.Literal.t array -> Logtk.Literal.t array -> bool

equality subsumption

val subsumed_by_active_set : C.t -> bool

check whether the clause is subsumed by any clause in the set

val subsumed_in_active_set : Env.backward_redundant_rule

list of clauses in the active set that are subsumed by the clause

val contextual_literal_cutting : Env.simplify_rule

contextual Literal.t cutting of the given clause by the active set

val condensation : Env.simplify_rule

condensation

Registration
val register : unit -> unit

Register rules in the environment

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct