package libzipperposition

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

Module AC.MakeSource

Parameters

module Env : Env.S

Signature

module Env = Env
Sourcemodule C : module type of Env.C
Sourceval 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.

Sourceval is_ac : Logtk.ID.t -> bool

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

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

set of AC symbols

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

set of AC symbols occurring in the given term

Sourceval exists_ac : unit -> bool

Is there any AC symbol?

Sourceval scan_statement : Logtk.Statement.clause_t -> unit

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

Rules

Sourceval is_trivial_lit : Logtk.Literal.t -> bool

Is the literal AC-trivial?

Sourceval is_trivial : C.t -> bool

Check whether the clause is AC-trivial

Simplify the clause modulo AC

Sourceval 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