Commit 3a94474f authored by Sylvain Dailler's avatar Sylvain Dailler

Q424-012 Parse z3s boolean expression and floating point value

This commit adds parsing for boolean expression and floating point value
which are returned by z3 on the last version. This adds floating point
values in the collected data and JSON printed data. This does not add
boolean expressions because it does not add information.
Also added transformation eliminate epsilon in driver for Z3 ce.

* drivers/z3_gnatprove_ce.drv
(eliminate_epsilon): Added transformation eliminate epsilon in driver for
counterex for z3.

* src/core/model_parser.ml
(float_type): Added a float_type and functions to send it as JSON data.

* src/driver/collect_data_model.ml
(convert_array_value): Explicit matching for error handling when adding
constructs.
(convert_float): Dummy conversion of float_type to avoid circular
dependency.

* src/driver/parse_smtv2_model_lexer.mll
(token): Adding z3 specific boolean expressions. Also adding a way to
parse all floating point value including those we don't want to print
because we need to parse them even if we don't want to print them.

* src/driver/parse_smtv2_model_parser.mly
(smt_term): Adding floating point value case which is handled in the lexer.
Added boolean_expression case.

* src/driver/smt2_model_defs.ml
(float_type): Adding a duplicated float_type for dependencies reasons.
(print_float): Debugging print of float_type.
(): Adding cases for float in remaining functions.

