diff options
| author | Brian Campbell | 2019-06-12 17:25:47 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-06-13 18:03:07 +0100 |
| commit | d2f702da3b5cc9934f8cd3ea457f93c6ce2b6c12 (patch) | |
| tree | b20fb23cb690571bdbdf28b6f8694cb44c8f7d63 /src/slice.ml | |
| parent | 4b83ad134a472159f730a015187f036104ff35fd (diff) | |
Add AST for greater-than and less-than constraints
Mostly to make constraints sent to the SMT solver and Coq nicer, but
also makes it easy to remove uninformative constraints in the Coq
back-end.
Diffstat (limited to 'src/slice.ml')
| -rw-r--r-- | src/slice.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/slice.ml b/src/slice.ml index 9dee4761..1bbbca1e 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -104,7 +104,7 @@ let builtins = let rec constraint_ids' (NC_aux (aux, _)) = match aux with - | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_not_equal (n1, n2) -> + | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_lt (n1, n2) | NC_bounded_gt (n1, n2) | NC_not_equal (n1, n2) -> IdSet.union (nexp_ids' n1) (nexp_ids' n2) | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> IdSet.union (constraint_ids' nc1) (constraint_ids' nc2) |