asymetric 'and' and 'or' constructors

parent 4f066431
......@@ -170,7 +170,9 @@ let print_quant fmt = function
| Tforall -> fprintf fmt "forall"
| Texists -> fprintf fmt "exists"
let print_binop fmt = function
let print_binop ~asym fmt = function
| Tand when asym -> fprintf fmt "&&"
| Tor when asym -> fprintf fmt "||"
| Tand -> fprintf fmt "/\\"
| Tor -> fprintf fmt "\\/"
| Timplies -> fprintf fmt "->"
......@@ -259,9 +261,10 @@ and print_tnode pri fmt t = match t.t_node with
| Tfalse ->
fprintf fmt "false"
| Tbinop (b,f1,f2) ->
let asym = List.mem Term.asym_label t.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "%a %a@ %a")
(print_lterm (p + 1)) f1 print_binop b (print_lterm p) f2
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
| Tnot f ->
fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
......
......@@ -41,7 +41,7 @@ val print_ty : formatter -> ty -> unit (* type *)
val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
val print_quant : formatter -> quant -> unit (* quantifier *)
val print_binop : formatter -> binop -> unit (* binary operator *)
val print_binop : asym:bool -> formatter -> binop -> unit (* binary operator *)
val print_const : formatter -> constant -> unit (* int/real constant *)
val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
......
......@@ -737,6 +737,10 @@ let t_or = t_binary Tor
let t_implies = t_binary Timplies
let t_iff = t_binary Tiff
let asym_label = "asym_split"
let t_and_asym t1 t2 = t_label [asym_label] (t_and t1 t2)
let t_or_asym t1 t2 = t_label [asym_label] (t_or t1 t2)
(* closing constructors *)
let t_quant_close q vl tl f =
......@@ -1311,45 +1315,55 @@ let t_not_simp f = match f.t_node with
| Tnot f -> f
| _ -> t_not f
let t_and_simp f1 f2 =
let f12 = t_and f1 f2 in
match f1.t_node, f2.t_node with
let t_and_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ -> f2
| _, Ttrue -> f1
| Tfalse, _ -> f1
| _, Tfalse -> f2
| _, _ -> if t_equal f1 f2 then f1 else f12
| _, _ -> if t_equal f1 f2 then f1 else t_and f1 f2
let t_and_simp_l l = List.fold_left t_and_simp t_true l
let t_or_simp f1 f2 =
let f12 = t_or f1 f2 in
match f1.t_node, f2.t_node with
let t_or_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ -> f1
| _, Ttrue -> f2
| Tfalse, _ -> f2
| _, Tfalse -> f1
| _, _ -> if t_equal f1 f2 then f1 else f12
| _, _ -> if t_equal f1 f2 then f1 else t_or f1 f2
let t_or_simp_l l = List.fold_left t_or_simp t_false l
let t_implies_simp f1 f2 =
let f12 = t_implies f1 f2 in
match f1.t_node, f2.t_node with
let t_and_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ -> f2
| _, Ttrue -> f1
| Tfalse, _ -> f1
| _, Tfalse -> f2
| _, _ -> if t_equal f1 f2 then f1 else t_and_asym f1 f2
let t_and_asym_simp_l l = List.fold_left t_and_asym_simp t_true l
let t_or_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ -> f1
| _, Ttrue -> f2
| Tfalse, _ -> f2
| _, Tfalse -> f1
| _, _ -> if t_equal f1 f2 then f1 else t_or_asym f1 f2
let t_or_asym_simp_l l = List.fold_left t_or_asym_simp t_false l
let t_implies_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ -> f2
| _, Ttrue -> f2
| Tfalse, _ -> t_true
| _, Tfalse -> t_not_simp f1
| _, _ -> if t_equal f1 f2 then t_true else f12
| _, _ -> if t_equal f1 f2 then t_true else t_implies f1 f2
let t_iff_simp f1 f2 =
let f12 = t_iff f1 f2 in
match f1.t_node, f2.t_node with
let t_iff_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ -> f2
| _, Ttrue -> f1
| Tfalse, _ -> t_not_simp f2
| _, Tfalse -> t_not_simp f1
| _, _ -> if t_equal f1 f2 then t_true else f12
| _, _ -> if t_equal f1 f2 then t_true else t_iff f1 f2
let t_binary_simp op = match op with
| Tand -> t_and_simp
......@@ -1357,16 +1371,14 @@ let t_binary_simp op = match op with
| Timplies -> t_implies_simp
| Tiff -> t_iff_simp
let t_if_simp f1 f2 f3 =
let f123 = t_if f1 f2 f3 in
match f1.t_node, f2.t_node, f3.t_node with
let t_if_simp f1 f2 f3 = match f1.t_node, f2.t_node, f3.t_node with
| Ttrue, _, _ -> f2
| Tfalse, _, _ -> f3
| _, Ttrue, _ -> t_implies_simp (t_not_simp f1) f3
| _, Tfalse, _ -> t_and_simp (t_not_simp f1) f3
| _, _, Ttrue -> t_implies_simp f1 f2
| _, _, Tfalse -> t_and_simp f1 f2
| _, _, _ -> if t_equal f2 f3 then f2 else f123
| _, _, _ -> if t_equal f2 f3 then f2 else t_if f1 f2 f3
let small t = match t.t_node with
| Tvar _ | Tconst _ -> true
......
......@@ -230,6 +230,10 @@ val t_not : term -> term
val t_true : term
val t_false : term
val asym_label : label
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term
val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> term -> term
val t_quant_close : quant -> vsymbol list -> trigger -> term -> term
......@@ -256,6 +260,11 @@ val t_implies_simp : term -> term -> term
val t_iff_simp : term -> term -> term
val t_not_simp : term -> term
val t_and_asym_simp : term -> term -> term
val t_and_asym_simp_l : term list -> term
val t_or_asym_simp : term -> term -> term
val t_or_asym_simp_l : term list -> term
val t_let_close_simp : vsymbol -> term -> term -> term
val t_quant_close_simp : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close_simp : vsymbol list -> trigger -> term -> term
......
......@@ -565,11 +565,11 @@ lexpr:
| lexpr OR lexpr
{ infix_pp $1 PPor $3 }
| lexpr BARBAR lexpr
{ mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPor $3)) }
{ mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPor $3)) }
| lexpr AND lexpr
{ infix_pp $1 PPand $3 }
| lexpr AMPAMP lexpr
{ mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPand $3)) }
{ mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPand $3)) }
| NOT lexpr
{ prefix_pp PPnot $2 }
| lexpr EQUAL lexpr
......
......@@ -215,9 +215,10 @@ and print_tnode pri fmt t = match t.t_node with
(print_list comma print_vsty) vl print_tl tl print_term f;
List.iter forget_var vl
| Tbinop (b,f1,f2) ->
let asym = List.mem Term.asym_label t.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "%a %a@ %a")
(print_lterm (p + 1)) f1 print_binop b (print_lterm p) f2
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
| Tnot f ->
fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
| Ttrue ->
......
......@@ -53,20 +53,13 @@ let get_mutable_field ts i =
(* phase 4: weakest preconditions *******************************************)
(* smart constructors for building WPs
TODO: use simp forms / tag with label "WP" *)
TODO: tag with label "WP" *)
let wp_and ?(sym=false) f1 f2 =
(* if sym then t_and_simp f1 f2 else t_and_simp f1 (t_implies_simp f1 f2) *)
let f = t_and_simp f1 f2 in
(* experiment, but does not work
let f = t_label_add Split_goal.stop_split f in
*)
match f.t_node with
| Tbinop (Tand, _, _) when not sym -> t_label_add Split_goal.asym_split f
| _ -> f
if sym then t_and_simp f1 f2 else t_and_asym_simp f1 f2
let wp_ands ?(sym=false) fl =
List.fold_left (wp_and ~sym) t_true fl
if sym then t_and_simp_l fl else t_and_asym_simp_l fl
let wp_implies f1 f2 = match f2.t_node with
| Tfalse -> t_implies f1 f2
......
......@@ -40,7 +40,7 @@ let split_case forig spl c acc tl bl =
let fn bl = t_label_copy forig (t_case tl bl) in
apply_append fn acc bll
let asym_split = "asym_split"
let asym_split = Term.asym_label
let stop_split = "stop_split"
let asym f = List.mem asym_split f.t_label
......
......@@ -17,7 +17,6 @@
(* *)
(**************************************************************************)
val asym_split : Ident.label
val stop_split : Ident.label
val split_pos : Term.term -> Term.term list
......
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