module LogtkSkolem:`sig`

..`end`

`type `

ctx

Context needed to create new symbols

`val create : ``?ty_prop:LogtkType.t ->`

?prefix:string -> ?prop_prefix:string -> LogtkSignature.t -> ctx

New skolem contex. A prefix can be provided, which will be
added to all newly created skolem symbols.

`ty_prop`

: the type of atomic propositions (default `LogtkType.TPTP.o`

).`prefix`

: used to name skolem functions/constants`prop_prefix`

: used to name sub-formulas during CNF`val to_signature : ``ctx -> LogtkSignature.t`

Signature of all new skolem symbols that were created using this
context.

`val fresh_sym : ``ctx:ctx -> ty:LogtkType.t -> LogtkSymbol.t`

Just obtain a fresh skolem symbol. It is also declared
in the inner signature.

`val fresh_sym_with : ``ctx:ctx -> ty:LogtkType.t -> string -> LogtkSymbol.t`

Fresh symbol with a different name

`val fresh_ty_const : ``?prefix:string -> ctx:ctx -> unit -> LogtkSymbol.t`

New symbol to be used as a type constant (no need to declare it)

`val instantiate_ty : ``LogtkFormula.FO.t -> LogtkType.t -> LogtkFormula.FO.t`

Instantiate first open (type) variable with the given type

`val instantiate : ``LogtkFormula.FO.t -> LogtkFOTerm.t -> LogtkFormula.FO.t`

Instantiate first open variable with the given term

`val clear_var : ``ctx:ctx -> unit`

reset the variable counter (once a formula has been processed)

`val fresh_var : ``ctx:ctx -> int`

Unique index for universal variables

`val update_var : ``ctx:ctx -> LogtkFOTerm.t -> unit`

Avoid collisions with variables of this term in calls to

`LogtkSkolem.fresh_var`

.`val skolem_form : ``ctx:ctx ->`

ty:LogtkType.t -> LogtkFormula.FO.t -> LogtkFormula.FO.t

Skolemize the given formula at root (assumes it occurs just under an
existential quantifier, whose De Bruijn variable 0 is replaced
by a fresh symbol applied to free variables). This also caches symbols,
so that the same formula (modulo alpha-renaming) is always skolemized the
same way.

For instance, `skolem_form ~ctx p(a, b, db0, X)`

will yield
something like `p(a, b, sk42(X), X)`

.

`ty`

: the type of the De Bruijn variable to replacetype`polarity =`

`[ `Both | `Neg | `Pos ]`

`type `

definition = {

` ` |
`form : ` |

` ` |
`proxy : ` |

` ` |
`polarity : ` |

`val has_definition : ``ctx:ctx -> LogtkFormula.FO.t -> bool`

Does this formula already have a definition (in which case it's
very cheap to reduce it to CNF)

`val get_definition : ``ctx:ctx ->`

polarity:polarity -> LogtkFormula.FO.t -> LogtkFormula.FO.t

`rename_form ~ctx f`

returns a (possibly new) predicate for `f`

,
with the free variables of `f`

as arguments. If some other formula
that is alpha-equivalent to `f`

was defined, then the same name is
used. This modifies the context to remember that `f`

has a definition,
and which polarity it is used with.
**NOTE**: we assume no free variable occurs in `f`

. If any such variable
occurs, alpha-equivalent but distinct formulas will have different
names.

**Returns** the atomic formula that stands for `f`

.

`val all_definitions : ``ctx:ctx -> definition Sequence.t`

Definitions that were introduced so far.

`val remove_def : ``ctx:ctx -> definition -> unit`

remove the definition of

`f`

, so that we're sure it will
never be used again`val pop_new_definitions : ``ctx:ctx -> definition list`

List of new definitions, that were introduced since the last
call to

`new_definitions`

. The list can be obtained only once,
after which those definitions are not "new" anymore.
Will call `LogtkSkolem.remove_def`

so there is no risk of re-using a definition
with a new polarity.

`val has_new_definitions : ``ctx:ctx -> bool`

`val skolem_ho : ``ctx:ctx -> ty:LogtkType.t -> LogtkHOTerm.t -> LogtkHOTerm.t`