Commit 8983327a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve the heuristic for performing substitutions in the Gappa driver.

The original idea was to replace t1 by t2 only when t1 is more complicated
than t2, which was implemented by saying that t1 is neither a variable nor
a constant. Unfortunately, it means that no substitution happens when both
t1 and t2 are variables and/or constants. This patch fixes it.
parent 796da2b5
...@@ -44,8 +44,13 @@ let () = ...@@ -44,8 +44,13 @@ let () =
Trans.register_transform "simplify_unknown_lsymbols" Trans.register_transform "simplify_unknown_lsymbols"
(syntactic_transform (fun check_ls -> Trans.goal (fun pr f -> (syntactic_transform (fun check_ls -> Trans.goal (fun pr f ->
[create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst [create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst
(fun t _ -> match t.t_node with (fun t1 t2 -> match t1.t_node with
| Tconst _ | Tapp(_,[]) -> false | Tconst _ -> false
| Tapp(_,[]) ->
begin match t2.t_node with
| Tconst _ | Tapp(_,[]) -> true
| _ -> false
end
| Tapp(ls,_) -> not (check_ls ls) | Tapp(ls,_) -> not (check_ls ls)
| _ -> true) f) | _ -> true) f)
]))) ])))
......
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