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.
---
 src/smtlib.ml | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'src/smtlib.ml')

diff --git a/src/smtlib.ml b/src/smtlib.ml
index fe7aee5e..d17cb4d9 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -322,12 +322,25 @@ let rec sexp toks =
   in
   parse toks
 
+let parse p delim_regexp input =
+  let delim = Str.regexp delim_regexp in
+  let tokens = Str.full_split delim input in
+  let non_whitespace = function
+    | Str.Delim d when String.trim d = "" -> false
+    | _ -> true
+  in
+  let tokens = List.filter non_whitespace tokens in
+  match p tokens with
+  | Ok (result, []) -> Some result
+  | Ok (result, _) -> None
+  | Fail -> None
+
 let parse_sexps input =
   let delim = Str.regexp "[ \n\t]+\\|(\\|)" in
   let tokens = Str.full_split delim input in
   let non_whitespace = function
-    | Str.Delim "(" | Str.Delim ")" | Str.Text _ -> true
-    | Str.Delim _ -> false
+    | Str.Delim d when String.trim d = "" -> false
+    | _ -> true
   in
   let tokens = List.filter non_whitespace tokens in
   match plist sexp tokens with
@@ -347,7 +360,7 @@ let value_of_sexpr sexpr =
      | _ -> failwith "Cannot parse sexpr as ctyp"
      end
   | _ -> assert false
-          
+
 let rec find_arg id ctyp arg_smt_names = function
   | List [Atom "define-fun"; Atom str; List []; _; value] :: _
        when Util.assoc_compare_opt Id.compare id arg_smt_names = Some (Some str) ->
@@ -365,7 +378,7 @@ let rec run frame =
      run (Interpreter.eval_frame frame)
   | Interpreter.Break frame ->
      run (Interpreter.eval_frame frame)
-  
+
 let check_counterexample ast env fname args arg_ctyps arg_smt_names =
   let open Printf in
   prerr_endline ("Checking counterexample: " ^ fname);
-- 
cgit v1.2.3