A Skolem symbol is a witness for an existential property, used in CNF.
Typically, we transform ∃x. p(x) into p(sk_x) where sk_x is a fresh Skolem constant, "witnessing" the existential property.
type type_ = TypedSTerm.ttype term = TypedSTerm.ttype form = TypedSTerm.tval create :
?prefix:string ->
?prop_prefix:string ->
?on_new:(ID.t -> type_ -> unit) ->
unit ->
ctxNew skolem contex. A prefix can be provided, which will be added to all newly created skolem symbols.
used to name skolem functions/constants
used to name sub-formulas during CNF
function called whenever a Skolem symbol is created
Just obtain a fresh skolem symbol. It is also declared in the inner signature.
Remove and return the list of newly created Skolem symbols
val counter : ctx -> intMonotonic counter, increased at every definition
skolem_form ~ctx subst var f returns a term t made of a new symbol applied to the free variables of f that do not occur in subst. This term should replace the variable var, occurring free in f.
For instance, skolem_form ~ctx ø Y p(a, b, Y, X) will yield something like sk42(X).
val pp_polarity : polarity CCFormat.printertype form_definition = private {form : form;proxy_id : ID.t;proxy : term;proxy_ty : type_;rw_rules : bool;polarity : polarity;proof : Proof.step;as_stmt : Statement.input_t list lazy_t;}val pp_form_definition : form_definition CCFormat.printerval define_form :
?pattern:string ->
ctx:ctx ->
rw_rules:bool ->
polarity:polarity ->
parents:Proof.Parent.t list ->
form ->
form_definitiondefine ~ctx f returns a new predicate for f, with the free variables of f as arguments.
the atomic formula that stands for f.
type term_definition = private {td_id : ID.t;td_ty : type_;td_rules : (form, term, type_) Statement.def_rule list;td_as_def : (form, term, type_) Statement.def;td_proof : Proof.step;td_stmt : Statement.input_t list lazy_t;}val define_term :
?pattern:string ->
ctx:ctx ->
parents:Proof.Parent.t list ->
(term list * term) list ->
term_definitiondefine_term l introduces a new function symbol f that is defined by:
args, rhs in l, f args = rhsused to name the new function in an informative way
val pp_definition : definition CCFormat.printerval new_definitions : ctx:ctx -> definition listReturn the new definitions, without side effects
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 def_as_stmt : definition -> Statement.input_t listProject the definition into a list of statements