Previous  Up  Next

Module FO_rel

module FO_rel: sig .. end

Relational FO Logic

This corresponds, roughly, to Kodkod's logic


Types


type atom_name = ID.t 
type sub_universe = {
   su_name : atom_name;
   su_card : int option;
} 
type atom = {
   a_sub_universe : sub_universe;
   a_index : int;
} 
type tuple = atom list 
type tuple_set = private
| TS_list of tuple list
| TS_product of tuple_set list
| TS_all of sub_universe 
type unop =
| Flip (*
flip p x y <=> p y x
*)
| Trans (*
trans p == transitive closure
*) 
type binop =
| Union
| Inter
| Diff
| Join (*
join (x,y) (y,z) == (x,z)
*)
| Product (*
product (x1,y1) (x2,y2) == (x1,y1,x2,y2)
*) 
type mult =
| M_no
| M_one
| M_lone
| M_some
multiplicity
type expr =
| None_
| Const of ID.t
| Tuple_set of tuple_set
| Var of var
| Unop of unop * expr
| Binop of binop * expr * expr
| If of form * expr * expr
| Comprehension of var * form
| Let of var * expr * expr 
type var_ty = sub_universe 
type var = var_ty Var.t 
type form =
| True
| False
| Eq of expr * expr
| In of expr * expr
| Mult of mult * expr
| Not of form
| And of form list
| Or of form list
| Imply of form * form
| Equiv of form * form
| Forall of var * form
| Exists of var * form
| F_let of var * expr * form
| F_if of form * form * form
| Int_op of int_op * int_expr * int_expr 
type int_op =
| IO_leq 
type int_expr =
| IE_card of expr
| IE_sum of expr
| IE_cst of int 
type decl = {
   decl_id : ID.t;
   decl_arity : int;
   decl_dom : sub_universe list;
   decl_low : tuple_set;
   decl_high : tuple_set;
} 
type universe = {
   univ_prop : sub_universe;
   univ_l : sub_universe list;
}
A universe is a list of sub-universes, each with a different name
type problem = private {
   pb_univ : universe;
   pb_decls : decl ID.Map.t;
   pb_goal : form list;
   pb_meta : ProblemMetadata.t;
}

Helpers


val unop : unop -> expr -> expr
val binop : binop -> expr -> expr -> expr
val mult : mult -> expr -> form
val su_make : ?card:int -> ID.t -> sub_universe
val su_equal : sub_universe -> sub_universe -> bool
val su_hash : sub_universe -> int
val su_compare : sub_universe -> sub_universe -> int
val ts_list : tuple list -> tuple_set
val ts_all : sub_universe -> tuple_set
val ts_product : tuple_set list -> tuple_set
Cartesian product of given tuples
Raises Invalid_argument if the list is empty
val flip : expr -> expr
val trans : expr -> expr
val const : ID.t -> expr
val var : var -> expr
val tuple_set : tuple_set -> expr
val union : expr -> expr -> expr
val inter : expr -> expr -> expr
val diff : expr -> expr -> expr
val join : expr -> expr -> expr
val product : expr -> expr -> expr
val if_ : form -> expr -> expr -> expr
val comprehension : var -> form -> expr
val let_ : var -> expr -> expr -> expr
val true_ : form
val false_ : form
val eq : expr -> expr -> form
val in_ : expr -> expr -> form
val no : expr -> form
expr has no tuples
val one : expr -> form
expr has exactly one tuple
val some : expr -> form
expr has at least one tuple
val not_ : form -> form
val and_ : form -> form -> form
val and_l : form list -> form
val or_ : form -> form -> form
val or_l : form list -> form
val imply : form -> form -> form
val equiv : form -> form -> form
val for_all : var -> form -> form
val for_all_l : var list -> form -> form
val exists : var -> form -> form
val exists_l : var list -> form -> form
val f_let : var -> expr -> form -> form
val f_if : form -> form -> form -> form
val int_op : int_op -> int_expr -> int_expr -> form
val int_leq : int_expr -> int_expr -> form
val int_sum : expr -> int_expr
val int_card : expr -> int_expr
val int_const : int -> int_expr
val atom : sub_universe -> int -> atom
val atom_cmp : atom -> atom -> int
val atom_eq : atom -> atom -> bool
val mk_problem : meta:ProblemMetadata.t ->
       univ:universe ->
       decls:decl ID.Map.t -> goal:form list -> problem

IO


val print_atom : atom CCFormat.printer
val print_tuple : tuple CCFormat.printer
val print_tuple_set : tuple_set CCFormat.printer
val print_sub_universe : sub_universe CCFormat.printer
val print_var_ty : var_ty CCFormat.printer
val print_universe : universe CCFormat.printer
val print_expr : expr CCFormat.printer
val print_int_expr : int_expr CCFormat.printer
val print_form : form CCFormat.printer
val print_decl : decl CCFormat.printer
val print_problem : problem CCFormat.printer