package libzipperposition

  1. Overview
  2. Docs

Module Libzipperposition.Bool_selection

Boolean selection functions

module T = Logtk.Term
module Pos = Logtk.Position

As described in FBoolSup paper, Boolean selection function selects positions in the clause that are non-interpreted Boolean subterms.

type t = Logtk.Literal.t array -> (Logtk.Term.t * Logtk.Position.t) list
type parametrized = strict:bool -> ord:Logtk.Ordering.t -> t

Selection Functions

val all_selectable_subterms : ?forbidden:T.VarSet.t -> ord:Logtk.Ordering.t -> pos_builder:PB.t -> T.t -> ((T.t * Pos.t) -> unit) -> unit
val all_eligible_subterms : ord:Logtk.Ordering.t -> pos_builder:PB.t -> T.t -> ((T.t * Pos.t) -> unit) -> unit
val from_string : ord:Logtk.Ordering.t -> string -> t

selection function from string (may fail)