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/specialize.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/specialize.ml')
| -rw-r--r-- | src/specialize.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/specialize.ml b/src/specialize.ml index 815514d1..d749bc53 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -186,7 +186,9 @@ let string_of_instantiation instantiation = | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_gt (n1, n2), _) -> string_of_nexp n1 ^ " > " ^ string_of_nexp n2 | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_lt (n1, n2), _) -> string_of_nexp n1 ^ " < " ^ string_of_nexp n2 | NC_aux (NC_or (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_and (nc1, nc2), _) -> |