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/constraint.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/constraint.ml')

diff --git a/src/constraint.ml b/src/constraint.ml
index 1a4129ff..6c34bc9b 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -192,7 +192,9 @@ let to_smt l vars constr =
     match aux with
     | NC_equal (nexp1, nexp2) -> sfun "=" [smt_nexp nexp1; smt_nexp nexp2]
     | NC_bounded_le (nexp1, nexp2) -> sfun "<=" [smt_nexp nexp1; smt_nexp nexp2]
+    | NC_bounded_lt (nexp1, nexp2) -> sfun "<" [smt_nexp nexp1; smt_nexp nexp2]
     | NC_bounded_ge (nexp1, nexp2) -> sfun ">=" [smt_nexp nexp1; smt_nexp nexp2]
+    | NC_bounded_gt (nexp1, nexp2) -> sfun ">" [smt_nexp nexp1; smt_nexp nexp2]
     | NC_not_equal (nexp1, nexp2) -> sfun "not" [sfun "=" [smt_nexp nexp1; smt_nexp nexp2]]
     | NC_set (v, ints) ->
        sfun "or" (List.map (fun i -> sfun "=" [smt_var v; Atom (Big_int.to_string i)]) ints)
-- 
cgit v1.2.3