Module Logtk.Statement

Statement

The input problem is made of statements. Each statement can declare a type, assert a formula, or a conjecture, define a term, add a rewrite rule, etc.

Those statements do not necessarily reflect exactly statements in the input language(s) (e.g., TPTP).

type 'ty data = {
  1. data_id : ID.t;
    (*

    Name of the type

    *)
  2. data_args : 'ty Var.t list;
    (*

    type parameters

    *)
  3. data_ty : 'ty;
    (*

    type of Id, that is, type -> type -> ... -> type

    *)
  4. data_cstors : (ID.t * 'ty * ('ty * (ID.t * 'ty)) list) list;
    (*

    Each constructor is id, ty, args. ty must be of the form ty1 -> ty2 -> ... -> id args. args has the form (ty1, p1), (ty2,p2), … where each p is a projector.

    *)
}

A datatype declaration

type attr =
  1. | A_AC
  2. | A_infix of string
  3. | A_prefix of string
  4. | A_sos
    (*

    set of support

    *)
type attrs = attr list
type 'ty skolem = ID.t * 'ty
type polarity = [
  1. | `Equiv
  2. | `Imply
]

polarity for rewrite rules

type ('f, 't, 'ty) def_rule =
  1. | Def_term of {
    1. vars : 'ty Var.t list;
    2. id : ID.t;
    3. ty : 'ty;
    4. args : 't list;
    5. rhs : 't;
    6. as_form : 'f;
    }
    (*

    forall vars, id args = rhs

    *)
  2. | Def_form of {
    1. vars : 'ty Var.t list;
    2. lhs : 't SLiteral.t;
    3. rhs : 'f list;
    4. polarity : polarity;
    5. as_form : 'f list;
    }
    (*

    forall vars, lhs op bigand rhs where op depends on polarity (in {=>, <=>, <=})

    *)
type ('f, 't, 'ty) def = {
  1. def_id : ID.t;
  2. def_ty : 'ty;
  3. def_rules : ('f, 't, 'ty) def_rule list;
  4. def_rewrite : bool;
}
type ('f, 't, 'ty) view =
  1. | TyDecl of ID.t * 'ty
    (*

    id: ty

    *)
  2. | Data of 'ty data list
  3. | Def of ('f, 't, 'ty) def list
  4. | Rewrite of ('f, 't, 'ty) def_rule
  5. | Assert of 'f
    (*

    assert form

    *)
  6. | Lemma of 'f list
    (*

    lemma to prove and use, using Avatar cut

    *)
  7. | Goal of 'f
    (*

    goal to prove

    *)
  8. | NegatedGoal of 'ty skolem list * 'f list
    (*

    goal after negation, with skolems

    *)
type lit = Term.t SLiteral.t
type formula = TypedSTerm.t
type clause = lit list
type ('f, 't, 'ty) t = private {
  1. id : int;
  2. view : ('f, 't, 'ty) view;
  3. attrs : attrs;
  4. proof : proof;
  5. mutable name : string option;
}
and proof = Proof.Step.t
and clause_t = (clause, Term.t, Type.t) t
val compare : (_, _, _) t -> (_, _, _) t -> int
val view : ('f, 't, 'ty) t -> ('f, 't, 'ty) view
val attrs : (_, _, _) t -> attrs
val proof_step : (_, _, _) t -> proof
val name : (_, _, _) t -> string

Retrieve a name from the proof, or generate+save a new one

val as_proof_i : input_t -> Proof.t
val res_tc_i : input_t Proof.result_tc
val as_proof_c : clause_t -> Proof.t
val res_tc_c : clause_t Proof.result_tc
val mk_data : ID.t -> args:'ty Var.t list -> 'ty -> (ID.t * 'ty * ('ty * (ID.t * 'ty)) list) list -> 'ty data
val mk_def : ?rewrite:bool -> ID.t -> 'ty -> ('f, 't, 'ty) def_rule list -> ('f, 't, 'ty) def
val attrs_ua : (_, _, _) t -> UntypedAST.attrs

All attributes, included these in the proof

val ty_decl : ?attrs:attrs -> proof:proof -> ID.t -> 'ty -> (_, _, 'ty) t
val def : ?attrs:attrs -> proof:proof -> ('f, 't, 'ty) def list -> ('f, 't, 'ty) t
val rewrite : ?attrs:attrs -> proof:proof -> ('f, 't, 'ty) def_rule -> ('f, 't, 'ty) t
val data : ?attrs:attrs -> proof:proof -> 'ty data list -> (_, _, 'ty) t
val assert_ : ?attrs:attrs -> proof:proof -> 'f -> ('f, _, _) t
val lemma : ?attrs:attrs -> proof:proof -> 'f list -> ('f, _, _) t
val goal : ?attrs:attrs -> proof:proof -> 'f -> ('f, _, _) t
val neg_goal : ?attrs:attrs -> proof:proof -> skolems:'ty skolem list -> 'f list -> ('f, _, 'ty) t
val signature : ?init:Signature.t -> ?conj_syms:ID.t Iter.t -> (_, _, Type.t) t Iter.t -> Signature.t

Compute signature when the types are using Type

val conv_attrs : UntypedAST.attrs -> attrs
val attr_to_ua : attr -> UntypedAST.attr
val map_data : ty:('ty1 -> 'ty2) -> 'ty1 data -> 'ty2 data
val map_def : form:('f1 -> 'f2) -> term:('t1 -> 't2) -> ty:('ty1 -> 'ty2) -> ('f1, 't1, 'ty1) def -> ('f2, 't2, 'ty2) def
val map_def_rule : form:('a -> 'b) -> term:('c -> 'd) -> ty:('e -> 'f) -> ('a, 'c, 'e) def_rule -> ('b, 'd, 'f) def_rule
val map : form:('f1 -> 'f2) -> term:('t1 -> 't2) -> ty:('ty1 -> 'ty2) -> ('f1, 't1, 'ty1) t -> ('f2, 't2, 'ty2) t

Defined Constants

type definition = Rewrite.rule_set
val as_defined_cst : ID.t -> (int * definition) option

as_defined_cst id returns Some level if id is a constant defined at stratification level level, None otherwise

val as_defined_cst_level : ID.t -> int option
val is_defined_cst : ID.t -> bool
val declare_defined_cst : ID.t -> level:int -> definition -> unit

declare_defined_cst id ~level states that id is a defined constant of given level. It means that it is defined based only on constants of strictly lower levels

val scan_stmt_for_defined_cst : clause_t -> unit

Try and declare defined constants in the given statement

val scan_tst_rewrite : input_t -> unit

Inductive Types

val scan_stmt_for_ind_ty : clause_t -> unit

scan_stmt_for_ind_ty stmt examines stmt, and, if the statement is a declaration of inductive types or constants, it declares them using declare_ty or declare_inductive_constant.

val scan_simple_stmt_for_ind_ty : input_t -> unit

Same as scan_stmt but on earlier statements

val get_rw_rule : ?weight_incr:int -> clause_t -> (ID.Set.elt * Rewrite.rule) option
val get_formulas_from_defs : ('a, _, _) t -> 'a CCList.t
val sine_axiom_selector : ?ignore_k_most_common_symbols:int option -> ?take_conj_defs:bool -> ?take_only_defs:bool -> ?trim_implications:bool -> ?depth_start:int -> ?depth_end:int -> ?tolerance:float -> input_t Iter.t -> input_t Iter.t

Implementation of SinE algorithm with the usual parameters described in Hoder and Voronkov Sine Qua Non paper

Iterators

module Seq : sig ... end

IO

val pp_def_rule : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) def_rule CCFormat.printer
val pp_def : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) def CCFormat.printer
val pp : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) t CCFormat.printer
val to_string : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) t -> string
val pp_clause : clause_t CCFormat.printer
val pp_input : input_t CCFormat.printer
module ZF : sig ... end
module TPTP : sig ... end