Booleans (p.libzipperposition.2.1.doc.libzipperposition.calculi.Libzipperposition

Booleans

val _quant_rename : bool ref

type reasoning_kind =

val k_bool_reasoning : reasoning_kind Logtk.Flex_state.key

module type S = sig ... end

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

val extension : Libzipperposition.Extensions.t

val name_quantifiers : 
  Logtk.TypeInference.typed_statement CCVector.ro_vector ->
  Logtk.TypeInference.typed_statement CCVector.ro_vector

val preprocess_booleans : 
  Logtk.TypeInference.typed_statement CCVector.ro_vector ->
  Logtk.TypeInference.typed_statement CCVector.ro_vector

val preprocess_cnf_booleans : 
  Logtk.Statement.clause_t CCVector.ro_vector ->
  Logtk.Statement.clause_t CCVector.ro_vector