package libzipperposition

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

Parameters

module Env : Env.S

Signature

module Env = Env
module C : sig ... end
val add : proof:Logtk.Proof.parent -> Logtk.ID.t -> Logtk.Type.t -> unit

Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.

val is_ac : Logtk.ID.t -> bool
val find_proof : Logtk.ID.t -> Logtk.Proof.parent

Recover the proof for the AC-property of this symbol.

  • raises Not_found

    if the symbol is not AC

val symbols : unit -> Logtk.ID.Set.t

set of AC symbols

val symbols_of_terms : Logtk.Term.t Iter.t -> Logtk.ID.Set.t

set of AC symbols occurring in the given term

val exists_ac : unit -> bool

Is there any AC symbol?

val scan_statement : Logtk.Statement.clause_t -> unit

Check whether the statement contains an "AC" attribute, do the proper declaration in this case

Rules

val is_trivial_lit : Logtk.Literal.t -> bool

Is the literal AC-trivial?

val is_trivial : C.t -> bool

Check whether the clause is AC-trivial

val simplify : Env.simplify_rule

Simplify the clause modulo AC

val setup : unit -> unit

Register on Env

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