SMT: Add reals and strings to SMT backend

Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.

Strings are likewise encoded as SMTLIB strings, for similar reasons.

Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.

4 files changed, 49 insertions, 0 deletions

diff --git a/test/smt/sqrt.sat.sail b/test/smt/sqrt.sat.sail
new file mode 100644
index 00000000..1cb47944
--- /dev/null
+++ b/test/smt/sqrt.sat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+$include <real.sail>
+
+$counterexample
+function prop(x: real) -> bool = {
+  not_bool(sqrt(x) == 2.0);
+}
diff --git a/test/smt/sqrt.unsat.sail b/test/smt/sqrt.unsat.sail
new file mode 100644
index 00000000..6aba221c
--- /dev/null
+++ b/test/smt/sqrt.unsat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+$include <real.sail>
+
+$property
+function prop() -> bool = {
+  sqrt(4.0) == 2.0;
+}
diff --git a/test/smt/string.sat.sail b/test/smt/string.sat.sail
new file mode 100644
index 00000000..c9c45b66
--- /dev/null
+++ b/test/smt/string.sat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "concat_str" : (string, string) -> string
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+$counterexample
+function prop(x : string) -> bool = {
+  let y = ", World!";
+  not_bool(concat_str(x, y) == "Hello, World!")
+}
\ No newline at end of file
diff --git a/test/smt/string.unsat.sail b/test/smt/string.unsat.sail
new file mode 100644
index 00000000..b91abfad
--- /dev/null
+++ b/test/smt/string.unsat.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "concat_str" : (string, string) -> string
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+$property
+function prop(() : unit) -> bool = {
+  let x = "Hello, ";
+  let y = "World!";
+  concat_str(x, y) == "Hello, World!"
+}
\ No newline at end of file