diff options
| author | Alasdair Armstrong | 2019-01-08 17:08:34 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-01-08 17:11:48 +0000 |
| commit | eb837a0ae70ef5dc8a2a3a28d59a736c57a952b3 (patch) | |
| tree | 96f3fcfde01cc6798d00c969be4363c2bf055b38 /src/rewrites.ml | |
| parent | 36d876fd74d8fdcb9bb54a4c0aa220f0ab14e5da (diff) | |
Improvements for v85
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 9f082f49..7536edf4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2274,25 +2274,29 @@ let rewrite_fix_val_specs (Defs defs) = (* Turn constraints into numeric expressions with sizeof *) let rewrite_constraint = - let rec rewrite_nc (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux nc_aux) - and rewrite_nc_aux = function + let rec rewrite_nc env (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux l env nc_aux) + and rewrite_nc_aux l env = function | NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2)) | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "<=", mk_exp (E_sizeof n2)) | NC_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2)) | NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2)) - | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2) - | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2) + | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc env nc1, mk_id "&", rewrite_nc env nc2) + | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc env nc1, mk_id "|", rewrite_nc env nc2) | NC_false -> E_lit (mk_lit L_false) | NC_true -> E_lit (mk_lit L_true) | NC_set (kid, []) -> E_lit (mk_lit (L_false)) | NC_set (kid, int :: ints) -> let kid_eq kid int = nc_eq (nvar kid) (nconstant int) in - unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints)) + unaux_exp (rewrite_nc env (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints)) + | NC_app (f, args) -> + unaux_exp (rewrite_nc env (Env.expand_constraint_synonyms env (mk_nc (NC_app (f, args))))) + | NC_var v -> + Reporting.unreachable l __POS__ "Cannot rewrite this constraint" in let rewrite_e_aux (E_aux (e_aux, _) as exp) = match e_aux with | E_constraint nc -> - check_exp (env_of exp) (rewrite_nc nc) bool_typ + check_exp (env_of exp) (rewrite_nc (env_of exp) nc) bool_typ | _ -> exp in |