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.

0 files changed, 0 insertions, 0 deletions