val create :
?ty_prop:LogtkType.t ->
?prefix:string ->
?prop_prefix:string ->
LogtkSignature.t ->
ctxNew skolem contex. A prefix can be provided, which will be added to all newly created skolem symbols.
val to_signature : ctx -> LogtkSignature.tSignature of all new skolem symbols that were created using this context.
val fresh_sym : ctx:ctx -> ty:LogtkType.t -> LogtkSymbol.tJust obtain a fresh skolem symbol. It is also declared in the inner signature.
val fresh_sym_with : ctx:ctx -> ty:LogtkType.t -> string -> LogtkSymbol.tFresh symbol with a different name
val fresh_ty_const : ?prefix:string -> ctx:ctx -> unit -> LogtkSymbol.tNew symbol to be used as a type constant (no need to declare it)
val instantiate_ty : LogtkFormula.FO.t -> LogtkType.t -> LogtkFormula.FO.tInstantiate first open (type) variable with the given type
val instantiate : LogtkFormula.FO.t -> LogtkFOTerm.t -> LogtkFormula.FO.tInstantiate first open variable with the given term
val clear_var : ctx:ctx -> unitreset the variable counter (once a formula has been processed)
val fresh_var : ctx:ctx -> intUnique index for universal variables
val update_var : ctx:ctx -> LogtkFOTerm.t -> unitAvoid collisions with variables of this term in calls to fresh_var.
val skolem_form :
ctx:ctx ->
ty:LogtkType.t ->
LogtkFormula.FO.t ->
LogtkFormula.FO.tSkolemize 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).
type definition = {form : LogtkFormula.FO.t;proxy : LogtkFormula.FO.t;polarity : polarity Pervasives.ref;}val has_definition : ctx:ctx -> LogtkFormula.FO.t -> boolDoes 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.trename_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.
val all_definitions : ctx:ctx -> definition Sequence.tDefinitions that were introduced so far.
val remove_def : ctx:ctx -> definition -> unitremove the definition of f, so that we're sure it will never be used again
val pop_new_definitions : ctx:ctx -> definition listList 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 remove_def so there is no risk of re-using a definition with a new polarity.
val has_new_definitions : ctx:ctx -> boolval clear_skolem_cache : ctx:ctx -> unitForget already skolemized formulas, so that new formulas use different Skolem symbols
val skolem_ho : ctx:ctx -> ty:LogtkType.t -> LogtkHOTerm.t -> LogtkHOTerm.tSkolemize a higher order term. Quite the same as skolem_form. Not implemented