diff options
| author | Vincent Laporte | 2021-04-14 15:20:43 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2021-04-14 15:20:43 +0200 |
| commit | 90a6c01dec9d58fa409e7097ac5ba03f08a9ae7b (patch) | |
| tree | 77260cc386ae0eafcbfec1d2a862f9e721e56b34 /plugins/micromega/certificate.ml | |
| parent | ea62d1e19f2ba565ea3a18ba3709a06af5c845ac (diff) | |
| parent | 8193ca191cc435c108a4842ae38a11d74c7c20a5 (diff) | |
Merge PR #14045: Zify: more aggressive application of saturation rules
Reviewed-by: vbgl
Diffstat (limited to 'plugins/micromega/certificate.ml')
| -rw-r--r-- | plugins/micromega/certificate.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 53aa619d10..1018271751 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -449,6 +449,8 @@ let bound_monomials (sys : WithProof.t list) = in List.map snd (List.filter has_mon bounds) @ snd l +let bound_monomials = tr_sys "bound_monomials" bound_monomials + let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); max_nb_cstr := compute_max_nb_cstr sys prfdepth; @@ -1181,10 +1183,12 @@ let nlia enum prfdepth sys = It would only be safe if the variable is linear... *) let sys1 = - elim_simple_linear_equality (WithProof.subst_constant true sys) + normalise + (elim_simple_linear_equality (WithProof.subst_constant true sys)) in + let bnd1 = bound_monomials sys1 in let sys2 = saturate_by_linear_equalities sys1 in - let sys3 = nlinear_preprocess (sys1 @ sys2) in + let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in let sys4 = make_cstr_system (*sys2@*) sys3 in (* [reduction_equations] is too brutal - there should be some non-linear reasoning *) xlia (List.map fst sys) enum reduction_equations sys4 |