From ff4b53fba32ebdb6cb587fac0bc5f4a523304a55 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 8 May 2019 18:14:51 +0100
Subject: 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.
---
 test/smt/sqrt.sat.sail     |  9 +++++++++
 test/smt/sqrt.unsat.sail   |  9 +++++++++
 test/smt/string.sat.sail   | 15 +++++++++++++++
 test/smt/string.unsat.sail | 16 ++++++++++++++++
 4 files changed, 49 insertions(+)
 create mode 100644 test/smt/sqrt.sat.sail
 create mode 100644 test/smt/sqrt.unsat.sail
 create mode 100644 test/smt/string.sat.sail
 create mode 100644 test/smt/string.unsat.sail

(limited to 'test/smt')

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