dolmen_model 0.9 · OCaml Package

type typed_model = Model.t

type parsed_model = Dolmen.Std.Statement.defs list

type cst = Dolmen.Std.Expr.term_cst

type term = Dolmen.Std.Expr.Term.t

type 't located = {

contents : 't;
loc : Dolmen.Std.Loc.full;
file : Dolmen_loop.Logic.language Dolmen_loop.State.file;

}

type acc =

| Def of (cst * term) list located
| Hyp of term located
| Goal of term located
| Clause of term list located

type answer =

| None
| Unsat of Dolmen.Std.Loc.full
| Error of Dolmen.Std.Loc.full
| Sat of {
1. parsed : parsed_model;
2. model : typed_model;
3. evaluated_goals : bool located list;
4. delayed : acc list Model.C.t;
}
| Post_sat

type 'st input =

| Init
| Response_loaded of 'st -> 'st * answer

type 'st t = {

answer : answer;
input : 'st input;

}

val empty : 'a t

val file_loc_of_acc : 
  acc ->
  Dolmen_loop.Logic.language Dolmen_loop.State.file * Dolmen.Std.Loc.full

module E = Dolmen.Std.Expr

val pp_wrap : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a ->
  unit

val pp_app : Format.formatter -> (E.Term.Const.t * Value.t list) -> unit

val pp_defs_loc : 
  file:Dolmen.Std.Loc.file ->
  Format.formatter ->
  Dolmen.Std.Statement.defs ->
  unit

val pp_located : Format.formatter -> 'a located -> unit

val code : Dolmen_loop.Code.t

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 parsed_model : 
  (Dolmen.Std.Loc.file * Dolmen.Std.Statement.defs list)
    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 undefined_variable : Dolmen.Std.Expr.Term.Var.t Dolmen_loop.Report.Error.t

val undefined_constant : 
  Dolmen.Std.Expr.Term.Const.t Dolmen_loop.Report.Error.t

val unhandled_builtin : Dolmen.Std.Expr.Term.Const.t Dolmen_loop.Report.Error.t

val partial_interpretation : 
  (Dolmen.Std.Expr.Term.Const.t * Value.t list) Dolmen_loop.Report.Error.t

val bad_extension : 
  (Dolmen.Std.Expr.Term.Const.t * Value.t list * Value.t)
    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

module Make
  (State : Dolmen_loop.State.S)
  (Parse : 
    Dolmen_loop.Parser.S
      with type state := State.t
       and type 'a key := 'a State.key)
  (Typer : 
    Dolmen_loop.Typer.Typer_Full
      with type state := State.t
       and type 'a key := 'a State.key
       and type ty_state := Dolmen_loop.Typer.ty_state
       and type env = Dolmen_loop.Typer.T.env)
  (Typer_Pipe : 
    Dolmen_loop.Typer.S
      with type state := State.t
       and type env = Typer.env
       and type 'a key := 'a State.key
       and type ty := Dolmen.Std.Expr.ty
       and type ty_var := Dolmen.Std.Expr.ty_var
       and type ty_cst := Dolmen.Std.Expr.ty_cst
       and type ty_def := Dolmen.Std.Expr.ty_def
       and type term := Dolmen.Std.Expr.term
       and type term_var := Dolmen.Std.Expr.term_var
       and type term_cst := Dolmen.Std.Expr.term_cst
       and type formula := Dolmen.Std.Expr.formula) : 
  sig ... end

package dolmen_model