Module Logtk.Statement

Statement

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

Name of the type

data_args : 'ty Var.t list;

type parameters

data_ty : 'ty;

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

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 =
| A_AC
| A_infix of string
| A_prefix of string
| A_sos

set of support

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

polarity for rewrite rules

type ('f, 't, 'ty) def_rule =
| Def_term of {
vars : 'ty Var.t list;
id : ID.t;
ty : 'ty;
args : 't list;
rhs : 't;
as_form : 'f;
}

forall vars, id args = rhs

| Def_form of {
vars : 'ty Var.t list;
lhs : 't SLiteral.t;
rhs : 'f list;
polarity : polarity;
as_form : 'f list;
}

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

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

id: ty

| Data of 'ty data list
| Def of ('f, 't, 'ty) def list
| Rewrite of ('f, 't, 'ty) def_rule
| Assert of 'f

assert form

| Lemma of 'f list

lemma to prove and use, using Avatar cut

| Goal of 'f

goal to prove

| NegatedGoal of 'ty skolem list * 'f list

goal after negation, with skolems

type lit = Term.t SLiteral.t
type formula = TypedSTerm.t
type input_def = (TypedSTerm.t, TypedSTerm.t, TypedSTerm.t) def
type clause = lit list
type ('f, 't, 'ty) t = private {
id : int;
view : ('f, 't, 'ty) view;
attrs : attrs;
proof : proof;
mutable name : string option;
}
and proof = Proof.Step.t
and input_t = (TypedSTerm.t, TypedSTerm.t, TypedSTerm.t) 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 -> (Logtk.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
val pp_clause_in : Output_format.t -> clause_t CCFormat.printer
val pp_input_in : Output_format.t -> input_t CCFormat.printer