SMT: Add min and max functions

Allow conversion between int(n) and int in smt_conversion

3 files changed, 44 insertions, 0 deletions

diff --git a/test/smt/minmax.unsat.sail b/test/smt/minmax.unsat.sail
new file mode 100644
index 00000000..f1bdf55a
--- /dev/null
+++ b/test/smt/minmax.unsat.sail
@@ -0,0 +1,20 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$property
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(3, 2) == 3);
+  assert(min_int(3, 2) == 2);
+  assert(max_int(-132542345, 3) == 3);
+
+  assert(max_int(a, b) == max_int(b, a));
+  assert(min_int(a, b) == min_int(b, a));
+
+  assert(max_int(0, 0) == 0);
+
+  true
+}
diff --git a/test/smt/minmax_1.sat.sail b/test/smt/minmax_1.sat.sail
new file mode 100644
index 00000000..09119db0
--- /dev/null
+++ b/test/smt/minmax_1.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, a) == max_int(b, a));
+  true
+}
diff --git a/test/smt/minmax_2.sat.sail b/test/smt/minmax_2.sat.sail
new file mode 100644
index 00000000..dd773058
--- /dev/null
+++ b/test/smt/minmax_2.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, b) == min_int(a, b));
+  true
+}