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/Hlt_elim/index.html

Module `Libzipperposition_calculi.Hlt_elim`

module T = Logtk.Term

module Ty = Logtk.Type

module Lits = Logtk.Literals

module Lit = Logtk.Literal

module A = Libzipperposition_avatar

val section : Logtk.Util.Section.t

val k_enabled : bool Logtk.Flex_state.key

val k_max_depth : int Logtk.Flex_state.key

val k_simpl_new : bool Logtk.Flex_state.key

val k_clauses_to_track : [ `Active | `All | `Passive ] Logtk.Flex_state.key

val k_max_self_impls : int Logtk.Flex_state.key

val k_unit_propagated_hle : bool Logtk.Flex_state.key

val k_reduce_tautologies : bool Logtk.Flex_state.key

val k_delete_lits : bool Logtk.Flex_state.key

val k_max_tracked_clauses : int Logtk.Flex_state.key

val k_track_eq : bool Logtk.Flex_state.key

val k_insert_only_ordered : bool Logtk.Flex_state.key

val k_heartbeat_steps : int option Logtk.Flex_state.key

val k_heartbeat_disabled_hlbe : bool Logtk.Flex_state.key

val k_max_imp_entries : int Logtk.Flex_state.key

val k_basic_rules : bool Logtk.Flex_state.key

val k_penalize_tautologies : bool Logtk.Flex_state.key

module type S = sig ... end

module Make (E : Libzipperposition.Env.S) : S with module Env = E

val max_depth_ : int ref

val enabled_ : bool ref

val simpl_new_ : bool ref

val clauses_to_track_ : [ `Active | `All | `Passive ] ref

val max_self_impls_ : int ref

val max_tracked_clauses : int ref

val propagated_hle : bool ref

val hte_ : bool ref

val hle_ : bool ref

val track_eq_ : bool ref

val insert_ordered_ : bool ref

val heartbeat_steps : int option ref

val max_imp_ : int ref

val basic_rules_ : bool ref

val penalize_tautologies_ : bool ref

val extension : Libzipperposition.Extensions.t