diff options
| author | Robert Norton | 2018-11-15 15:13:06 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-11-15 15:13:06 +0000 |
| commit | c631ae96bbe9d659a8b3dbb1fc0c7ac812c2d43f (patch) | |
| tree | ebb2ac2f4a1159b45a5fb41fd3212b499d1c68cb /src | |
| parent | 5f00f0d75cfaabb89f2ec22115392443539664bd (diff) | |
ast_utils: simplify numeric constraints in inequalities.
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index f0b6508b..71b3299a 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -296,7 +296,10 @@ let rec constraint_simp (NC_aux (nc_aux, l)) = | NC_aux (nc, _), NC_aux (NC_true, _) -> NC_true | _, _ -> NC_or (nc1, nc2) end - + | NC_bounded_ge (nexp1, nexp2) -> + NC_bounded_ge (nexp_simp nexp1, nexp_simp nexp2) + | NC_bounded_le (nexp1, nexp2) -> + NC_bounded_le (nexp_simp nexp1, nexp_simp nexp2) | _ -> nc_aux in NC_aux (nc_aux, l) |