package dolmen_model

  1. Overview
  2. Docs
type typed_model = Model.t
type parsed_model = Dolmen.Std.Statement.defs list
type 't located = {
  1. contents : 't;
  2. loc : Dolmen.Std.Loc.full;
  3. file : Dolmen_loop.Logic.language Dolmen_loop.State.file;
}
type acc =
  1. | Def of (cst * term) list located
  2. | Hyp of term located
  3. | Goal of term located
  4. | Clause of term list located
type answer =
  1. | None
  2. | Unsat of Dolmen.Std.Loc.full
  3. | Error of Dolmen.Std.Loc.full
  4. | Sat of {
    1. parsed : parsed_model;
    2. model : typed_model;
    3. evaluated_goals : bool located list;
    4. delayed : acc list Dolmen_model.Model.C.t;
    }
  5. | Post_sat
type 'st input =
  1. | Init
  2. | Response_loaded of 'st -> 'st * answer
type 'st t = {
  1. answer : answer;
  2. input : 'st input;
}
val empty : 'a t
module E = Dolmen.Std.Expr
val pp_wrap : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit
val pp_app : Stdlib.Format.formatter -> (E.Term.Const.t * Value.t list) -> unit
val pp_defs_loc : file:Dolmen.Std.Loc.file -> Stdlib.Format.formatter -> Dolmen.Std.Statement.defs -> unit
val pp_located : Stdlib.Format.formatter -> 'a located -> unit
val incr_check_not_supported : unit Dolmen_loop.Report.Error.t
val type_def_in_model : unit Dolmen_loop.Report.Error.t
val bad_model : [ `Clause | `Goals of bool located list | `Hyp ] Dolmen_loop.Report.Error.t
val cannot_check_proofs : unit Dolmen_loop.Report.Warning.t
val error_in_response : unit Dolmen_loop.Report.Error.t
val missing_answer : unit Dolmen_loop.Report.Error.t
val assertion_stack_not_supported : unit Dolmen_loop.Report.Error.t
val fo_model : unit Dolmen_loop.Report.Error.t
val unhandled_float_exponand_and_mantissa : (int * int) Dolmen_loop.Report.Error.t
type 'a file = 'a Dolmen_loop.State.file
OCaml

Innovation. Community. Security.