From 58d46e240315abb684823812ff1b2a9684653e5d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 30 Apr 2019 19:35:43 +0100
Subject: SMT: Allow custom queries

As an example:

$counterexample :query exist match_failure
function prop(xs: bits(4)) -> unit = {
  match xs {
    _ : bits(3) @ 0b0 => ()
  }
}

Will return

Solver found counterexample: ok
  xs -> 0x1

as we are asking for an input such that a match failure occurs,
meanwhile

$counterexample :query ~(exist match_failure)
function prop(xs: bits(4)) -> unit = {
  match xs {
    _ : bits(3) @ 0b0 => ()
  }
}

will return 0x0 as we are asking for an input such that no match
failure occurs. Note that we can now support properties for
non-boolean functions by not including the return event in the query.
---
 test/smt/match_fail_query_1.sat.sail | 10 ++++++++++
 test/smt/match_fail_query_2.sat.sail | 10 ++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 test/smt/match_fail_query_1.sat.sail
 create mode 100644 test/smt/match_fail_query_2.sat.sail

(limited to 'test')

diff --git a/test/smt/match_fail_query_1.sat.sail b/test/smt/match_fail_query_1.sat.sail
new file mode 100644
index 00000000..15036ad9
--- /dev/null
+++ b/test/smt/match_fail_query_1.sat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$counterexample :query ~(exist match_failure)
+function prop(xs: bits(4)) -> unit = {
+  match xs {
+    _ : bits(3) @ 0b0 => ()
+  }
+}
diff --git a/test/smt/match_fail_query_2.sat.sail b/test/smt/match_fail_query_2.sat.sail
new file mode 100644
index 00000000..8c83f84f
--- /dev/null
+++ b/test/smt/match_fail_query_2.sat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$counterexample :query exist match_failure
+function prop(xs: bits(4)) -> unit = {
+  match xs {
+    _ : bits(3) @ 0b0 => ()
+  }
+}
-- 
cgit v1.2.3