sig
type rac_result_state =
Res_normal
| Res_fail of Pinterp_core.cntr_ctx * Term.term
| Res_stuck of string
| Res_incomplete of string
val print_rac_result_state : Check_ce.rac_result_state Pp.pp
type rac_result =
RAC_not_done of string
| RAC_done of Check_ce.rac_result_state * Pinterp_core.Log.exec_log
val string_of_rac_result_state : Check_ce.rac_result_state -> string
val print_rac_result : ?verb_lvl:int -> Check_ce.rac_result Pp.pp
val print_dbg_rac_result_model :
print_normal:bool ->
print_giant:bool ->
int option ->
(int * 'a * 'b * Check_ce.rac_result * Check_ce.rac_result) Pp.pp
val rac_execute :
Pinterp.ctx ->
Expr.rsymbol -> Check_ce.rac_result_state * Pinterp_core.Log.exec_log
val oracle_of_model :
Pdecl.known_map -> Model_parser.model -> Pinterp_core.oracle
val model_of_exec_log :
env:Env.env ->
known_map:Decl.known_map ->
prover_model:Model_parser.model ->
Pinterp_core.Log.exec_log -> Model_parser.model
type verdict = NC | SW | NC_SW | BAD_CE of string | INCOMPLETE of string
val string_of_verdict : Check_ce.verdict -> string
type classification = Check_ce.verdict * Pinterp_core.Log.exec_log
val report_verdict : Env.env -> Check_ce.classification Pp.pp
val print_classification_log_or_model :
?verb_lvl:int ->
json:bool ->
print_attrs:bool -> (Model_parser.model * Check_ce.classification) Pp.pp
val print_model_classification :
?verb_lvl:int ->
json:bool ->
Env.env -> (Model_parser.model * Check_ce.classification) Pp.pp
val classify :
vc_term_loc:Loc.position option ->
vc_term_attrs:Ident.Sattr.t ->
normal_result:Check_ce.rac_result_state * Pinterp_core.Log.exec_log ->
giant_step_result:Check_ce.rac_result_state * Pinterp_core.Log.exec_log ->
Check_ce.classification
val models_from_rac :
limits:Call_provers.resource_limits ->
?verb_lvl:int ->
?compute_term:Pinterp_core.compute_term ->
Pinterp_core.rac ->
Env.env ->
Pmodule.pmodule ->
(Call_provers.prover_answer * Model_parser.model) list ->
(Model_parser.model * Check_ce.rac_result * Check_ce.rac_result *
Check_ce.classification)
list
val models_from_giant_step :
limits:Call_provers.resource_limits ->
?verb_lvl:int ->
?compute_term:Pinterp_core.compute_term ->
Pinterp_core.rac ->
Env.env ->
Pmodule.pmodule ->
(Call_provers.prover_answer * Model_parser.model) list ->
(Model_parser.model * Check_ce.rac_result) list
val best_rac_result :
(Model_parser.model * Check_ce.rac_result * Check_ce.rac_result *
Check_ce.classification)
list -> (Model_parser.model * Check_ce.classification) option
val best_giant_step_result :
(Model_parser.model * Check_ce.rac_result) list ->
(Model_parser.model * Check_ce.rac_result) option
val last_nonempty_model :
env:Env.env ->
known_map:Decl.known_map ->
(Call_provers.prover_answer * Model_parser.model) list ->
Model_parser.model option
val debug_check_ce_rac_results : Debug.flag
val debug_check_ce_categorization : Debug.flag
val warn_concrete_term : Loc.warning_id
end