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.2007@m4x.org

Sources

2.0.tar.gz

md5=7a8e57388083ed763d12d18324c8a086

sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

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