Commit b0ef7adf authored by Sylvain Dailler's avatar Sylvain Dailler

ce: support for if-branching

This adds introduce_premises as a counterexample transformation (to
introduce possible exists quantifications) and add attributes that are
tagged with the special branch_id= to variables directly near it.
parent c8605766
...@@ -218,11 +218,11 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \ ...@@ -218,11 +218,11 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
encoding_sort simplify_array filter_trigger \ encoding_sort simplify_array filter_trigger \
abstraction close_epsilon lift_epsilon \ abstraction close_epsilon lift_epsilon \
eliminate_epsilon intro_projections_counterexmp \ eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \ instantiate_predicate smoke_detector \
prop_curry eliminate_literal \ prop_curry eliminate_literal \
generic_arg_trans_utils case apply subst \ generic_arg_trans_utils case apply subst \
introduction ind_itp destruct cut congruence \ introduction ind_itp destruct cut congruence \
intro_vc_vars_counterexmp prepare_for_counterexmp \
induction induction_pr matching reflection induction induction_pr matching reflection
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\ LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
......
...@@ -5,7 +5,7 @@ module Main ...@@ -5,7 +5,7 @@ module Main
type path_sel_type = { mutable sel_path : bool} type path_sel_type = { mutable sel_path : bool}
val path_selector [@model] [@model_trace:TEMP_NAME]: path_sel_type val path_selector [@model_trace:TEMP_NAME]: path_sel_type
end end
...@@ -19,13 +19,15 @@ module Other ...@@ -19,13 +19,15 @@ module Other
ensures {result = 5} ensures {result = 5}
= =
(* The counterexample should contain the node_id 5454 here but not 121 *) (* The counterexample should contain the node_id 5454 here but not 121 *)
if (([@node_id=5454] path_selector).sel_path <- (a = 1); path_selector.sel_path) then if (path_selector.sel_path <- (a = 1); ([@branch_id=5454] path_selector).sel_path) then
5 5
else else
begin path_selector.sel_path <- true;
(* The counterexample should contain the node_id 121 but not 5454 *) (* The counterexample should contain the node_id 121 but not 5454 *)
if (([@node_id=121] path_selector).sel_path <- (a = 5); path_selector.sel_path) then if (path_selector.sel_path <- (a = 5); ([@branch_id=121] path_selector).sel_path) then
15 15
else else
22 22
end
end end
...@@ -10,11 +10,14 @@ Line 19: ...@@ -10,11 +10,14 @@ Line 19:
result, [[@introduced]] = {"type" : "Integer" , result, [[@introduced]] = {"type" : "Integer" ,
"val" : "15" } "val" : "15" }
Line 22: Line 22:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , [@branch_id=5454]] = {"type" : "Boolean" ,
"val" : false } "val" : false }
Line 26: Line 25:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , "val" : true }
Line 27:
TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@branch_id=121]] = {"type" : "Boolean" ,
"val" : true } "val" : true }
...@@ -10,11 +10,11 @@ Line 19: ...@@ -10,11 +10,11 @@ Line 19:
result, [[@introduced]] = {"type" : "Integer" , result, [[@introduced]] = {"type" : "Integer" ,
"val" : "15" } "val" : "15" }
Line 22: Line 22:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , [@branch_id=5454]] = {"type" : "Boolean" ,
"val" : false } "val" : false }
Line 26: Line 27:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , [@branch_id=121]] = {"type" : "Boolean" ,
"val" : true } "val" : true }
...@@ -10,11 +10,14 @@ Line 19: ...@@ -10,11 +10,14 @@ Line 19:
result, [[@introduced]] = {"type" : "Integer" , result, [[@introduced]] = {"type" : "Integer" ,
"val" : "22" } "val" : "22" }
Line 22: Line 22:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , [@branch_id=5454]] = {"type" : "Boolean" ,
"val" : false } "val" : false }
Line 26: Line 25:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , "val" : true }
Line 27:
TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@branch_id=121]] = {"type" : "Boolean" ,
"val" : false } "val" : false }
...@@ -10,11 +10,11 @@ Line 19: ...@@ -10,11 +10,11 @@ Line 19:
result, [[@introduced]] = {"type" : "Integer" , result, [[@introduced]] = {"type" : "Integer" ,
"val" : "22" } "val" : "22" }
Line 22: Line 22:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , [@branch_id=5454]] = {"type" : "Boolean" ,
"val" : false } "val" : false }
Line 26: Line 27:
TEMP_NAME, [[@introduced], [@model], TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" , [@branch_id=121]] = {"type" : "Boolean" ,
"val" : false } "val" : false }
...@@ -98,6 +98,8 @@ let check_exit_vc_term t in_goal info = ...@@ -98,6 +98,8 @@ let check_exit_vc_term t in_goal info =
(* This is used to update info_labels of info in the printer. This takes the (* This is used to update info_labels of info in the printer. This takes the
label informations present in the term and add a location to help pretty label informations present in the term and add a location to help pretty
printing the counterexamples. printing the counterexamples.
This also takes the information for if_branching "branch_id=" used by API
users.
*) *)
let update_info_labels lsname cur_attrs t ls = let update_info_labels lsname cur_attrs t ls =
let cur_l = let cur_l =
...@@ -118,7 +120,10 @@ let update_info_labels lsname cur_attrs t ls = ...@@ -118,7 +120,10 @@ let update_info_labels lsname cur_attrs t ls =
let attr = create_attribute (attr.attr_string ^ ":loc:" ^ f ^ ":" ^ (string_of_int l)) in let attr = create_attribute (attr.attr_string ^ ":loc:" ^ f ^ ":" ^ (string_of_int l)) in
Sattr.add attr acc Sattr.add attr acc
else else
acc if Strings.has_prefix "branch_id=" attr.attr_string then
Sattr.add attr acc
else
acc
) (Sattr.union t.t_attrs ls.ls_name.id_attrs) cur_l ) (Sattr.union t.t_attrs ls.ls_name.id_attrs) cur_l
in in
Mstr.add lsname updated_attr_labels cur_attrs Mstr.add lsname updated_attr_labels cur_attrs
......
...@@ -260,7 +260,7 @@ let rec print_term info fmt t = ...@@ -260,7 +260,7 @@ let rec print_term info fmt t =
let str_ls = sprintf "%a" (print_ident info) ls.ls_name in let str_ls = sprintf "%a" (print_ident info) ls.ls_name in
let cur_var = info.info_labels in let cur_var = info.info_labels in
let new_var = update_info_labels str_ls cur_var t ls in let new_var = update_info_labels str_ls cur_var t ls in
let () = info.info_labels <- new_var in let () = info.info_labels <- new_var in
let vc_term_info = info.info_vc_term in let vc_term_info = info.info_vc_term in
if vc_term_info.vc_inside then begin if vc_term_info.vc_inside then begin
......
...@@ -33,6 +33,7 @@ let prepare_for_counterexmp2 env task = ...@@ -33,6 +33,7 @@ let prepare_for_counterexmp2 env task =
(* Counter-example will be queried, prepare the task *) (* Counter-example will be queried, prepare the task *)
Debug.dprintf debug "Get ce@."; Debug.dprintf debug "Get ce@.";
let comp_trans = Trans.seq [ let comp_trans = Trans.seq [
Introduction.introduce_premises;
Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp; Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp;
Intro_projections_counterexmp.intro_projections_counterexmp env Intro_projections_counterexmp.intro_projections_counterexmp env
] in ] in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment