Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
(* Type definitions *)type term = Term.ttype location = Loc.ttype defs = Statement.defs
type descr = | Unsat | Sat of defs list option | Error of string
type t = { id : Id.t option; descr : descr; attrs : term list; loc : location;}
let pp_defs = Statement.print_group Statement.print_def
let print_model_opt fmt = function | None -> Format.fprintf fmt "@[<h>no model@]" | Some l -> let pp_sep fmt () = Format.fprintf fmt ",@ " in Format.fprintf fmt "%a" (Format.pp_print_list ~pp_sep pp_defs) l
let print_descr fmt = function | Unsat -> Format.fprintf fmt "unsat" | Sat model_opt -> Format.fprintf fmt "@[<hv 2>sat:@ %a@]" print_model_opt model_opt | Error message -> Format.fprintf fmt "@[<hv 2>error:@ @[<hov>%a@]@]" Format.pp_print_text message
let print_attrs fmt = function | [] -> () | l -> Format.fprintf fmt "@[<hov>{ %a }@]@ " (Format.pp_print_list Term.print) l
let print fmt = function { descr; attrs; _ } -> Format.fprintf fmt "%a%a" print_attrs attrs print_descr descr
let mk ?id ?(loc= Loc.no_loc) ?(attrs=[]) descr = { id; descr; loc; attrs; }
let fun_def ?loc id vars params ret_ty body : defs = Statement.group ~recursive:false [ Statement.def ?loc id ~vars ~params ret_ty body ]
let funs_def_rec ?loc l = let contents = List.map (fun (id, vars, params, ret_ty, body) -> Statement.def ?loc id ~vars ~params ret_ty body ) l in Statement.group ~recursive:true contents
let sat ?loc model = mk ?loc (Sat model)
let unsat ?loc () = mk ?loc Unsat
let error ?loc message = mk ?loc (Error message)