Module Logtk.SkolemSource

Skolem symbols

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.

Sourcetype type_ = TypedSTerm.t
Sourcetype term = TypedSTerm.t
Sourcetype form = TypedSTerm.t
Sourcetype ctx

Context needed to create new symbols

Sourceval create : ?prefix:string -> ?prop_prefix:string -> ?on_new:(ID.t -> type_ -> unit) -> unit -> ctx

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

  • parameter prefix

    used to name skolem functions/constants

  • parameter prop_prefix

    used to name sub-formulas during CNF

  • parameter on_id

    function called whenever a Skolem symbol is created

Sourceval fresh_skolem : ctx:ctx -> ty:type_ -> vars_count:int -> ID.t

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

Sourceval fresh_skolem_prefix : ctx:ctx -> ty:type_ -> vars_count:int -> string -> ID.t

Fresh symbol with a different name

Sourceval pop_new_skolem_symbols : ctx:ctx -> (ID.t * type_) list

Remove and return the list of newly created Skolem symbols

Sourceval counter : ctx -> int

Monotonic counter, increased at every definition

Skolemization

Sourceval skolem_form : ctx:ctx -> (type_, term) Var.Subst.t -> type_ Var.t -> form -> term

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).

Definitions of Formulas

Sourcetype polarity = [
  1. | `Pos
  2. | `Neg
  3. | `Both
]
Sourcetype form_definition = private {
  1. form : form;
  2. proxy_id : ID.t;
  3. proxy : term;
  4. proxy_ty : type_;
  5. rw_rules : bool;
  6. polarity : polarity;
  7. proof : Proof.step;
  8. as_stmt : Statement.input_t list lazy_t;
}
Sourceval pp_form_definition : form_definition CCFormat.printer
Sourceval define_form : ?pattern:string -> ctx:ctx -> rw_rules:bool -> polarity:polarity -> parents:Proof.Parent.t list -> form -> form_definition

define ~ctx f returns a new predicate for f, with the free variables of f as arguments.

  • returns

    the atomic formula that stands for f.

Sourcetype term_definition = private {
  1. td_id : ID.t;
  2. td_ty : type_;
  3. td_rules : (form, term, type_) Statement.def_rule list;
  4. td_as_def : (form, term, type_) Statement.def;
  5. td_proof : Proof.step;
  6. td_stmt : Statement.input_t list lazy_t;
}
Sourceval define_term : ?pattern:string -> ctx:ctx -> parents:Proof.Parent.t list -> (term list * term) list -> term_definition

define_term l introduces a new function symbol f that is defined by:

  • for each args, rhs in l, f args = rhs
  • parameter pattern

    used to name the new function in an informative way

Sourcetype definition =
  1. | Def_form of form_definition
  2. | Def_term of term_definition
Sourceval new_definitions : ctx:ctx -> definition list

Return the new definitions, without side effects

Sourceval 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 remove_def so there is no risk of re-using a definition with a new polarity.

Sourceval def_as_stmt : definition -> Statement.input_t list

Project the definition into a list of statements

Attribute