From d2f702da3b5cc9934f8cd3ea457f93c6ce2b6c12 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Jun 2019 17:25:47 +0100
Subject: 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.

---
 src/specialize.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/specialize.ml')

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), _) ->
-- 
cgit v1.2.3