Commit 82188ee6 authored by Sylvain Dailler's avatar Sylvain Dailler

Why3 counterex - Changing parsing of prover return statement for altergo.

Adding "I don't know" as a correct keyword for provers return (inside
counterexamples).
Updating scripts because of move from hoare_logic to WP_revisited.

* src/driver/parse_smtv2_model.ml
(parse): Adding I dont know as a keyword.

* bench/bench
Changing to WP_revisited.

* examples/bench.sh
Changing to WP_revisited.

* examples/regtests.sh
Changing to WP_revisited.
parent 3713cd7e
......@@ -194,7 +194,7 @@ goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/in_progress
......
......@@ -15,7 +15,7 @@ echo '<html>' > $HTML
echo '<head><title>Why3 Bench</title></head>' >> $HTML
echo '<body>' >> $HTML
echo '<h1>Why3 bench</h1>' >> $HTML
run_dir () {
echo '<h2>Directory '$1'</h2>' >> $HTML
echo '<ul>' >> $HTML
......@@ -68,7 +68,7 @@ echo ""
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
run_dir WP_revisited
run_dir vacid_0_binary_heaps "-I vacid_0_binary_heaps"
echo ""
......
......@@ -89,7 +89,7 @@ echo ""
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
run_dir WP_revisited
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir avl "-L avl"
run_dir double_wp "-L double_wp"
......@@ -100,6 +100,3 @@ echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
exit $res
......@@ -16,17 +16,17 @@ open Lexing
let debug = Debug.register_info_flag "parse_smtv2_model"
~desc:"Print@ debugging@ messages@ about@ parsing@ model@ \
returned@ from@ cvc4@ or@ z3."
(*
***************************************************************
***************************************************************
** Parser
****************************************************************
*)
let get_position lexbuf =
let pos = lexbuf.lex_curr_p in
let cnum = pos.pos_cnum - pos.pos_bol + 1 in
Loc.user_position
"Model string returned from the prover"
Loc.user_position
"Model string returned from the prover"
pos.pos_lnum
cnum
cnum
......@@ -36,8 +36,8 @@ let do_parsing model =
try
Parse_smtv2_model_parser.output Parse_smtv2_model_lexer.token lexbuf
with
| Parse_smtv2_model_lexer.SyntaxError ->
Warning.emit
| Parse_smtv2_model_lexer.SyntaxError ->
Warning.emit
~loc:(get_position lexbuf)
"Error@ during@ lexing@ of@ smtlib@ model:@ unexpected character";
[]
......@@ -47,21 +47,24 @@ let do_parsing model =
Warning.emit ~loc:loc "Error@ during@ parsing@ of@ smtlib@ model";
[]
end
(* Parses the model returned by CVC4 or Z3.
(* Parses the model returned by CVC4, Z3 or Alt-ergo.
Returns the list of pairs term - value *)
(* For Alt-ergo the output is not the same and we
match on "I don't know". But we also need to begin
parsing on a fresh new line ".*" ensures it *)
let parse input =
try
let r = Str.regexp "unknown\\|sat" in
let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Str.search_forward r input 0);
let match_end = Str.match_end () in
let model_string =
let model_string =
String.sub input match_end ((String.length input) - match_end) in
do_parsing model_string
with
| Not_found -> []
with
| Not_found -> []
let () = register_model_parser "smtv2" parse
~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment