Commit 3d3dc3f6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Simplify code by using the relative sign of formulas rather than their absolute one.

Clarify documentation.
parent 030ec924
...@@ -46,7 +46,7 @@ let () = ...@@ -46,7 +46,7 @@ let () =
(fun t _ -> match t.t_node with (fun t _ -> match t.t_node with
| Tconst _ | Tapp(_,[]) -> false | Tconst _ | Tapp(_,[]) -> false
| Tapp(ls,_) -> not (check_ls ls) | Tapp(ls,_) -> not (check_ls ls)
| _ -> true) true f) | _ -> true) f)
]))) ])))
(* Gappa pre-compilation *) (* Gappa pre-compilation *)
......
...@@ -140,9 +140,8 @@ let () = Trans.register_transform ...@@ -140,9 +140,8 @@ let () = Trans.register_transform
(** linearize all the subformulas with the given connector (conj/disj); (** linearize all the subformulas with the given connector (conj/disj);
the returned array also contains the sign of each subformula *) the returned array also contains the sign of each subformula *)
let fmla_flatten conj sign f = let fmla_flatten conj f =
let terms = ref [] in let terms = ref [] in
let conj = (conj = sign) in
let rec aux sign f = let rec aux sign f =
match f.f_node with match f.f_node with
| Fnot f -> aux (not sign) f | Fnot f -> aux (not sign) f
...@@ -153,13 +152,12 @@ let fmla_flatten conj sign f = ...@@ -153,13 +152,12 @@ let fmla_flatten conj sign f =
| Fbinop (Fimplies, f1, f2) when sign <> conj -> | Fbinop (Fimplies, f1, f2) when sign <> conj ->
aux sign f2; aux (not sign) f1 aux sign f2; aux (not sign) f1
| _ -> terms := (f, sign)::!terms in | _ -> terms := (f, sign)::!terms in
aux sign f; aux true f;
Array.of_list !terms Array.of_list !terms
(** recreate the structure of a given formula with linearized subformulas *) (** recreate the structure of a given formula with linearized subformulas *)
let fmla_unflatten conj sign f formulas = let fmla_unflatten conj f formulas =
let i = ref 0 in let i = ref 0 in
let conj = (conj = sign) in
let rec aux sign f = f_label_copy f (match f.f_node with let rec aux sign f = f_label_copy f (match f.f_node with
| Fnot f -> f_not (aux (not sign) f) | Fnot f -> f_not (aux (not sign) f)
| Fbinop (For, f1, f2) when sign <> conj -> | Fbinop (For, f1, f2) when sign <> conj ->
...@@ -173,29 +171,29 @@ let fmla_unflatten conj sign f formulas = ...@@ -173,29 +171,29 @@ let fmla_unflatten conj sign f formulas =
assert (sign = s); assert (sign = s);
incr i; incr i;
t) in t) in
aux sign f aux true f
(** substitute all the terms that appear as a side of an equality/disequality (** substitute all the terms that appear as a side of an equality/disequality
and that match the given filter and that match the given filter
in a positive formula, equal terms can be substituted in all the terms of equal terms can be substituted in all the terms of surrounding
surrounding conjunctions, while disequal terms can be substituted in conjunctions, while disequal terms can be substituted in all the terms
all the terms of surrounding disjunctions of surrounding disjunctions
substitutions are not exported outside quantifiers (even if their free substitutions are not exported outside quantifiers (even if their free
variables are untouched), so the transformation is possibly incomplete variables are untouched), so the transformation is possibly incomplete
(but still correct) on formulas that have inner quantifiers *) (but still correct) on formulas that have inner quantifiers *)
let rec fmla_cond_subst filter sign f = let rec fmla_cond_subst filter f =
let rec aux sign f = let rec aux f =
match f.f_node with match f.f_node with
| Fbinop (o, _, _) when o <> Fiff -> | Fbinop (o, _, _) when o <> Fiff ->
let conj = match o with let conj = match o with
Fand -> true | For | Fimplies -> false | Fiff -> assert false in Fand -> true | For | Fimplies -> false | Fiff -> assert false in
let subf = fmla_flatten conj sign f in let subf = fmla_flatten conj f in
let subl = Array.length subf in let subl = Array.length subf in
for i = 0 to subl - 1 do for i = 0 to subl - 1 do
let (f, s) = subf.(i) in let (f, s) = subf.(i) in
subf.(i) <- (aux s f, s); subf.(i) <- (aux f, s);
done; done;
for i = 0 to subl - 1 do for i = 0 to subl - 1 do
let do_subst t1 t2 = let do_subst t1 t2 =
...@@ -206,11 +204,11 @@ let rec fmla_cond_subst filter sign f = ...@@ -206,11 +204,11 @@ let rec fmla_cond_subst filter sign f =
done in done in
let (f, s) = subf.(i) in let (f, s) = subf.(i) in
match f.f_node with match f.f_node with
| Fapp (ls,[t1;t2]) when ls_equal ls ps_equ && s = (conj = sign) -> | Fapp (ls,[t1;t2]) when ls_equal ls ps_equ && s = conj ->
if filter t1 t2 then do_subst t1 t2 else if filter t1 t2 then do_subst t1 t2 else
if filter t2 t1 then do_subst t2 t1 if filter t2 t1 then do_subst t2 t1
| _ -> () | _ -> ()
done; done;
fmla_unflatten conj sign f subf fmla_unflatten conj f subf
| _ -> f_map_sign (fun t -> t) aux sign f in | _ -> f_map (fun t -> t) aux f in
aux sign f aux f
...@@ -27,8 +27,8 @@ val fmla_remove_quant : Term.fmla -> Term.fmla ...@@ -27,8 +27,8 @@ val fmla_remove_quant : Term.fmla -> Term.fmla
and \forall x. x <> y \/ F into F[y/x] *) and \forall x. x <> y \/ F into F[y/x] *)
val fmla_cond_subst : (Term.term -> Term.term -> bool) -> val fmla_cond_subst : (Term.term -> Term.term -> bool) ->
bool -> Term.fmla -> Term.fmla Term.fmla -> Term.fmla
(** given a formula [f] (with positivity [sign]) containing some equality (** given a formula [f] containing some equality or disequality [t1] ?= [t2]
or disequality [t1] ?= [t2] such that [filter t1 t2] evaluates to true, such that [filter t1 t2] (resp [filter t2 t1]) evaluates to true,
[fmla_subst_cond filter sign f] performs the substitution [t1] -> [t2] [fmla_subst_cond filter f] performs the substitution [t1] -> [t2]
wherever possible and returns an equivalent formula *) (resp [t2] -> [t1]) wherever possible and returns an equivalent formula *)
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