package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

Library for Zipperposition

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

Maintainers

S

simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz

md5=e72de75e9f0f87da9e6e8c0a4d4c89f9

sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

doc/libzipperposition.calculi/Libzipperposition_calculi/Pure_literal_elim/index.html

Module `Libzipperposition_calculi.Pure_literal_elim`

val section : Logtk.Util.Section.t

type id_sgn = Logtk.ID.t * bool

module IDMap : sig ... end

module IntSet = Logtk.Util.Int_set

module TST = Logtk.TypedSTerm

exception AppVarFound

val _enabled : bool ref

val total_clauses : Logtk.Util.stat

val removed_clauses : Logtk.Util.stat

val pp_key : (Logtk.ID.t * CCBool.t) CCPair.printer

val cl_syms : Logtk__TypedSTerm.t Logtk.SLiteral.t list -> Logtk.ID.Set.t

val compute_occurence_map : 
  (TST.t Logtk.SLiteral.t list, TST.t, TST.t) Logtk.Statement.t Iter.t ->
  Logtk.ID.Set.t * IntSet.t Logtk.ID.Map.t * int IDMap.t list

val get_pure_symbols : 
  Logtk.ID.Set.t ->
  IntSet.t Logtk.ID.Map.t ->
  int IDMap.t list ->
  Logtk.ID.Set.t

val remove_pure_clauses : 
  (TST.t Logtk.SLiteral.t list, TST.t, TST.t) Logtk.Statement.t Iter.t ->
  (TST.t Logtk.SLiteral.t CCList.t, TST.t, TST.t) Logtk.Statement.t Iter.t

val extension : Libzipperposition.Extensions.t