Module Skolem

module Skolem: sig .. end

Skolemization

type term = Nunchaku_core.TermInner.Default.t

val name : string

type mode = [ `Sk_all | `Sk_ho | `Sk_types ]

type state

val create : ?prefix:string -> mode:mode -> unit -> state

prefix : the prefix used to generate Skolem symbols

mode : the kind of skolemization we expect

val skolemize : state:state ->
       ?in_goal:bool ->
       Nunchaku_core.Polarity.t ->
       term -> term * (Nunchaku_core.ID.t * term) list

skolemize ~state pol t returns t', new_syms where t' is the skolemization of t under polarity pol, and new_syms is a set of new symbols with their type

in_goal : if true, record skolem definitions so that they can appear in the model

val print_state : Format.formatter -> state -> unit

val skolemize_pb : state:state ->
       (term, term) Nunchaku_core.Problem.t ->
       (term, term) Nunchaku_core.Problem.t

val decode_model : skolems_in_model:bool ->
       state:state ->
       (term, term) Nunchaku_core.Model.t ->
       (term, term) Nunchaku_core.Model.t

Decode the given model

skolems_in_model : if true, skolem constants will stay in the model after decoding; otherwise they are dropped

val pipe : skolems_in_model:bool ->
       mode:mode ->
       print:bool ->
       check:bool ->
       ((term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.Res.t,
        (term, term) Nunchaku_core.Problem.Res.t)
       Nunchaku_core.Transform.t

val pipe_with : mode:mode ->
       decode:(state -> 'c -> 'd) ->
       print:bool ->
       check:bool ->
       ((term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.t, 'c, 'd)
       Nunchaku_core.Transform.t

Similar to Skolem.pipe but with a generic decode function.

mode : determines which variables are skolemized

decode : is given find_id_def, which maps Skolemized constants to the formula they define

print : if true, prints problem after skolemization

check : if true, check the invariants on the result