Change-Id: I5baee2880a9843f0fec61b1bf3edb2a2f3e54bd1
parent 3f732c46
......@@ -27,9 +27,18 @@ let debug = Debug.register_info_flag "model_parser"
****************************************************************
*)
type float_type =
| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| Not_a_number
| Float_value of string * string * string
type model_value =
| Integer of string
| Decimal of (string * string)
| Float of float_type
| Boolean of bool
| Array of model_array
| Record of model_record
......@@ -67,14 +76,42 @@ let array_add_element ~array ~index ~value =
arr_indices = arr_index::array.arr_indices;
}
let convert_float_value f =
match f with
| Plus_infinity ->
let m = Mstr.add "cons" (Json.String "Plus_infinity") Stdlib.Mstr.empty in
Json.Record m
| Minus_infinity ->
let m = Mstr.add "cons" (Json.String "Minus_infinity") Stdlib.Mstr.empty in
Json.Record m
| Plus_zero ->
let m = Mstr.add "cons" (Json.String "Plus_zero") Stdlib.Mstr.empty in
Json.Record m
| Minus_zero ->
let m = Mstr.add "cons" (Json.String "Minus_zero") Stdlib.Mstr.empty in
Json.Record m
| Not_a_number ->
let m = Mstr.add "cons" (Json.String "Not_a_number") Stdlib.Mstr.empty in
Json.Record m
| Float_value (b, eb, sb) ->
let m = Mstr.add "cons" (Json.String "Float_value") Stdlib.Mstr.empty in
let m = Mstr.add "sign" (Json.String b) m in
let m = Mstr.add "exponent" (Json.String eb) m in
let m = Mstr.add "significand" (Json.String sb) m in
Json.Record m
let rec convert_model_value value : Json.json =
match value with
| Integer s ->
let m = Mstr.add "type" (Json.String "Integer") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json.String s) m in
Json.Record m
| Decimal (int_part, fract_part) ->
| Float f ->
let m = Mstr.add "type" (Json.String "Float") Stdlib.Mstr.empty in
let m = Mstr.add "val" (convert_float_value f) m in
Json.Record m
| Decimal (int_part, fract_part) ->
let m = Mstr.add "type" (Json.String "Decimal") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json.String (int_part^"."^fract_part)) m in
Json.Record m
| Unparsed s ->
......
......@@ -14,9 +14,19 @@
** Counter-example model values
****************************************************************
*)
type float_type =
| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| Not_a_number
| Float_value of string * string * string
type model_value =
| Integer of string
| Decimal of (string * string)
| Float of float_type
| Boolean of bool
| Array of model_array
| Record of model_record
......
......@@ -8,7 +8,7 @@ exception Not_value
let rec get_variables_term (table: correspondence_table) t =
match t with
| Variable _ | Function_Local_Variable _ | Boolean _ | Integer _
| Decimal _ | Other _ | Bitvector _ -> table
| Decimal _ | Float _ | Other _ | Bitvector _ -> table
| Array a ->
get_variables_array table a
| Ite (t1, t2, t3, t4) ->
......@@ -29,7 +29,6 @@ let rec get_variables_term (table: correspondence_table) t =
| To_array t ->
get_variables_term table t
and get_variables_array table a =
match a with
| Const t ->
......@@ -143,7 +142,7 @@ and refine_array table a =
their value. *)
and refine_function table term =
match term with
| Integer _ | Decimal _ | Other _ | Bitvector _ | Boolean _ -> term
| Integer _ | Decimal _ | Float _ | Other _ | Bitvector _ | Boolean _ -> term
| Cvc4_Variable v ->
begin
try (
......@@ -192,6 +191,14 @@ and refine_variable_value (table: correspondence_table) key v =
let tv = refine_definition table t in
Mstr.add key (true, tv) table
let convert_float (f: Smt2_model_defs.float_type) : Model_parser.float_type =
match f with
| Plus_infinity -> Model_parser.Plus_infinity
| Minus_infinity -> Model_parser.Minus_infinity
| Plus_zero -> Model_parser.Plus_zero
| Minus_zero -> Model_parser.Minus_zero
| Not_a_number -> Model_parser.Not_a_number
| Float_value (b, eb, sb) -> Model_parser.Float_value (b, eb, sb)
(* Conversion to value referenced as defined in model_parser.
We assume that array indices fit into an integer *)
......@@ -220,6 +227,7 @@ and convert_to_model_value (t: term): Model_parser.model_value =
match t with
| Integer i -> Model_parser.Integer i
| Decimal (d1, d2) -> Model_parser.Decimal (d1, d2)
| Float f -> Model_parser.Float (convert_float f)
| Bitvector bv -> Model_parser.Bitvector bv
| Boolean b -> Model_parser.Boolean b
| Other _s -> raise Not_value
......@@ -229,7 +237,7 @@ and convert_to_model_value (t: term): Model_parser.model_value =
| Cvc4_Variable _v -> Model_parser.Unparsed "!"
(* TODO change the value returned for non populated Cvc4 variable '!' -> '?' ? *)
| To_array t -> convert_to_model_value (Array (convert_z3_array t))
| _ -> raise Not_value
| Function_Local_Variable _ | Variable _ | Ite _ | Discr _ -> raise Not_value
and convert_z3_array (t: term) : array =
......@@ -369,7 +377,8 @@ let create_list (table: correspondence_table) =
Mstr.fold (fun key v acc -> refine_variable_value acc key v) table table in
(* Then converts all variables to raw_model_element *)
Mstr.fold (fun key value list_acc ->
Mstr.fold
(fun key value list_acc ->
let t = match value with
| (_, Term t) ->
Some t
......@@ -377,4 +386,6 @@ let create_list (table: correspondence_table) =
Some t
| _ -> None in
try (convert_to_model_element key t :: list_acc)
with Not_value -> list_acc) table []
with Not_value -> list_acc)
table
[]
......@@ -20,6 +20,9 @@ let num = ['0'-'9']+
let opt_num = ['0'-'9']*
let dec_num = num"."num
let name = (['a'-'z']*'_'*['0'-'9']*)*
let dummy = ('_''_''_')?
let float_num = '#'('b' | 'x') num
rule token = parse
| '\n'
......@@ -44,31 +47,44 @@ rule token = parse
| "declare-fun" { DECLARE_FUN }
| "declare-sort" { DECLARE_SORT } (* z3 declare functions *)
| "forall" { FORALL } (* z3 cardinality *)
| "not" { NOT } (* Z3 specific *)
| "and" { AND } (* z3 specific in ite *)
| "<=" { LE } (* z3 specific *)
| ">=" { GE } (* z3 specific *)
| "declare-datatypes" { DECLARE_DATATYPES }
| "let" { LET }
| "true" { TRUE }
| "false" { FALSE }
| "LAMBDA" { LAMBDA }
| "ARRAY_LAMBDA" { ARRAY_LAMBDA }
| "mk___split_fields"(opt_num as n) opt_num "___" {
| "mk___split_fields"(opt_num as n) dummy {
match n with
| "" -> MK_SPLIT_FIELD ("mk___split_fields",0)
| n -> MK_SPLIT_FIELD ("mk____split_fields"^n, int_of_string n) }
| "mk___rep"(opt_num as n) opt_num "___" {
| n -> MK_SPLIT_FIELD ("mk___split_fields"^n, int_of_string n) }
| "mk___rep"(opt_num as n) dummy {
match n with
| "" -> MK_REP ("mk___rep", 0)
| n -> MK_REP ("mk___rep"^n, int_of_string n) }
| "mk___t"(opt_num as n) opt_num "___" {
| "mk___t"(opt_num as n) dummy {
match n with
| "" -> MK_T ("mk___t", 0)
| n -> MK_T ("mk___t"^n, int_of_string n) }
| "mk___split_discrs"(opt_num as n) opt_num "___" {
| "mk___split_discrs"(opt_num as n) dummy {
match n with
| "" -> MK_SPLIT_DISCRS ("mk___split_discrs",0)
| n -> MK_SPLIT_DISCRS ("mk____split_discrs"^n, int_of_string n) }
| "mk" name "___" { MK_ANYTHING } (* encapsulate mk_int_ref etc (other refs) *)
| "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE bv_value }
| "(_ BitVec "num")" { BITVECTOR_TYPE }
| n -> MK_SPLIT_DISCRS ("mk___split_discrs"^n, int_of_string n) }
| "mk" name dummy { MK_ANYTHING } (* encapsulate mk_int_ref etc (other refs) *)
| "(_" space+ "bv"(num as bv_value) space+ num")" { BITVECTOR_VALUE bv_value }
| "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
| "(_" space+ "+zero" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Plus_zero }
| "(_" space+ "-zero" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Minus_zero }
| "(_" space+ "+oo" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Plus_infinity }
| "(_" space+ "-oo" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Minus_infinity }
| "(_" space+ "NaN" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Not_a_number }
| "(fp" space+ (float_num as b) space+ (float_num as eb) space+ (float_num as sb) ")"
{ FLOAT_VALUE (Smt2_model_defs.Float_value (b, eb, sb)) }
| num as integer
{ INT_STR (integer) }
| '-'space*(num as integer) { MINUS_INT_STR ("-"^integer) }
......
......@@ -32,6 +32,8 @@
%token ARRAY_LAMBDA
%token TRUE FALSE
%token LET
%token AND LE GE NOT
%token <Smt2_model_defs.float_type> FLOAT_VALUE
%token <string> COMMENT
%token <string> BITVECTOR_VALUE
%token BITVECTOR_TYPE
......@@ -93,6 +95,9 @@ smt_term:
| array { Smt2_model_defs.Array $1 }
| bitvector { Smt2_model_defs.Bitvector $1 }
| boolean { Smt2_model_defs.Boolean $1 }
(* z3 sometimes answer with boolean expressions for some reason ? *)
| boolean_expression { Smt2_model_defs.Other "" }
| FLOAT_VALUE { Smt2_model_defs.Float $1 }
(* ite (= ?a ?b) ?c ?d *)
| LPAREN ITE ps pair_equal ps smt_term ps smt_term RPAREN
{ match $4 with
......@@ -130,9 +135,16 @@ list_let:
(* Condition of an if-then-else. We are only interested in equality case *)
pair_equal:
| LPAREN AND SPACE list_pair_equal RPAREN { None }
| LPAREN EQUAL ps smt_term ps smt_term RPAREN { Some ($4, $6) }
| application { None }
| name { None }
(* ITE containing boolean expressions cannot be dealt with for counterex *)
| LPAREN NOT SPACE smt_term RPAREN { None }
list_pair_equal:
| { }
| pair_equal ps list_pair_equal { }
list_smt_term:
| smt_term { [$1] }
......@@ -175,6 +187,15 @@ name:
(* Should not happen in relevant part of the model (ad hoc) *)
| BITVECTOR_TYPE { "" }
(* Z3 specific boolean expression. This should maybe be used in the future as
it may give some information on the counterexample. *)
boolean_expression:
| LPAREN ps FORALL SPACE LPAREN ps args_lists RPAREN ps smt_term ps RPAREN { }
| LPAREN NOT SPACE smt_term RPAREN { }
| LPAREN LE SPACE smt_term SPACE smt_term RPAREN { }
| LPAREN GE SPACE smt_term SPACE smt_term RPAREN { }
| LPAREN AND ps list_smt_term RPAREN { }
integer:
| INT_STR { $1 }
| LPAREN ps MINUS_INT_STR ps RPAREN
......
......@@ -2,6 +2,14 @@ open Stdlib
type variable = string
type float_type =
| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| Not_a_number
| Float_value of string * string * string
type array =
| Const of term
| Store of array * term * term
......@@ -9,6 +17,7 @@ type array =
and term =
| Integer of string
| Decimal of (string * string)
| Float of float_type
| Other of string
| Array of array
| Bitvector of string
......@@ -31,6 +40,15 @@ type definition =
associated definition (complex stuff) *)
type correspondence_table = (bool * definition) Mstr.t
let print_float fmt f =
match f with
| Plus_infinity -> Format.fprintf fmt "Plus_infinity"
| Minus_infinity -> Format.fprintf fmt "Minus_infinity"
| Plus_zero -> Format.fprintf fmt "Plus_zero"
| Minus_zero -> Format.fprintf fmt "Minus_zero"
| Not_a_number -> Format.fprintf fmt "NaN"
| Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb
let rec print_array fmt a =
match a with
| Const t -> Format.fprintf fmt "CONST : %a" print_term t
......@@ -43,6 +61,7 @@ and print_term fmt t =
match t with
| Integer s -> Format.fprintf fmt "Integer: %s" s
| Decimal (s1, s2) -> Format.fprintf fmt "Decimal: %s . %s" s1 s2
| Float f -> Format.fprintf fmt "Float: %a" print_float f
| Other s -> Format.fprintf fmt "Other: %s" s
| Array a -> Format.fprintf fmt "Array: %a" print_array a
| Bitvector bv -> Format.fprintf fmt "Bv: %s" bv
......@@ -113,7 +132,7 @@ and make_local vars_lists t =
let t3 = make_local vars_lists t3 in
let t4 = make_local vars_lists t4 in
Ite (t1, t2, t3, t4)
| Integer _ | Decimal _ | Other _ -> t
| Integer _ | Decimal _ | Float _ | Other _ -> t
| Bitvector _ -> t
| Cvc4_Variable _ -> raise Bad_local_variable
| Boolean _ -> t
......@@ -148,7 +167,7 @@ let build_record_discr lgen =
let rec subst var value t =
match t with
| Integer _ | Decimal _ | Other _ | Bitvector _ | Boolean _ ->
| Integer _ | Decimal _ | Float _ | Other _ | Bitvector _ | Boolean _ ->
t
| Array a -> Array (subst_array var value a)
| Cvc4_Variable _ -> raise Bad_local_variable
......
open Stdlib
type variable = string
type float_type =
| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| Not_a_number
| Float_value of string * string * string
type array =
| Const of term
| Store of array * term * term
......@@ -11,6 +17,7 @@ type array =
and term =
| Integer of string
| Decimal of (string * string)
| Float of float_type
| Other of string
| Array of array
| Bitvector of string
......
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