Module Imandra_surface.Top_result

Top_result: Results of analysis

type 'a printer = Stdlib.Format.formatter -> 'a -> unit
type model_string = string
type callgraph = string lazy_t

graphviz code

type term_model = Term.Model.t

A model represented as terms

type verify_result =
| V_proved of {
proof : Imandra_document.Document.t option;
proof_graph : string lazy_t option;
callgraph : callgraph option;
}
| V_proved_upto of {
callgraph : callgraph option;
upto : Event.upto;
}
| V_refuted of {
model_str : model_string;
model : term_model;
callgraph : callgraph option;
proof : Imandra_document.Document.t option;
}
| V_unknown of {
callgraph : callgraph option;
instances : Imandra_document.Document.t option;
proof : Imandra_document.Document.t option;
reason : string;
}

A simplified view of Verify.t, obtained after verifying a goal

type instance_result =
| I_unsat of {
proof : Imandra_document.Document.t option;
proof_graph : string lazy_t option;
callgraph : callgraph option;
}
| I_unsat_upto of {
callgraph : callgraph option;
upto : Event.upto;
}
| I_sat of {
model_str : model_string;
model : term_model;
callgraph : callgraph option;
proof : Imandra_document.Document.t option;
}
| I_unknown of {
callgraph : callgraph option;
instances : Imandra_document.Document.t option;
proof : Imandra_document.Document.t option;
reason : string;
}
type verify_or_instance_result =
| V of verify_result
| I of instance_result
type modular_region = private Modular_region.t = {
mreg_session : Modular_region.session_id;
mreg_id : Modular_region.id;
mreg_constraints : Term.t list;
mreg_invariant : Term.t;
mreg_args : Var.t list;
mreg_status : Modular_region.status;
}
type modular_decomposition = private Modular_decomposition.t = {
md_session : Modular_decomposition.session_id;
md_f : Uid.t;
md_args : Var.t list;
mutable md_regions : modular_region option Imandra_surface.Modular_decomposition.Id_map.t;
}
type view =
| Modular_decomp of modular_decomposition
| Verify of verify_result
| Instance of instance_result
| Doc of Imandra_document.Document.t
type t

A toplevel result of Imandra analysis algorithms

type simplify_mode =
| Basic
| Dyn_asms

dynamic assumptions for if-then-else

| Full

forward chaining, rewriting, simplify booleans

val force_values_verify_res : verify_result -> unit

remove lazyness

val force_values_instance_res : instance_result -> unit

remove lazyness

remove lazyness

val force_values_verify_or_instance_res : verify_or_instance_result -> unit

remove lazyness

remove lazyness

val force_values : t -> unit

remove lazyness

remove lazyness

val serialize : t Imandra_util.Serialize.t
val view : t -> view
val loc : t -> Imandra_util.Iloc.t option
val set_loc : Imandra_util.Iloc.t -> t -> t
val pp_model_string : model_string printer
val pp_model : term_model printer
val pp_view : view printer
val pp : t printer
val to_string : t -> string
val make : ?⁠loc:Imandra_util.Iloc.t -> view -> t

Make a top result

val make_modular_decomp : ?⁠loc:Imandra_util.Iloc.t -> modular_decomposition -> t
val make_verify : ?⁠loc:Imandra_util.Iloc.t -> verify_result -> t
val make_instance : ?⁠loc:Imandra_util.Iloc.t -> instance_result -> t
val make_doc : ?⁠loc:Imandra_util.Iloc.t -> Imandra_document.Document.t -> t
val serialize : t Imandra_util.Serialize.t
val serialize_l : t list Imandra_util.Serialize.t
val to_doc : t -> Imandra_document.Document.t

Conversion to a document

Toplevel set of results

val push : (unit -> t) -> bool

Push a (lazy) result in the global set. Return true if the document was pushed

val push' : (unit -> t) -> unit
val push_forced : t -> unit
val with_results : (unit -> unit) -> t list

with_results f calls f () and returns all top results produced during its execution. Can be nested on the stack.

val with_capturing_res : (unit -> 'a) -> 'a * t list

Run the function and return its results, also returning any toplevel result produced during the evaluation